integrable_toReal_of_lintegral_ne_top

English

If f is a.e.-measurable and its lintegral is finite, then ∫ f dμ < ∞ implies integrability of its real part.

Русский

Если f измеримо почти всюду и лин.интеграл конечен, то интегрируемость по Real следует из конечности лин.интеграла.

LaTeX

$$Integrable (f) μ ↔ ∫⁻ f < ∞$$

Lean4

theorem integrable_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
    Integrable (fun x ↦ (f x).toReal) μ :=
  memLp_one_iff_integrable.1 <| mem_L1_toReal_of_lintegral_ne_top hfm hfi

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