Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-12 11:43 5808afcb

View on Github →

feat(analysis/mean_inequalities): Holder and Minkowski inequalities (#3025)

Estimated changes

Modified src/analysis/mean_inequalities.lean

added theorem nnreal.Lp_add_le

deleted theorem nnreal.am_gm2_weighted

deleted theorem nnreal.am_gm3_weighted

deleted theorem nnreal.am_gm_weighted

added theorem nnreal.arith_mean_le_rpow_mean

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_mean_weighted

added theorem nnreal.inner_le_Lp_mul_Lq

added theorem nnreal.is_greatest_Lp

deleted theorem nnreal.pow_am_le_am_pow

added theorem nnreal.pow_arith_mean_le_arith_mean_pow

deleted theorem nnreal.rpow_am_le_am_rpow

added theorem nnreal.rpow_arith_mean_le_arith_mean_rpow

added theorem real.Lp_add_le

added theorem real.Lp_add_le_of_nonneg

deleted theorem real.am_gm2_weighted

deleted theorem real.am_gm_weighted

added theorem real.arith_mean_le_rpow_mean

deleted theorem real.fpow_am_le_am_fpow

added theorem real.fpow_arith_mean_le_arith_mean_fpow

added theorem real.geom_mean_le_arith_mean2_weighted

added theorem real.geom_mean_le_arith_mean_weighted

added theorem real.inner_le_Lp_mul_Lq

added theorem real.inner_le_Lp_mul_Lq_of_nonneg

deleted theorem real.pow_am_le_am_pow

deleted theorem real.pow_am_le_am_pow_of_even

added theorem real.pow_arith_mean_le_arith_mean_pow

added theorem real.pow_arith_mean_le_arith_mean_pow_of_even

deleted theorem real.rpow_am_le_am_rpow

added theorem real.rpow_arith_mean_le_arith_mean_rpow