aefinStronglyMeasurable_of_aemeasurable

English

If f: α → ℝ≥0∞ is measurable and its lintegral is finite, then there exists an a.e.-equal representative that is FinStronglyMeasurable, i.e., f is AEFinStronglyMeasurable with respect to μ.

Русский

Если f: α → ℝ≥0∞ измерима и её линегральный интеграл конечен, то существует представитель, равный f почти везде, который является FinStronglyMeasurable, то есть f является AEFinStronglyMeasurable по μ.

LaTeX

$$$\text{Measurable}(f) \wedge \int f \, d\mu \neq \infty \Rightarrow \text{AEFinStronglyMeasurable}(f,\mu)$$$

Lean4

theorem aefinStronglyMeasurable_of_aemeasurable (hf : ∫⁻ x, f x ∂μ ≠ ∞) (hf_meas : AEMeasurable f μ) :
    AEFinStronglyMeasurable f μ :=
  by
  refine ⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk, hf_meas.ae_eq_mk⟩
  rwa [lintegral_congr_ae hf_meas.ae_eq_mk.symm]

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