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,
α is a
E : α → Type u and
p : ℝ≥0∞, there is a natural linear isometric
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.
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
fintype α, so there are no issues of convergence
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