integrable_of_integrable_trim — Mathlib

English

If f is integrable with respect to the trimmed measure μ′.trim hm and f is strongly measurable, then f is integrable with respect to μ′.

Русский

Если f интегрируема по μ′.trim hm и сильно измерима, то f интегрируема по μ′.

LaTeX

$$$ (hm: m \\le m_0) \\; (hf_{int}: \\operatorname{Integrable}(f,\\mu'.trim hm)) \\; (hf: \\operatorname{StronglyMeasurable}[m] f) \\Rightarrow \\operatorname{Integrable}(f,\\mu')$$$

Lean4

theorem integrable_of_integrable_trim (hm : m ≤ m0) (hf_int : Integrable f (μ'.trim hm)) : Integrable f μ' :=
  by
  obtain ⟨hf_meas_ae, hf⟩ := hf_int
  refine ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, ?_⟩
  simpa [HasFiniteIntegral, lintegral_trim_ae hm hf_meas_ae.enorm] using hf

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