instNorm — Mathlib

English

Lp is a normed space with norm defined by ‖f‖ = toReal(eLpNorm f p μ).

Русский

Lp является нормированным пространством; норма задана ‖f‖ = toReal(eLpNorm(f,p,μ)).

LaTeX

$$‖f‖ = toReal(eLpNorm(f,p,μ))$$

Lean4

instance instNorm : Norm (Lp E p μ) where
  norm
    f :=
    ENNReal.toReal
      (eLpNorm f p μ)
        -- note: we need this to be defeq to the instance from `SeminormedAddGroup.toNNNorm`, so
        -- can't use `ENNReal.toNNReal (eLpNorm f p μ)`

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