Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-19 23:20 2d6556dd

View on Github →

feat(analysis/mean_inequalities) : Prove AM-GM (#1836)

  • feat(analysis/mean_inequalities) : Prove AM-GM
  • Update, add more inequalities
  • Update src/analysis/convex/specific_functions.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Update src/analysis/mean_inequalities.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Update src/analysis/mean_inequalities.lean
  • Small fixes, thanks @sgouezel
  • Update src/analysis/mean_inequalities.lean Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

added theorem deriv_fpow
added theorem deriv_within_fpow
added theorem differentiable_at_fpow
added theorem differentiable_on_fpow
added theorem has_deriv_at_fpow
added theorem iter_deriv_fpow
added theorem iter_deriv_pow'
added theorem iter_deriv_pow
added theorem convex_on_exp
added theorem convex_on_fpow
added theorem convex_on_pow
added theorem convex_on_pow_of_even
added theorem int_prod_range_nonneg
added theorem nnreal.am_gm2_weighted
added theorem nnreal.am_gm3_weighted
added theorem nnreal.am_gm_weighted
added theorem real.am_gm2_weighted
added theorem real.am_gm_weighted
added theorem real.pow_am_le_am_pow
added theorem real.young_inequality
added theorem nat.even.add
added theorem nat.even.sub
added theorem nnreal.coe_mk
added theorem set.compl_Ici
added theorem set.compl_Iic
added theorem set.compl_Iio
added theorem set.compl_Ioi
added theorem interior_Icc
added theorem interior_Ici
added theorem interior_Ico
added theorem interior_Iic
added theorem interior_Iio
added theorem interior_Ioc
added theorem interior_Ioi
added theorem interior_Ioo
modified theorem is_open_Iio
modified theorem is_open_Ioi
modified theorem is_open_Ioo