mathlib3 documentation

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 #

theorem mem_ℓp.all {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [finite α] (f : Π (i : α), E i) :

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 : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] :
(lp E p) pi_Lp 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 : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] (f : (lp E p)) :
theorem coe_equiv_lp_pi_Lp_symm {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] (f : pi_Lp p E) :
theorem equiv_lp_pi_Lp_norm {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] (f : (lp E p)) :
def add_equiv.lp_pi_Lp {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] [fact (1 p)] :
(lp E p) ≃+ pi_Lp 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 : α), normed_add_comm_group (E 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 : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] [fact (1 p)] (f : pi_Lp p E) :
noncomputable def lp_pi_Lpₗᵢ {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] (𝕜 : Type u_3) [nontrivially_normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] [fact (1 p)] :
(lp E p) ≃ₗᵢ[𝕜] pi_Lp 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 : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] {𝕜 : Type u_3} [nontrivially_normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] [fact (1 p)] (f : (lp E p)) :
theorem coe_lp_pi_Lpₗᵢ_symm {α : Type u_1} {E : α Type u_2} [Π (i : α), normed_add_comm_group (E i)] {p : ennreal} [fintype α] {𝕜 : Type u_3} [nontrivially_normed_field 𝕜] [Π (i : α), normed_space 𝕜 (E i)] [fact (1 p)] (f : pi_Lp p E) :
(((lp_pi_Lpₗᵢ 𝕜).symm) f) = f
noncomputable def add_equiv.lp_bcf {α : Type u_1} {E : Type u_2} [topological_space α] [discrete_topology α] [normed_add_comm_group E] :
(lp (λ (_x : α), E) ) ≃+ bounded_continuous_function α 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} [topological_space α] [discrete_topology α] [normed_add_comm_group E] (f : (lp (λ (_x : α), E) )) :
noncomputable def lp_bcfₗᵢ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_5) [topological_space α] [discrete_topology α] [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :
(lp (λ (_x : α), E) ) ≃ₗᵢ[𝕜] bounded_continuous_function α 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} [topological_space α] [discrete_topology α] [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] (f : (lp (λ (_x : α), E) )) :
noncomputable def ring_equiv.lp_bcf {α : Type u_1} (R : Type u_3) [topological_space α] [discrete_topology α] [non_unital_normed_ring R] :
(lp (λ (_x : α), R) ) ≃+* bounded_continuous_function α 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} [topological_space α] [discrete_topology α] [non_unital_normed_ring R] (f : (lp (λ (_x : α), R) )) :
noncomputable def alg_equiv.lp_bcf (α : Type u_1) (A : Type u_4) (𝕜 : Type u_5) [topological_space α] [discrete_topology α] [normed_ring A] [norm_one_class A] [nontrivially_normed_field 𝕜] [normed_algebra 𝕜 A] :
(lp (λ (_x : α), A) ) ≃ₐ[𝕜] bounded_continuous_function α 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} [topological_space α] [discrete_topology α] [normed_ring A] [norm_one_class A] [nontrivially_normed_field 𝕜] [normed_algebra 𝕜 A] (f : (lp (λ (_x : α), A) )) :
((alg_equiv.lp_bcf α A 𝕜) f) = f