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

• WithLp p V: a copy of V to be equipped with an Lp norm.
• WithLp.equiv p V: the canonical equivalence between WithLp p V and V.
• WithLp.linearEquiv p K V: the canonical K-module isomorphism between WithLp p V and V.

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).

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.

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

instance WithLp.instAddCommGroup (p : ENNReal) (V : Type uV) [AddCommGroup V] : AddCommGroup (WithLp p V)

instance WithLp.instModule (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] : Module K (WithLp p V)

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] : IsScalarTower K K' (WithLp p V)

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] : SMulCommClass K K' (WithLp p V)

instance WithLp.instModuleFinite (p : ENNReal) (K : Type uK) (V : Type uV) [Semiring K] [AddCommGroup V] [Module K V] [Module.Finite K V] : Module.Finite K (WithLp p V)

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] : ↑(LinearEquiv.symm (WithLp.linearEquiv p K V)) = ↑(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 p V ≃ₗ[K] V

WithLp.equiv as a linear equivalence.