Commit 2022-10-13 15:02 91b5bdde
View on Github →feat(analysis/normed_space/lp_equiv): equivalences between lp and pi_Lp, bounded_continuous_function (#15872)
This adds a new file for equivalences between various L^p spaces. We do this in a new file instead of analysis/normed_space/lp_space in order to minimize imports. We begin by establishing the equivalence between lp and pi_Lp when the index type is a fintype, and then proceed to recognize the equivalence between lp (for p = ∞) and bounded_continuous_function when the codomain has various algebraic structures.