mono_fun_enorm — Mathlib

English

If f is interval-integrable on [a,b] and Ι c d ≤ᵐ[μ] Ι a b, then f is interval-integrable on [c,d].

Русский

Если f интервал-интегрируема на [a,b] и Ιc d ≤ᵐ[μ] Ι a b, тогда на [c,d].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,μ,a,b) \rightarrow (Ι c d ≤ᵐ[μ] Ι a b) \rightarrow \operatorname{IntervalIntegrable}(f,μ,c,d)$$$

Lean4

theorem mono_fun_enorm [PseudoMetrizableSpace ε'] {g : ℝ → ε'} (hf : IntervalIntegrable f μ a b)
    (hgm : AEStronglyMeasurable g (μ.restrict (Ι a b))) (hle : (‖g ·‖ₑ) ≤ᵐ[μ.restrict (Ι a b)] (‖f ·‖ₑ)) :
    IntervalIntegrable g μ a b :=
  intervalIntegrable_iff.2 <| hf.def'.integrable.mono_enorm hgm hle

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