Theorem ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_one
Modification history
2021-06-19 15:31
src/analysis/mean_inequalities.lean
chore(analysis/mean_inequalities): split integral mean inequalities to a new file (#7990) …
Modified ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_oneView on Github →