Commit 2023-05-25 13:41 9febf7e0

View on Github →

feat: port Analysis.MeanInequalitiesPow (#4331)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/MeanInequalitiesPow.lean

added theorem ENNReal.add_rpow_le_rpow_add

added theorem ENNReal.rpow_add_le_add_rpow

added theorem ENNReal.rpow_add_le_mul_rpow_add_rpow

added theorem ENNReal.rpow_add_rpow_le

added theorem ENNReal.rpow_add_rpow_le_add

added theorem ENNReal.rpow_arith_mean_le_arith_mean2_rpow

added theorem ENNReal.rpow_arith_mean_le_arith_mean_rpow

added theorem NNReal.add_rpow_le_rpow_add

added theorem NNReal.arith_mean_le_rpow_mean

added theorem NNReal.pow_arith_mean_le_arith_mean_pow

added theorem NNReal.pow_sum_div_card_le_sum_pow

added theorem NNReal.rpow_add_le_add_rpow

added theorem NNReal.rpow_add_le_mul_rpow_add_rpow

added theorem NNReal.rpow_add_rpow_le

added theorem NNReal.rpow_add_rpow_le_add

added theorem NNReal.rpow_arith_mean_le_arith_mean2_rpow

added theorem NNReal.rpow_arith_mean_le_arith_mean_rpow

added theorem Real.arith_mean_le_rpow_mean

added theorem Real.pow_arith_mean_le_arith_mean_pow

added theorem Real.pow_arith_mean_le_arith_mean_pow_of_even

added theorem Real.pow_sum_div_card_le_sum_pow

added theorem Real.rpow_arith_mean_le_arith_mean_rpow

added theorem Real.zpow_arith_mean_le_arith_mean_zpow