Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-11 20:24 666b9e59

View on Github →

refactor(analysis/mean_inequalities): review (#3023) Also add several lemmas to other files

Estimated changes

Modified src/algebra/group_with_zero.lean

added theorem div_mul_cancel_of_imp

added theorem mul_div_cancel_left_of_imp

added theorem mul_div_cancel_of_imp'

added theorem mul_div_cancel_of_imp

Modified src/analysis/convex/basic.lean

added theorem convex_on_const

added theorem convex_on_id

Modified src/analysis/convex/specific_functions.lean

Modified src/analysis/mean_inequalities.lean

modified theorem nnreal.am_gm2_weighted

modified theorem nnreal.am_gm3_weighted

modified theorem nnreal.am_gm_weighted

modified theorem nnreal.pow_am_le_am_pow

added theorem nnreal.rpow_am_le_am_rpow

modified theorem nnreal.young_inequality

modified theorem real.am_gm2_weighted

modified theorem real.am_gm_weighted

modified theorem real.fpow_am_le_am_fpow

modified theorem real.pow_am_le_am_pow

modified theorem real.pow_am_le_am_pow_of_even

added theorem real.rpow_am_le_am_rpow

modified theorem real.young_inequality

added theorem real.young_inequality_of_nonneg

Modified src/analysis/special_functions/pow.lean

modified theorem nnreal.rpow_add

added theorem nnreal.rpow_le_rpow_iff

added theorem nnreal.rpow_lt_rpow_iff

added theorem nnreal.rpow_sub'

added theorem nnreal.rpow_sub

added theorem real.rpow_le_rpow_iff

added theorem real.rpow_lt_rpow_iff

added theorem real.rpow_sub'

added theorem real.rpow_sub

Modified src/data/real/conjugate_exponents.lean

added theorem real.is_conjugate_exponent.conjugate_eq

added theorem real.is_conjugate_exponent.mul_eq_add

added theorem real.is_conjugate_exponent.nonneg

added theorem real.is_conjugate_exponent.one_div_nonneg

added theorem real.is_conjugate_exponent.sub_one_mul_conj

added theorem real.is_conjugate_exponent.sub_one_pos

Modified src/data/real/nnreal.lean

deleted theorem nnreal.div_mul_cancel

added theorem nnreal.div_self_le