# mathlib3documentation

analysis.normed_space.lp_equiv

# Equivalences among $L^p$ spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 lp_pi_Lpₗᵢ : lp E p ≃ₗᵢ pi_Lp p E. In addition, when α is a discrete topological space, the bounded continuous functions α →ᵇ β correspond exactly to lp (λ _, β) ∞. 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 pi_Lp 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 pi_Lp for fintype α, so there are no issues of convergence to consider.

While pre_lp 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 pre_lp satisfying mem_ℓp.

## TODO #

• Equivalence between lp and measure_theory.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 : α), ] {p : ennreal} [finite α] (f : Π (i : α), E i) :
p

When α is finite, every f : pre_lp E p satisfies mem_ℓp f p.

def equiv.lp_pi_Lp {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] :
(lp E p) E

The canonical equiv between lp E p ≃ pi_Lp p E when E : α → Type u with [fintype α].

Equations
theorem coe_equiv_lp_pi_Lp {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] (f : (lp E p)) :
theorem coe_equiv_lp_pi_Lp_symm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] (f : E) :
theorem equiv_lp_pi_Lp_norm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] (f : (lp E p)) :
def add_equiv.lp_pi_Lp {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] [fact (1 p)] :
(lp E p) ≃+ E

The canonical add_equiv between lp E p and pi_Lp p E when E : α → Type u with [fintype α] and [fact (1 ≤ p)].

Equations
theorem coe_add_equiv_lp_pi_Lp {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] [fact (1 p)] (f : (lp E p)) :
theorem coe_add_equiv_lp_pi_Lp_symm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] [fact (1 p)] (f : E) :
noncomputable def lp_pi_Lpₗᵢ {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] (𝕜 : Type u_3) [Π (i : α), (E i)] [fact (1 p)] :
(lp E p) ≃ₗᵢ[𝕜] E

The canonical linear_isometry_equiv between lp E p and pi_Lp p E when E : α → Type u with [fintype α] and [fact (1 ≤ p)].

Equations
theorem coe_lp_pi_Lpₗᵢ {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] {𝕜 : Type u_3} [Π (i : α), (E i)] [fact (1 p)] (f : (lp E p)) :
theorem coe_lp_pi_Lpₗᵢ_symm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p : ennreal} [fintype α] {𝕜 : Type u_3} [Π (i : α), (E i)] [fact (1 p)] (f : E) :
(((lp_pi_Lpₗᵢ 𝕜).symm) f) = f
noncomputable def add_equiv.lp_bcf {α : Type u_1} {E : Type u_2}  :
(lp (λ (_x : α), E) ) ≃+

The canonical map between lp (λ (_ : α), E) ∞ and α →ᵇ E as an add_equiv.

Equations
theorem coe_add_equiv_lp_bcf {α : Type u_1} {E : Type u_2} (f : (lp (λ (_x : α), E) )) :
= f
theorem coe_add_equiv_lp_bcf_symm {α : Type u_1} {E : Type u_2} (f : E) :
noncomputable def lp_bcfₗᵢ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_5) [ E] :
(lp (λ (_x : α), E) ) ≃ₗᵢ[𝕜]

The canonical map between lp (λ (_ : α), E) ∞ and α →ᵇ E as a linear_isometry_equiv.

Equations
theorem coe_lp_bcfₗᵢ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [ E] (f : (lp (λ (_x : α), E) )) :
theorem coe_lp_bcfₗᵢ_symm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [ E] (f : E) :
noncomputable def ring_equiv.lp_bcf {α : Type u_1} (R : Type u_3)  :
(lp (λ (_x : α), R) ) ≃+*

The canonical map between lp (λ (_ : α), R) ∞ and α →ᵇ R as a ring_equiv.

Equations
theorem coe_ring_equiv_lp_bcf {α : Type u_1} {R : Type u_3} (f : (lp (λ (_x : α), R) )) :
( f) = f
theorem coe_ring_equiv_lp_bcf_symm {α : Type u_1} {R : Type u_3} (f : R) :
noncomputable def alg_equiv.lp_bcf (α : Type u_1) (A : Type u_4) (𝕜 : Type u_5) [normed_ring A] [ A] :
(lp (λ (_x : α), A) ) ≃ₐ[𝕜]

The canonical map between lp (λ (_ : α), A) ∞ and α →ᵇ A as an alg_equiv.

Equations
theorem coe_alg_equiv_lp_bcf {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [normed_ring A] [ A] (f : (lp (λ (_x : α), A) )) :
( A 𝕜) f) = f
theorem coe_alg_equiv_lp_bcf_symm {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [normed_ring A] [ A] (f : A) :
( A 𝕜).symm) f) = f