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 α