norm_le_norm_of_ae_le — Mathlib

English

If almost everywhere ‖f x‖ ≤ ‖g x‖, then ‖f‖ ≤ ‖g‖.

Русский

Если почти всюду ‖f(x)‖ ≤ ‖g(x)‖, то ‖f‖ ≤ ‖g‖.

LaTeX

$$$\forall^{\mathrm{ae}} x, \|f(x)\| ≤ \|g(x)\| \Rightarrow \|f\| ≤ \|g\|$$$

Lean4

theorem norm_le_norm_of_ae_le {f : Lp E p μ} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : ‖f‖ ≤ ‖g‖ :=
  by
  rw [norm_def, norm_def]
  exact ENNReal.toReal_mono (by finiteness) (eLpNorm_mono_ae h)

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