Commit 2022-02-24 18:24 d3d37017

View on Github →

feat(analysis/mean_inequalities): AM and GM are equal on a constant tuple (#12179) The converse is also true, but I have not gotten around to proving it.

Estimated changes

Modified src/analysis/mean_inequalities.lean

added theorem real.arith_mean_weighted_of_constant

added theorem real.geom_mean_eq_arith_mean_weighted_of_constant

added theorem real.geom_mean_weighted_of_constant

Modified src/analysis/special_functions/pow.lean

modified theorem real.rpow_add'

modified theorem real.rpow_add

added theorem real.rpow_add_of_nonneg

added theorem real.rpow_sum_of_nonneg

added theorem real.rpow_sum_of_pos

Modified src/data/finset/basic.lean

added theorem finset.filter_nonempty_iff

added theorem finset.forall_mem_cons

added theorem finset.mem_of_mem_filter