mono' — Mathlib

English

If g is integrable, f is AEStronglyMeasurable, and almost everywhere ||f|| ≤ g, then f is integrable (Real-valued case).

Русский

Если g интегрируема, f — AEStronglyMeasurable, и почти всюду выполняется ||f|| ≤ g, то f интегрируема.

LaTeX

$$$\operatorname{Integrable}(g, \mu) \Rightarrow \operatorname{AEStronglyMeasurable}(f, \mu) \Rightarrow \forall^\mathrm{ae} a, \|f(a)\| ≤ g(a) \Rightarrow \operatorname{Integrable}(f, \mu)$$$

Lean4

theorem mono' {f : α → β} {g : α → ℝ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ a ∂μ, ‖f a‖ ≤ g a) :
    Integrable f μ :=
  ⟨hf, hg.hasFiniteIntegral.mono' h⟩

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