mono_fun' — Mathlib

English

If f is interval-integrable on [a,b], and g is measurable with an almost everywhere bound by ‖f‖, then g is interval-integrable on [a,b].

Русский

Если f интервал-интегрируема на [a,b], а g измерим и почти везде ограничен сверху ‖f‖, то g интервал-интегрируема на [a,b].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \rightarrow \operatorname{AEStronglyMeasurable}(g,\mu|_{I[a,b]}) \rightarrow (\|g\| ≤^* \|f\|) \Rightarrow \operatorname{IntervalIntegrable}(g,\mu,a,b)$$$

Lean4

theorem mono_fun' {f : ℝ → E} {g : ℝ → ℝ} (hg : IntervalIntegrable g μ a b)
    (hfm : AEStronglyMeasurable f (μ.restrict (Ι a b))) (hle : (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Ι a b)] g) :
    IntervalIntegrable f μ a b :=
  intervalIntegrable_iff.2 <| hg.def'.integrable.mono' hfm hle

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