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.toLp: the canonical inclusion from V to WithLp p V.
• WithLp.ofLp: the canonical inclusion from WithLp p V to 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.toLp (p : ENNReal) {V : Type uV} : V → WithLp p V

The canonical inclusion of V into WithLp p V.

def WithLp.ofLp {p : ENNReal} {V : Type uV} : WithLp p V → V

The canonical inclusion of WithLp p V into V.

def WithLp.equiv (p : ENNReal) (V : Type uV) : WithLp p V ≃ V

WithLp.ofLp and WithLp.toLp as an equivalence.

@[simp]

theorem WithLp.equiv_apply (p : ENNReal) (V : Type uV) (a✝ : WithLp p V) : (WithLp.equiv p V) a✝ = a✝.ofLp

@[simp]

theorem WithLp.equiv_symm_apply (p : ENNReal) (V : Type uV) (a✝ : V) : (WithLp.equiv p V).symm a✝ = toLp p a✝

def WithLp.rec (p : ENNReal) (V : Type uV) {motive : WithLp p V → Sort u_1} (toLp : (v : V) → motive (toLp p v)) (v : WithLp p V) : motive v

A recursor for WithLp p V, that reduces to the underlying space V.

This unfortunately cannot be registered with cases_eliminator, but it can still be used as cases v using WithLp.rec with | toLp v =>.

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

instance WithLp.instNontrivial (p : ENNReal) (V : Type uV) [Nontrivial V] : Nontrivial (WithLp p V)

instance WithLp.instUnique (p : ENNReal) (V : Type uV) [Unique V] : Unique (WithLp p V)

instance WithLp.instDecidableEq (p : ENNReal) (V : Type uV) [DecidableEq V] : DecidableEq (WithLp p V)

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

instance WithLp.instSMul (p : ENNReal) (K : Type uK) (V : Type uV) [SMul K V] : SMul K (WithLp p V)

instance WithLp.instVAdd (p : ENNReal) (K : Type uK) (V : Type uV) [VAdd K V] : VAdd K (WithLp p V)

instance WithLp.instMulAction (K : Type uK) (V : Type uV) [Monoid K] [MulAction K V] : MulAction K V

instance WithLp.instAddAction (K : Type uK) (V : Type uV) [AddMonoid K] [AddAction K V] : AddAction K V

instance WithLp.instDistribMulAction (p : ENNReal) (K : Type uK) (V : Type uV) [Monoid K] [AddCommGroup V] [DistribMulAction K V] : DistribMulAction K (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) [SMul K K'] [SMul K V] [SMul K' V] [IsScalarTower K K' V] : IsScalarTower K K' (WithLp p V)

instance WithLp.instVAddAssocClass (p : ENNReal) (K : Type uK) (K' : Type uK') (V : Type uV) [VAdd K K'] [VAdd K V] [VAdd K' V] [VAddAssocClass K K' V] : VAddAssocClass K K' (WithLp p V)

instance WithLp.instSMulCommClass (p : ENNReal) (K : Type uK) (K' : Type uK') (V : Type uV) [SMul K V] [SMul K' V] [SMulCommClass K K' V] : SMulCommClass K K' (WithLp p V)

instance WithLp.instVAddCommClass (p : ENNReal) (K : Type uK) (K' : Type uK') (V : Type uV) [VAdd K V] [VAdd K' V] [VAddCommClass K K' V] : VAddCommClass 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)

@[simp]

theorem WithLp.ofLp_toLp (p : ENNReal) {V : Type uV} (x : V) : (toLp p x).ofLp = x

@[simp]

theorem WithLp.toLp_ofLp (p : ENNReal) {V : Type uV} (x : WithLp p V) : toLp p x.ofLp = x

theorem WithLp.ofLp_surjective (p : ENNReal) {V : Type uV} : Function.Surjective ofLp

theorem WithLp.toLp_surjective (p : ENNReal) {V : Type uV} : Function.Surjective (toLp p)

@[simp]

theorem WithLp.toLp_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] : toLp p 0 = 0

@[simp]

theorem WithLp.ofLp_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] : ofLp 0 = 0

@[simp]

theorem WithLp.toLp_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : V) : toLp p (x + y) = toLp p x + toLp p y

@[simp]

theorem WithLp.ofLp_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : WithLp p V) : (x + y).ofLp = x.ofLp + y.ofLp

@[simp]

theorem WithLp.toLp_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : V) : toLp p (x - y) = toLp p x - toLp p y

@[simp]

theorem WithLp.ofLp_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : WithLp p V) : (x - y).ofLp = x.ofLp - y.ofLp

@[simp]

theorem WithLp.toLp_neg (p : ENNReal) {V : Type uV} [AddCommGroup V] (x : V) : toLp p (-x) = -toLp p x

@[simp]

theorem WithLp.ofLp_neg (p : ENNReal) {V : Type uV} [AddCommGroup V] (x : WithLp p V) : (-x).ofLp = -x.ofLp

@[simp]

theorem WithLp.toLp_eq_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] {x : V} : toLp p x = 0 ↔ x = 0

@[simp]

theorem WithLp.ofLp_eq_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] {x : WithLp p V} : x.ofLp = 0 ↔ x = 0

@[simp]

theorem WithLp.toLp_smul (p : ENNReal) {K : Type uK} {V : Type uV} [SMul K V] (c : K) (x : V) : toLp p (c • x) = c • toLp p x

@[simp]

theorem WithLp.ofLp_smul (p : ENNReal) {K : Type uK} {V : Type uV} [SMul K V] (c : K) (x : WithLp p V) : (c • x).ofLp = c • x.ofLp

@[deprecated WithLp.ofLp_zero (since := "2025-06-08")]

theorem WithLp.equiv_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] : (WithLp.equiv p V) 0 = 0

@[deprecated WithLp.toLp_zero (since := "2025-06-08")]

theorem WithLp.equiv_symm_zero (p : ENNReal) {V : Type uV} [AddCommGroup V] : (WithLp.equiv p V).symm 0 = 0

@[deprecated WithLp.toLp_eq_zero (since := "2025-06-08")]

theorem WithLp.equiv_symm_eq_zero_iff (p : ENNReal) {V : Type uV} [AddCommGroup V] {x : V} : (WithLp.equiv p V).symm x = 0 ↔ x = 0

@[deprecated WithLp.ofLp_eq_zero (since := "2025-06-08")]

theorem WithLp.equiv_eq_zero_iff (p : ENNReal) {V : Type uV} [AddCommGroup V] {x : WithLp p V} : (WithLp.equiv p V) x = 0 ↔ x = 0

@[deprecated WithLp.ofLp_add (since := "2025-06-08")]

theorem WithLp.equiv_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : WithLp p V) : (WithLp.equiv p V) (x + y) = (WithLp.equiv p V) x + (WithLp.equiv p V) y

@[deprecated WithLp.toLp_add (since := "2025-06-08")]

theorem WithLp.equiv_symm_add (p : ENNReal) {V : Type uV} [AddCommGroup V] (x' y' : V) : (WithLp.equiv p V).symm (x' + y') = (WithLp.equiv p V).symm x' + (WithLp.equiv p V).symm y'

@[deprecated WithLp.ofLp_sub (since := "2025-06-08")]

theorem WithLp.equiv_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x y : WithLp p V) : (WithLp.equiv p V) (x - y) = (WithLp.equiv p V) x - (WithLp.equiv p V) y

@[deprecated WithLp.toLp_sub (since := "2025-06-08")]

theorem WithLp.equiv_symm_sub (p : ENNReal) {V : Type uV} [AddCommGroup V] (x' y' : V) : (WithLp.equiv p V).symm (x' - y') = (WithLp.equiv p V).symm x' - (WithLp.equiv p V).symm y'

@[deprecated WithLp.ofLp_neg (since := "2025-06-08")]

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

@[deprecated WithLp.toLp_neg (since := "2025-06-08")]

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'

@[deprecated WithLp.ofLp_smul (since := "2025-06-08")]

theorem WithLp.equiv_smul (p : ENNReal) {K : Type uK} {V : Type uV} [SMul K V] (c : K) (x : WithLp p V) : (WithLp.equiv p V) (c • x) = c • (WithLp.equiv p V) x

@[deprecated WithLp.toLp_smul (since := "2025-06-08")]

theorem WithLp.equiv_symm_smul (p : ENNReal) {K : Type uK} {V : Type uV} [SMul K V] (c : K) (x' : V) : (WithLp.equiv p V).symm (c • x') = c • (WithLp.equiv p V).symm x'

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.

@[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) = ofLp

@[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 = toLp p