integrable_comp_div_iff — Mathlib

English

Let g: ℝ → F and R ≠ 0. Then g(x/R) is integrable iff g is integrable (with Lebesgue measure).

Русский

Пусть g: ℝ → F и R ≠ 0. Тогда g( x / R ) интегрируема ⇔ g интегрируема по мере Лебега.

LaTeX

$$$\\int_{\\mathbb{R}} \\|g(x/R)\\| \\, dx < \\infty \\;\\Leftrightarrow\\; \\int_{\\mathbb{R}} \\|g(x)\\| \\, dx < \\infty, \\quad R \\neq 0.$$$

Lean4

theorem integrable_comp_div_iff (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) : (Integrable fun x => g (x / R)) ↔ Integrable g :=
  integrable_comp_mul_right_iff g (inv_ne_zero hR)

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