Commit 2021-06-29 12:50 54eccb0e
View on Github →feat(measure_theory/lp_space): add snorm_eq_lintegral_rpow_nnnorm (#8115)
Add two lemmas to go from snorm to integrals (through snorm'). The idea is that snorm' should then generally not be used, except in the construction of snorm.