mono_fun_enorm' — Mathlib

English

If hg is IntervalIntegrable of g and hfm AEStronglyMeasurable f with hle: ‖f‖ ≤ᵐ g, then f is interval-integrable on [a,b].

Русский

Если hg: IntervalIntegrable(g) и hfm: AEStronglyMeasurable(f) и hle: ‖f‖ ≤ᵐ g, то f интервал-интегрируема на [a,b].

LaTeX

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

Lean4

theorem mono_fun_enorm' {f : ℝ → ε} {g : ℝ → ℝ≥0∞} (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_enorm hfm hle

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