English
If f is interval-integrable on [a,b], AEStronglyMeasurable g on μ restricted to [a,b], and ‖g‖ ≤ᵐ μ.restrict [a,b] ‖f‖, then g is interval-integrable on [a,b].
Русский
Если f интервал-интегрируема на [a,b], g достигает AEStronglyMeasurable, и почти везде ‖g‖ ≤ ‖f‖, то g интервал-интегрируема на [a,b].
LaTeX
$$$\operatorname{IntervalIntegrable}(f,\nu,a,b) \rightarrow (\text{AEStronglyMeasurable}(g,\mu|_{I[a,b]})) \rightarrow (\|g\| \le^*_{\mu|_{I[a,b]}} \|f\|) \Rightarrow \operatorname{IntervalIntegrable}(g,\mu,a,b)$$$
Lean4
theorem mono_fun {f : ℝ → E} [NormedAddCommGroup F] {g : ℝ → F} (hf : IntervalIntegrable f μ a b)
(hgm : AEStronglyMeasurable g (μ.restrict (Ι a b))) (hle : (fun x => ‖g x‖) ≤ᵐ[μ.restrict (Ι a b)] fun x => ‖f x‖) :
IntervalIntegrable g μ a b :=
intervalIntegrable_iff.2 <| hf.def'.integrable.mono hgm hle
