Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-24 00:43 0ac9f83b

View on Github →

feat(analysis/mean_inequalities): Minkowski inequality for infinite sums (#10984) A few versions of the Minkowski inequality for tsum and has_sum.

Estimated changes

Modified src/analysis/mean_inequalities.lean

added theorem nnreal.Lp_add_le_has_sum

added theorem nnreal.Lp_add_le_tsum

added theorem real.Lp_add_le_has_sum_of_nonneg

added theorem real.Lp_add_le_tsum_of_nonneg

Modified src/analysis/special_functions/pow.lean

added theorem nnreal.eq_rpow_one_div_iff

added theorem nnreal.rpow_eq_rpow_iff

added theorem nnreal.rpow_inv_rpow_self

added theorem nnreal.rpow_left_bijective

added theorem nnreal.rpow_left_injective

added theorem nnreal.rpow_left_surjective

added theorem nnreal.rpow_one_div_eq_iff

added theorem nnreal.rpow_one_div_le_iff

added theorem nnreal.rpow_self_rpow_inv