Equivalences among $L^p$ spaces

In this file we collect a variety of equivalences among various $L^p$ spaces. In particular, when α is a Fintype, given E : α → Type u and p : ℝ≥0∞, there is a natural linear isometric equivalence lpPiLpₗᵢₓ : lp E p ≃ₗᵢ PiLp p E. In addition, when α is a discrete topological space, the bounded continuous functions α →ᵇ β correspond exactly to lp (fun _ ↦ β) ∞. Here there can be more structure, including ring and algebra structures, and we implement these equivalences accordingly as well.

We keep this as a separate file so that the various $L^p$ space files don't import the others.

Recall that PiLp is just a type synonym for Π i, E i but given a different metric and norm structure, although the topological, uniform and bornological structures coincide definitionally. These structures are only defined on PiLp for Fintype α, so there are no issues of convergence to consider.

While PreLp is also a type synonym for Π i, E i, it allows for infinite index types. On this type there is a predicate Memℓp which says that the relevant p-norm is finite and lp E p is the subtype of PreLp satisfying Memℓp.

TODO

• Equivalence between lp and MeasureTheory.Lp, for f : α → E (i.e., functions rather than pi-types) and the counting measure on α

theorem Memℓp.all {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] (f : (i : α) → E i) : Memℓp f p

When α is Finite, every f : PreLp E p satisfies Memℓp f p.

def Equiv.lpPiLp {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] : ↥(lp E p) ≃ PiLp p E

The canonical Equiv between lp E p ≃ PiLp p E when E : α → Type u with [Finite α].

Equations

• Equiv.lpPiLp = { toFun := fun (f : ↥(lp E p)) => ↑f, invFun := fun (f : PiLp p E) => ⟨f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem coe_equiv_lpPiLp {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] (f : ↥(lp E p)) : Equiv.lpPiLp f = ↑f

theorem coe_equiv_lpPiLp_symm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] (f : PiLp p E) : ↑(Equiv.lpPiLp.symm f) = f

def AddEquiv.lpPiLp {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] : ↥(lp E p) ≃+ PiLp p E

The canonical AddEquiv between lp E p and PiLp p E when E : α → Type u with [Fintype α].

Equations

• AddEquiv.lpPiLp = { toEquiv := Equiv.lpPiLp, map_add' := ⋯ }

theorem coe_addEquiv_lpPiLp {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] (f : ↥(lp E p)) : AddEquiv.lpPiLp f = ↑f

theorem coe_addEquiv_lpPiLp_symm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Finite α] (f : PiLp p E) : ↑(AddEquiv.lpPiLp.symm f) = f

theorem equiv_lpPiLp_norm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Fintype α] (f : ↥(lp E p)) : ‖Equiv.lpPiLp f‖ = ‖f‖

noncomputable def lpPiLpₗᵢ {α : Type u_1} (E : α → Type u_2) [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Fintype α] (𝕜 : Type u_3) [NontriviallyNormedField 𝕜] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 ≤ p)] : ↥(lp E p) ≃ₗᵢ[𝕜] PiLp p E

The canonical LinearIsometryEquiv between lp E p and PiLp p E when E : α → Type u with [Fintype α] and [Fact (1 ≤ p)].

Equations

• lpPiLpₗᵢ E 𝕜 = { toFun := AddEquiv.lpPiLp.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.lpPiLp.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

theorem coe_lpPiLpₗᵢ {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Fintype α] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 ≤ p)] (f : ↥(lp E p)) : (lpPiLpₗᵢ E 𝕜) f = ↑f

theorem coe_lpPiLpₗᵢ_symm {α : Type u_1} {E : α → Type u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [Fintype α] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 ≤ p)] (f : PiLp p E) : ↑((lpPiLpₗᵢ E 𝕜).symm f) = f

noncomputable def AddEquiv.lpBCF {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [DiscreteTopology α] [NormedAddCommGroup E] : ↥(lp (fun (x : α) => E) ⊤) ≃+ BoundedContinuousFunction α E

The canonical map between lp (fun _ : α ↦ E) ∞ and α →ᵇ E as an AddEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem coe_addEquiv_lpBCF {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [DiscreteTopology α] [NormedAddCommGroup E] (f : ↥(lp (fun (x : α) => E) ⊤)) : ⇑(AddEquiv.lpBCF f) = ↑f

theorem coe_addEquiv_lpBCF_symm {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [DiscreteTopology α] [NormedAddCommGroup E] (f : BoundedContinuousFunction α E) : ↑(AddEquiv.lpBCF.symm f) = ⇑f

noncomputable def lpBCFₗᵢ {α : Type u_1} (E : Type u_2) (𝕜 : Type u_5) [TopologicalSpace α] [DiscreteTopology α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ↥(lp (fun (x : α) => E) ⊤) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E

The canonical map between lp (fun _ : α ↦ E) ∞ and α →ᵇ E as a LinearIsometryEquiv.

Equations

• lpBCFₗᵢ E 𝕜 = { toFun := AddEquiv.lpBCF.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.lpBCF.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

theorem coe_lpBCFₗᵢ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [TopologicalSpace α] [DiscreteTopology α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : ↥(lp (fun (x : α) => E) ⊤)) : ⇑((lpBCFₗᵢ E 𝕜) f) = ↑f

theorem coe_lpBCFₗᵢ_symm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [TopologicalSpace α] [DiscreteTopology α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : BoundedContinuousFunction α E) : ↑((lpBCFₗᵢ E 𝕜).symm f) = ⇑f

noncomputable def RingEquiv.lpBCF {α : Type u_1} (R : Type u_3) [TopologicalSpace α] [DiscreteTopology α] [NonUnitalNormedRing R] : ↥(lp (fun (x : α) => R) ⊤) ≃+* BoundedContinuousFunction α R

The canonical map between lp (fun _ : α ↦ R) ∞ and α →ᵇ R as a RingEquiv.

Equations

• RingEquiv.lpBCF R = { toEquiv := AddEquiv.lpBCF.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

theorem coe_ringEquiv_lpBCF {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [DiscreteTopology α] [NonUnitalNormedRing R] (f : ↥(lp (fun (x : α) => R) ⊤)) : ⇑((RingEquiv.lpBCF R) f) = ↑f

theorem coe_ringEquiv_lpBCF_symm {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [DiscreteTopology α] [NonUnitalNormedRing R] (f : BoundedContinuousFunction α R) : ↑((RingEquiv.lpBCF R).symm f) = ⇑f

noncomputable def AlgEquiv.lpBCF (α : Type u_1) (A : Type u_4) (𝕜 : Type u_5) [TopologicalSpace α] [DiscreteTopology α] [NormedRing A] [NormOneClass A] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 A] : ↥(lp (fun (x : α) => A) ⊤) ≃ₐ[𝕜] BoundedContinuousFunction α A

The canonical map between lp (fun _ : α ↦ A) ∞ and α →ᵇ A as an AlgEquiv.

Equations

• AlgEquiv.lpBCF α A 𝕜 = { toEquiv := (RingEquiv.lpBCF A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem coe_algEquiv_lpBCF {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [TopologicalSpace α] [DiscreteTopology α] [NormedRing A] [NormOneClass A] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 A] (f : ↥(lp (fun (x : α) => A) ⊤)) : ⇑((AlgEquiv.lpBCF α A 𝕜) f) = ↑f

theorem coe_algEquiv_lpBCF_symm {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [TopologicalSpace α] [DiscreteTopology α] [NormedRing A] [NormOneClass A] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 A] (f : BoundedContinuousFunction α A) : ↑((AlgEquiv.lpBCF α A 𝕜).symm f) = ⇑f