mono_enorm — Mathlib

English

If f is locally integrable and g is a.e. bounded in norm by f, then g is locally integrable.

Русский

Если f локально интегрируема и почти везде по норме ограничена сверху на g на f, то g локально интегрируема.

LaTeX

$$$\\operatorname{LocallyIntegrable} f\\mu \\Rightarrow \\forall g,\\ \\text{AEStronglyMeasurable } g\\mu \\wedge (\\forall^{\\!a.e.} x, \\|g(x)\\| \\le \\|f(x)\\|) \\Rightarrow \\operatorname{LocallyIntegrable} g\\mu$$$

Lean4

theorem mono_enorm (hf : LocallyIntegrable f μ) {g : X → ε'} (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ x ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) : LocallyIntegrable g μ :=
  by
  rw [← locallyIntegrableOn_univ] at hf ⊢
  exact hf.mono_enorm hg h

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