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?

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

• toLp :: (
• ofLp : V

  Converts an element of WithLp p V to an element of V.

• )

def WithLp.delabToLp : Lean.PrettyPrinter.Delaborator.Delab

This prevents toLp p x being printed as { ofLp := x } by delabStructureInstance.

Equations

• WithLp.delabToLp = Lean.PrettyPrinter.Delaborator.delabApp

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

WithLp.ofLp and WithLp.toLp as an equivalence.

Equations

• WithLp.equiv p V = { toFun := WithLp.ofLp, invFun := WithLp.toLp p, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem WithLp.equiv_symm_apply_ofLp (p : ENNReal) (V : Type uV) (ofLp : V) : ((WithLp.equiv p V).symm ofLp).ofLp = ofLp

@[simp]

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

@[simp]

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

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)

Equations

• WithLp.instUnique p V = (WithLp.equiv p V).unique

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

Equations

• WithLp.instDecidableEq p V = (WithLp.equiv p V).decidableEq

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

Equations

• WithLp.instAddCommGroup p V = (WithLp.equiv p V).addCommGroup

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

Equations

• WithLp.instSMul p K V = Equiv.smul K (WithLp.equiv p V)

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

Equations

• WithLp.instVAdd p K V = Equiv.vadd K (WithLp.equiv p V)

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

Equations

• WithLp.instMulAction p K V = { toSMul := WithLp.instSMul p K V, one_smul := ⋯, mul_smul := ⋯ }

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

Equations

• WithLp.instAddAction p K V = { toVAdd := WithLp.instVAdd p K V, zero_vadd := ⋯, add_vadd := ⋯ }

instance WithLp.instDistribMulAction (p : ENNReal) (K : Type uK) (V : Type uV) [Monoid K] [AddCommGroup V] [DistribMulAction K V] : DistribMulAction K (WithLp p V)

Equations

• WithLp.instDistribMulAction p K V = { toMulAction := WithLp.instMulAction p K V, smul_zero := ⋯, smul_add := ⋯ }

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

Equations

• WithLp.instModule p K V = { toDistribMulAction := WithLp.instDistribMulAction p K V, add_smul := ⋯, zero_smul := ⋯ }

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)

theorem WithLp.ofLp_injective (p : ENNReal) {V : Type uV} : Function.Injective ofLp

theorem WithLp.toLp_injective (p : ENNReal) {V : Type uV} : Function.Injective (toLp p)

theorem WithLp.ofLp_bijective (p : ENNReal) {V : Type uV} : Function.Bijective ofLp

theorem WithLp.toLp_bijective (p : ENNReal) {V : Type uV} : Function.Bijective (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

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)

@[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.

Equations

• WithLp.linearEquiv p K V = { toFun := WithLp.ofLp, map_add' := ⋯, map_smul' := ⋯, invFun := WithLp.toLp p, left_inv := ⋯, right_inv := ⋯ }

@[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

@[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

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)