eLpNorm_mono_ae_real — Mathlib

English

If for all x, ‖f(x)‖ ≤ g(x) with g real-valued, then eLpNorm f p μ ≤ eLpNorm g p μ.

Русский

Если для всех x ‖f(x)‖ ≤ g(x) при g вещественного типа, то eLpNorm(f) ≤ eLpNorm(g).

LaTeX

$$$\\forall x, \\|f(x)\\| ≤ g(x) \\Rightarrow eLpNorm(f,p,μ) ≤ eLpNorm(g,p,μ)$.$$

Lean4

theorem eLpNorm_mono_ae_real {f : α → F} {g : α → ℝ} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ g x) : eLpNorm f p μ ≤ eLpNorm g p μ :=
  eLpNorm_mono_ae <| h.mono fun _x hx => hx.trans ((le_abs_self _).trans (Real.norm_eq_abs _).symm.le)

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