mono — Mathlib

English

If f is locally integrable, then any g with a.e. bound by f is locally integrable.

Русский

Если f локально интегрируема, то любой g, удовлетворяющий почти всюду условию |g| ≤ |f|, локально интегрируем.

LaTeX

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

Lean4

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

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