integrable_comp_mul_left_iff — Mathlib

English

Let g: ℝ → F be a function and R ≠ 0. Then g(R·) is integrable on ℝ with respect to Lebesgue measure iff g is integrable on ℝ.

Русский

Пусть g: ℝ → F; при R ≠ 0 интегрируемость g(R·) эквивалентна интегрируемости g на ℝ по мере Лебега.

LaTeX

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

Lean4

theorem integrable_comp_mul_left_iff (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) :
    (Integrable fun x => g (R * x)) ↔ Integrable g := by
  simpa only [smul_eq_mul] using integrable_comp_smul_iff volume g hR

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