English
Let f be a μ′-integrable function valued in a normed additive group, and suppose f is strongly measurable with respect to a coarser σ-algebra. Then f is integrable with respect to the trimmed measure μ′ trimmed by hm.
Русский
Пусть f — функция, интегрируемая по мере μ′, принимающая значения в нормированном аддитивном группе, и пусть f существенно измерима относительно меньшей σ-алгебры. Тогда f интегрируема по мере μ′.trim hm.
LaTeX
$$$ (hm: m \\le m_0) \\; (hf_{int}: \\operatorname{Integrable}(f,\\mu')) \\; (hf: \\operatorname{StronglyMeasurable}[m] f) \\Rightarrow \\operatorname{Integrable}(f, \\mu'.\\mathrm{trim}(hm))$$$
Lean4
theorem trim (hm : m ≤ m0) (hf_int : Integrable f μ') (hf : StronglyMeasurable[m] f) : Integrable f (μ'.trim hm) :=
by
refine ⟨hf.aestronglyMeasurable, ?_⟩
rw [HasFiniteIntegral, lintegral_trim hm _]
· exact hf_int.2
· fun_prop
