Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 13:16 1d37ff18

View on Github →

feat(analysis/mean_inequalities): add weighted generalized mean inequality for ennreal (#5316)

Estimated changes

Modified src/analysis/mean_inequalities.lean

added theorem ennreal.rpow_arith_mean_le_arith_mean2_rpow

added theorem ennreal.rpow_arith_mean_le_arith_mean_rpow

Modified src/data/real/ennreal.lean

added theorem ennreal.le_of_top_imp_top_of_to_nnreal_le

added theorem ennreal.to_nnreal_mul

added theorem ennreal.to_nnreal_pow

added theorem ennreal.to_nnreal_prod