Commit 2023-05-25 14:31 c8442dcb

View on Github →

feat: port MeasureTheory.Integral.MeanInequalities (#4337)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/MeanInequalities.lean

added theorem ENNReal.ae_eq_zero_of_lintegral_rpow_eq_zero

added def ENNReal.funMulInvSnorm

added theorem ENNReal.funMulInvSnorm_rpow

added theorem ENNReal.fun_eq_funMulInvSnorm_mul_snorm

added theorem ENNReal.lintegral_Lp_add_le

added theorem ENNReal.lintegral_Lp_add_le_of_le_one

added theorem ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr

added theorem ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero

added theorem ENNReal.lintegral_mul_le_Lp_mul_Lq

added theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top

added theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top

added theorem ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one

added theorem ENNReal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow

added theorem ENNReal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add

added theorem ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top

added theorem ENNReal.lintegral_rpow_funMulInvSnorm_eq_one

added theorem NNReal.lintegral_mul_le_Lp_mul_Lq