eLpNorm_congr_nnnorm_ae — Mathlib

English

If nnnorm(f(x)) equals nnnorm(g(x)) a.e., then eLpNorm f p μ equals eLpNorm g p μ.

Русский

Если nnnorm(f(x)) = nnnorm(g(x)) почти всюду, то eLpNorm f = eLpNorm g.

LaTeX

$$$\text{If } \forall^{\mathrm{a}} x, \; \|f(x)\|_{+} = \|g(x)\|_{+}, \text{ then } eLpNorm\; f\; p\; μ = eLpNorm\; g\; p\; μ.$$$

Lean4

theorem eLpNorm_congr_nnnorm_ae {f : α → F} {g : α → G} (hfg : ∀ᵐ x ∂μ, ‖f x‖₊ = ‖g x‖₊) :
    eLpNorm f p μ = eLpNorm g p μ :=
  le_antisymm (eLpNorm_mono_nnnorm_ae <| EventuallyEq.le hfg) (eLpNorm_mono_nnnorm_ae <| (EventuallyEq.symm hfg).le)

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