eLpNorm_congr_norm_ae — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem eLpNorm_congr_norm_ae {f : α → F} {g : α → G} (hfg : ∀ᵐ x ∂μ, ‖f x‖ = ‖g x‖) : eLpNorm f p μ = eLpNorm g p μ :=
  eLpNorm_congr_nnnorm_ae <| hfg.mono fun _x hx => NNReal.eq hx

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