comp_mul_right' — Mathlib

English

If g is integrable, then for any nonzero R the function x ↦ g(xR) is integrable with respect to Lebesgue measure.

Русский

Если g интегрируема, то для любого ненулевого R функция x ↦ g(xR) интегрируема по мере Лебега.

LaTeX

$$$\\text{Integrable}(g) \\Rightarrow \\text{Integrable}(x \\mapsto g(xR)), \\; R \\neq 0.$$$

Lean4

theorem comp_mul_right' {g : ℝ → F} (hg : Integrable g) {R : ℝ} (hR : R ≠ 0) : Integrable fun x => g (x * R) :=
  (integrable_comp_mul_right_iff g hR).2 hg

Похожие утверждения