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 u_1) : Type u_1

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 u_4) : 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_apply (p : ENNReal) (V : Type u_4) (self : WithLp p V) : (WithLp.equiv p V) self = self.ofLp

@[simp]

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

@[simp]

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

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance WithLp.instSMul (p : ENNReal) (K : Type u_1) (V : Type u_4) [SMul K V] : SMul K (WithLp p V)

Equations

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

@[implicit_reducible]

instance WithLp.instVAdd (p : ENNReal) (K : Type u_1) (V : Type u_4) [VAdd K V] : VAdd K (WithLp p V)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance WithLp.instDistribMulAction (p : ENNReal) (K : Type u_1) (V : Type u_4) [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 := ⋯ }

@[implicit_reducible]

instance WithLp.instModule (p : ENNReal) (K : Type u_1) (V : Type u_4) [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 u_4} (x : V) : (toLp p x).ofLp = x

@[simp]

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

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

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

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

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

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

theorem WithLp.toLp_bijective (p : ENNReal) {V : Type u_4} : Function.Bijective (toLp p)

def WithLp.map (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V → V') (x : WithLp p V) : WithLp p V'

Lift a function to WithLp.

Equations

• WithLp.map p f x = WithLp.toLp p (f x.ofLp)

@[simp]

theorem WithLp.map_id (p : ENNReal) {V : Type u_4} : WithLp.map p id = id

theorem WithLp.map_comp (p : ENNReal) {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} (f : V' → V'') (g : V → V') : WithLp.map p (f ∘ g) = WithLp.map p f ∘ WithLp.map p g

def WithLp.congr (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V ≃ V') : WithLp p V ≃ WithLp p V'

Lift an equivalence to WithLp.

Equations

• WithLp.congr p f = (WithLp.equiv p V).trans (f.trans (WithLp.equiv p V').symm)

@[simp]

theorem WithLp.coe_congr (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V ≃ V') : ⇑(WithLp.congr p f) = WithLp.map p ⇑f

@[simp]

theorem WithLp.congr_refl (p : ENNReal) {V : Type u_4} : WithLp.congr p (Equiv.refl V) = Equiv.refl (WithLp p V)

@[simp]

theorem WithLp.congr_symm (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V ≃ V') : (WithLp.congr p f).symm = WithLp.congr p f.symm

theorem WithLp.congr_trans (p : ENNReal) {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} (f : V ≃ V') (g : V' ≃ V'') : WithLp.congr p (f.trans g) = (WithLp.congr p f).trans (WithLp.congr p g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance WithLp.instIsScalarTower (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [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 u_1} (K' : Type u_2) {V : Type u_4} [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 u_1} (K' : Type u_2) {V : Type u_4} [SMul K V] [SMul K' V] [SMulCommClass K K' V] : SMulCommClass K K' (WithLp p V)

instance WithLp.instVAddCommClass (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [VAdd K V] [VAdd K' V] [VAddCommClass K K' V] : VAddCommClass K K' (WithLp p V)

def WithLp.addEquiv (p : ENNReal) (V : Type u_4) [AddCommGroup V] : WithLp p V ≃+ V

WithLp.equiv as a group isomorphism.

Equations

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

@[simp]

theorem WithLp.addEquiv_apply (p : ENNReal) (V : Type u_4) [AddCommGroup V] (self : WithLp p V) : (WithLp.addEquiv p V) self = self.ofLp

@[simp]

theorem WithLp.addEquiv_symm_apply (p : ENNReal) (V : Type u_4) [AddCommGroup V] (ofLp : V) : (WithLp.addEquiv p V).symm ofLp = toLp p ofLp

theorem WithLp.coe_addEquiv (p : ENNReal) (V : Type u_4) [AddCommGroup V] : ⇑(WithLp.addEquiv p V) = ofLp

theorem WithLp.coe_symm_addEquiv (p : ENNReal) (V : Type u_4) [AddCommGroup V] : ⇑(WithLp.addEquiv p V).symm = toLp p

@[simp]

theorem WithLp.ofLp_sum (p : ENNReal) (V : Type u_4) [AddCommGroup V] {ι : Type u_7} (s : Finset ι) (f : ι → WithLp p V) : (∑ i ∈ s, f i).ofLp = ∑ i ∈ s, (f i).ofLp

@[simp]

theorem WithLp.toLp_sum (p : ENNReal) (V : Type u_4) [AddCommGroup V] {ι : Type u_7} (s : Finset ι) (f : ι → V) : toLp p (∑ i ∈ s, f i) = ∑ i ∈ s, toLp p (f i)

@[simp]

theorem WithLp.ofLp_listSum (p : ENNReal) (V : Type u_4) [AddCommGroup V] (l : List (WithLp p V)) : l.sum.ofLp = (List.map ofLp l).sum

@[simp]

theorem WithLp.toLp_listSum (p : ENNReal) (V : Type u_4) [AddCommGroup V] (l : List V) : toLp p l.sum = (List.map (toLp p) l).sum

@[simp]

theorem WithLp.ofLp_multisetSum (p : ENNReal) (V : Type u_4) [AddCommGroup V] (s : Multiset (WithLp p V)) : s.sum.ofLp = (Multiset.map ofLp s).sum

@[simp]

theorem WithLp.toLp_multisetSum (p : ENNReal) (V : Type u_4) [AddCommGroup V] (s : Multiset V) : toLp p s.sum = (Multiset.map (toLp p) s).sum

def WithLp.linearEquiv (p : ENNReal) (K : Type u_1) (V : Type u_4) [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.addEquiv p V).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (WithLp.addEquiv p V).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem WithLp.linearEquiv_symm_apply (p : ENNReal) (K : Type u_1) (V : Type u_4) [Semiring K] [AddCommGroup V] [Module K V] (a✝ : V) : (WithLp.linearEquiv p K V).symm a✝ = (WithLp.addEquiv p V).invFun a✝

@[simp]

theorem WithLp.linearEquiv_apply (p : ENNReal) (K : Type u_1) (V : Type u_4) [Semiring K] [AddCommGroup V] [Module K V] (a✝ : WithLp p V) : (WithLp.linearEquiv p K V) a✝ = (WithLp.addEquiv p V).toFun a✝

theorem WithLp.coe_linearEquiv (p : ENNReal) (K : Type u_1) (V : Type u_4) [Semiring K] [AddCommGroup V] [Module K V] : ⇑(WithLp.linearEquiv p K V) = ofLp

theorem WithLp.coe_symm_linearEquiv (p : ENNReal) (K : Type u_1) (V : Type u_4) [Semiring K] [AddCommGroup V] [Module K V] : ⇑(WithLp.linearEquiv p K V).symm = toLp p

@[simp]

theorem WithLp.toAddEquiv_linearEquiv (p : ENNReal) (K : Type u_1) (V : Type u_4) [Semiring K] [AddCommGroup V] [Module K V] : (WithLp.linearEquiv p K V).toAddEquiv = WithLp.addEquiv p V

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

def LinearMap.withLpMap (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [Semiring K] [Semiring K'] {σ : K →+* K'} [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] (f : V →ₛₗ[σ] V') : WithLp p V →ₛₗ[σ] WithLp p V'

Lift a (semi)linear map to WithLp.

Equations

• LinearMap.withLpMap p f = ↑(WithLp.linearEquiv p K' V').symm ∘ₛₗ f ∘ₛₗ ↑(WithLp.linearEquiv p K V)

@[simp]

theorem LinearMap.coe_withLpMap (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [Semiring K] [Semiring K'] {σ : K →+* K'} [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] (f : V →ₛₗ[σ] V') : ⇑(withLpMap p f) = WithLp.map p ⇑f

@[simp]

theorem LinearMap.withLpMap_id (p : ENNReal) {K : Type u_1} {V : Type u_4} [Semiring K] [AddCommGroup V] [Module K V] : withLpMap p id = id

@[simp]

theorem LinearMap.withLpMap_comp (p : ENNReal) {K : Type u_1} {K' : Type u_2} {K'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [Semiring K] [Semiring K'] [Semiring K''] {σ : K →+* K'} {τ : K' →+* K''} {ρ : K →+* K''} [RingHomCompTriple σ τ ρ] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] [AddCommGroup V''] [Module K'' V''] (f : V' →ₛₗ[τ] V'') (g : V →ₛₗ[σ] V') : withLpMap p (f ∘ₛₗ g) = withLpMap p f ∘ₛₗ withLpMap p g

def LinearEquiv.withLpCongr (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [Semiring K] [Semiring K'] {σ : K →+* K'} {σ' : K' →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] (f : V ≃ₛₗ[σ] V') : WithLp p V ≃ₛₗ[σ] WithLp p V'

Lift a (semi)linear equivalence to WithLp.

Equations

• LinearEquiv.withLpCongr p f = (WithLp.linearEquiv p K V).trans (f.trans (WithLp.linearEquiv p K' V').symm)

@[simp]

theorem LinearEquiv.coe_withLpCongr (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [Semiring K] [Semiring K'] {σ : K →+* K'} {σ' : K' →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] (f : V ≃ₛₗ[σ] V') : ⇑(withLpCongr p f) = WithLp.map p ⇑f

@[simp]

theorem LinearEquiv.withLpCongr_symm (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [Semiring K] [Semiring K'] {σ : K →+* K'} {σ' : K' →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] (f : V ≃ₛₗ[σ] V') : (withLpCongr p f).symm = withLpCongr p f.symm

@[simp]

theorem LinearEquiv.withLpCongr_refl (p : ENNReal) {K : Type u_1} {V : Type u_4} [Semiring K] [AddCommGroup V] [Module K V] : withLpCongr p (refl K V) = refl K (WithLp p V)

theorem LinearEquiv.withLpCongr_trans (p : ENNReal) {K : Type u_1} {K' : Type u_2} {K'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [Semiring K] [Semiring K'] [Semiring K''] {σ : K →+* K'} {σ' : K' →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {τ : K' →+* K''} {τ' : K'' →+* K'} [RingHomInvPair τ τ'] [RingHomInvPair τ' τ] {ρ : K →+* K''} {ρ' : K'' →+* K} [RingHomInvPair ρ ρ'] [RingHomInvPair ρ' ρ] [RingHomCompTriple σ τ ρ] [RingHomCompTriple τ' σ' ρ'] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K' V'] [AddCommGroup V''] [Module K'' V''] (f : V ≃ₛₗ[σ] V') (g : V' ≃ₛₗ[τ] V'') : withLpCongr p (f.trans g) = (withLpCongr p f).trans (withLpCongr p g)