Commit 2020-06-13 09:51 938b73a4

View on Github →

feat(topology/metric_space/pi_lp): Holder and Minkowski inequalities in ennreal (#2988) Hölder and Minkowski inequalities for finite sums. Versions for ennreals.

Estimated changes

Modified src/algebra/big_operators.lean

added theorem with_top.sum_eq_top_iff

Modified src/analysis/mean_inequalities.lean

added theorem ennreal.Lp_add_le

added theorem ennreal.inner_le_Lp_mul_Lq

Modified src/data/real/ennreal.lean

added theorem ennreal.one_to_nnreal

added theorem ennreal.one_to_real

added theorem ennreal.sum_eq_top_iff