mono — Mathlib

English

If g is integrable, f is AEStronglyMeasurable, and almost everywhere ||f|| ≤ ||g||, then f is integrable.

Русский

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

LaTeX

$$$\operatorname{Integrable}(g, \mu) \to \operatorname{AEStronglyMeasurable}(f, \mu) \to \forall^\mathrm{ae} a, \|f(a)\| \le \|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⟩

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