integrable_smul_const — Mathlib

English

If c ≠ 0, then for any f, Integrable (c • f) ⇔ Integrable f.

Русский

Если c ≠ 0, тогда для любых f: Integrable(c • f) ⇔ Integrable f.

LaTeX

$$$c \neq 0 \Rightarrow \big( \mathrm{Integrable}(c \cdot f) \iff \mathrm{Integrable}(f) \big).$$$

Lean4

theorem integrable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) : Integrable (fun x => f x • c) μ ↔ Integrable f μ :=
  by
  simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
    hasFiniteIntegral_iff_enorm, enorm_smul]
  intro _; rw [lintegral_mul_const' _ _ enorm_ne_top, ENNReal.mul_lt_top_iff]
  have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
  simp [hc, or_iff_left_of_imp (this _)]

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