integrable_smul_measure — Mathlib

English

If c ≠ 0 and c ≠ ∞, integrability with respect to μ is equivalent to integrability with respect to c⁻¹·μ.

Русский

Если c ≠ 0 и c ≠ ∞, интегрируемость по μ эквивалентна интегрируемости по c⁻¹·μ.

LaTeX

$$Ne c 0 → Ne c ∞ → Integrable f (c⁻¹ • μ) ↔ Integrable f μ$$

Lean4

theorem integrable_smul_measure {f : α → ε} {c : ℝ≥0∞} (h₁ : c ≠ 0) (h₂ : c ≠ ∞) :
    Integrable f (c • μ) ↔ Integrable f μ :=
  ⟨fun h => by
    simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using h.smul_measure (ENNReal.inv_ne_top.2 h₁),
    fun h => h.smul_measure h₂⟩

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