comp_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_div {g : ℝ → F} (hg : Integrable g) {R : ℝ} (hR : R ≠ 0) : Integrable fun x => g (x / R) :=
  (integrable_comp_div_iff g hR).2 hg

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