Commit 2023-05-25 08:46 62d07763

View on Github →

feat: port Analysis.MeanInequalities (#4329)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/MeanInequalities.lean

added theorem ENNReal.Lp_add_le

added theorem ENNReal.inner_le_Lp_mul_Lq

added theorem ENNReal.rpow_sum_le_const_mul_sum_rpow

added theorem ENNReal.young_inequality

added theorem NNReal.Lp_add_le

added theorem NNReal.Lp_add_le_hasSum

added theorem NNReal.Lp_add_le_tsum'

added theorem NNReal.Lp_add_le_tsum

added theorem NNReal.geom_mean_le_arith_mean2_weighted

added theorem NNReal.geom_mean_le_arith_mean3_weighted

added theorem NNReal.geom_mean_le_arith_mean4_weighted

added theorem NNReal.geom_mean_le_arith_mean_weighted

added theorem NNReal.inner_le_Lp_mul_Lq

added theorem NNReal.inner_le_Lp_mul_Lq_hasSum

added theorem NNReal.inner_le_Lp_mul_Lq_tsum'

added theorem NNReal.inner_le_Lp_mul_Lq_tsum

added theorem NNReal.isGreatest_Lp

added theorem NNReal.rpow_sum_le_const_mul_sum_rpow

added theorem NNReal.summable_Lp_add

added theorem NNReal.summable_mul_of_Lp_Lq

added theorem NNReal.young_inequality

added theorem NNReal.young_inequality_real

added theorem Real.Lp_add_le

added theorem Real.Lp_add_le_hasSum_of_nonneg

added theorem Real.Lp_add_le_of_nonneg

added theorem Real.Lp_add_le_tsum_of_nonneg'

added theorem Real.Lp_add_le_tsum_of_nonneg

added theorem Real.arith_mean_weighted_of_constant

added theorem Real.geom_mean_eq_arith_mean_weighted_of_constant

added theorem Real.geom_mean_le_arith_mean2_weighted

added theorem Real.geom_mean_le_arith_mean3_weighted

added theorem Real.geom_mean_le_arith_mean4_weighted

added theorem Real.geom_mean_le_arith_mean_weighted

added theorem Real.geom_mean_weighted_of_constant

added theorem Real.inner_le_Lp_mul_Lq

added theorem Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg

added theorem Real.inner_le_Lp_mul_Lq_of_nonneg

added theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg'

added theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg

added theorem Real.rpow_sum_le_const_mul_sum_rpow

added theorem Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg

added theorem Real.summable_Lp_add_of_nonneg

added theorem Real.summable_mul_of_Lp_Lq_of_nonneg

added theorem Real.young_inequality

added theorem Real.young_inequality_of_nonneg