add_measure — Mathlib

English

If f is Integrable w.r.t μ, then for any finite ENNReal c ≠ ∞, f is Integrable w.r.t c•μ.

Русский

Если f интегрируема по μ, то для любого конечного c ≠ ∞, f интегрируема по c·μ.

LaTeX

$$Integrable f μ → ∀ c ≠ ∞, Integrable f (c • μ).$$

Lean4

@[fun_prop]
theorem add_measure [PseudoMetrizableSpace ε] {f : α → ε} (hμ : Integrable f μ) (hν : Integrable f ν) :
    Integrable f (μ + ν) := by
  simp_rw [← memLp_one_iff_integrable] at hμ hν ⊢
  refine ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩
  rw [eLpNorm_one_add_measure, ENNReal.add_lt_top]
  exact ⟨hμ.eLpNorm_lt_top, hν.eLpNorm_lt_top⟩

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