mem_L1_toReal_of_lintegral_ne_top

English

If a nonnegative a.e.-measurable f has finite lintegral, then its L1-norm is finite and its real part is integrable.

Русский

Если неотрицательная a.e.-измеримая f имеет конечный лин-интеграл, то её L1-норма конечна, и вещественна часть интегрируема.

LaTeX

$$MemLp (fun x => (f x).toReal) 1 μ$$

Lean4

theorem mem_L1_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
    MemLp (fun x ↦ (f x).toReal) 1 μ :=
  by
  rw [MemLp, eLpNorm_one_eq_lintegral_enorm]
  exact ⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable, hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩

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