Documentation

Mathlib.Analysis.Normed.Lp.WithLp

The WithLp type synonym #

WithLp p V is a copy of V with exactly the same vector space structure, but with the Lp norm instead of any existing norm on V; recall that by default ι → R and R × R are equipped with a norm defined as the supremum of the norms of their components.

This file defines the vector space structure for all types V; the norm structure is built for different specializations of V in downstream files.

Note that this should not be used for infinite products, as in these cases the "right" Lp spaces is not the same as the direct product of the spaces. See the docstring in Mathlib/Analysis/PiLp for more details.

Main definitions #

Implementation notes #

The pattern here is the same one as is used by Lex for order structures; it avoids having a separate synonym for each type (ProdLp, PiLp, etc), and allows all the structure-copying code to be shared.

TODO: is it safe to copy across the topology and uniform space structure too for all reasonable choices of V?

def WithLp (_p : ENNReal) (V : Type uV) :
Type uV

A type synonym for the given V, associated with the Lp norm. Note that by default this just forgets the norm structure on V; it is up to downstream users to implement the Lp norm (for instance, on Prod and finite Pi types).

Equations
Instances For
    def WithLp.equiv (p : ENNReal) (V : Type uV) :
    WithLp p V V

    The canonical equivalence between WithLp p V and V. This should always be used to convert back and forth between the representations.

    Equations
    Instances For
      instance WithLp.instNontrivial (p : ENNReal) (V : Type uV) [Nontrivial V] :
      Equations
      • = inst
      instance WithLp.instUnique (p : ENNReal) (V : Type uV) [Unique V] :
      Equations

      WithLp p V inherits various module-adjacent structures from V.

      instance WithLp.instModule (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] :
      Module K (WithLp p V)
      Equations
      instance WithLp.instIsScalarTower (p : ENNReal) (K : Type uK) (K' : Type uK') (V : Type uV) [Semiring K] [Semiring K'] [AddCommGroup V] [SMul K K'] [Module K V] [Module K' V] [IsScalarTower K K' V] :
      Equations
      • = inst
      instance WithLp.instSMulCommClass (p : ENNReal) (K : Type uK) (K' : Type uK') (V : Type uV) [Semiring K] [Semiring K'] [AddCommGroup V] [Module K V] [Module K' V] [SMulCommClass K K' V] :
      Equations
      • = inst
      instance WithLp.instModuleFinite (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] [Module.Finite K V] :
      Equations
      • = inst

      WithLp.equiv preserves the module structure.

      @[simp]
      theorem WithLp.equiv_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] :
      (WithLp.equiv p V) 0 = 0
      @[simp]
      theorem WithLp.equiv_symm_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] :
      (WithLp.equiv p V).symm 0 = 0
      @[simp]
      theorem WithLp.equiv_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x : WithLp p V) (y : WithLp p V) :
      (WithLp.equiv p V) (x + y) = (WithLp.equiv p V) x + (WithLp.equiv p V) y
      @[simp]
      theorem WithLp.equiv_symm_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x' : V) (y' : V) :
      (WithLp.equiv p V).symm (x' + y') = (WithLp.equiv p V).symm x' + (WithLp.equiv p V).symm y'
      @[simp]
      theorem WithLp.equiv_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x : WithLp p V) (y : WithLp p V) :
      (WithLp.equiv p V) (x - y) = (WithLp.equiv p V) x - (WithLp.equiv p V) y
      @[simp]
      theorem WithLp.equiv_symm_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x' : V) (y' : V) :
      (WithLp.equiv p V).symm (x' - y') = (WithLp.equiv p V).symm x' - (WithLp.equiv p V).symm y'
      @[simp]
      theorem WithLp.equiv_neg (p : ENNReal) {V : Type uV} [AddCommGroup V] (x : WithLp p V) :
      (WithLp.equiv p V) (-x) = -(WithLp.equiv p V) x
      @[simp]
      theorem WithLp.equiv_symm_neg (p : ENNReal) {V : Type uV} [AddCommGroup V] (x' : V) :
      (WithLp.equiv p V).symm (-x') = -(WithLp.equiv p V).symm x'
      @[simp]
      theorem WithLp.equiv_smul (p : ENNReal) {K : Type uK} {V : Type uV} [Semiring K] [AddCommGroup V] [Module K V] (c : K) (x : WithLp p V) :
      (WithLp.equiv p V) (c x) = c (WithLp.equiv p V) x
      @[simp]
      theorem WithLp.equiv_symm_smul (p : ENNReal) {K : Type uK} {V : Type uV} [Semiring K] [AddCommGroup V] [Module K V] (c : K) (x' : V) :
      (WithLp.equiv p V).symm (c x') = c (WithLp.equiv p V).symm x'
      @[simp]
      theorem WithLp.linearEquiv_symm_apply (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] :
      (WithLp.linearEquiv p K V).symm = (WithLp.equiv p V).symm
      @[simp]
      theorem WithLp.linearEquiv_apply (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] :
      (WithLp.linearEquiv p K V) = (WithLp.equiv p V)
      def WithLp.linearEquiv (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] :

      WithLp.equiv as a linear equivalence.

      Equations
      Instances For