mono_enorm — Mathlib

English

If g is integrable, f is AEStronglyMeasurable, and |f| ≤ |g| holds a.e., then f is integrable.

Русский

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

LaTeX

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

Lean4

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

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