eLpNorm_congr_enorm_ae — Mathlib

English

If f and g are almost everywhere such that their ENorm values are equal almost everywhere, then eLpNorm f equals eLpNorm g.

Русский

Если значения ENorm функции совпадают почти всюду, то eLpNorm соответствующих функций совпадает.

LaTeX

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

Lean4

theorem eLpNorm_congr_enorm_ae {f : α → ε} {g : α → ε'} (hfg : ∀ᵐ x ∂μ, ‖f x‖ₑ = ‖g x‖ₑ) :
    eLpNorm f p μ = eLpNorm g p μ :=
  le_antisymm (eLpNorm_mono_enorm_ae <| EventuallyEq.le hfg) (eLpNorm_mono_enorm_ae <| (EventuallyEq.symm hfg).le)

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