eLpNorm'_mono_enorm_ae — Mathlib

English

If q ≥ 0 and almost everywhere ‖f(x)‖ ≤ ‖g(x)‖, then the Lp' quasi-norm eLpNorm' satisfies eLpNorm'(f,q,μ) ≤ eLpNorm'(g,q,μ).

Русский

Если q ≥ 0 и почти везде выполнено ‖f(x)‖ ≤ ‖g(x)‖, то нормa eLpNorm'(f,q,μ) не превосходит eLpNorm'(g,q,μ).

LaTeX

$$$0 \\le q \\quad\\text{and}\\quad \\ae x\\, (f(x) ) ≤ ‖g(x)‖$ implies $eLpNorm'(f,q,μ) ≤ eLpNorm'(g,q,μ)$.$$

Lean4

theorem eLpNorm'_mono_enorm_ae {f : α → ε} {g : α → ε'} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) :
    eLpNorm' f q μ ≤ eLpNorm' g q μ := by
  simp only [eLpNorm'_eq_lintegral_enorm]
  gcongr ?_ ^ (1 / q)
  refine lintegral_mono_ae (h.mono fun x hx => ?_)
  gcongr

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