mono — Mathlib

English

If hf is locally integrable and g is dominated by f almost everywhere, then g is locally integrable.

Русский

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

LaTeX

$$$\\text{LocallyIntegrableOn}(f,s,μ) \\Rightarrow \\text{LocallyIntegrableOn}(g,s,μ)\\quad (‖g(x)‖ ≤ ‖f(x)‖ \\text{ a.e.})$$$

Lean4

theorem mono {f : X → E} (hf : LocallyIntegrableOn f s μ) {g : X → F} (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) : LocallyIntegrableOn g s μ :=
  by
  intro x hx
  rcases hf x hx with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩

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