Commit 2024-03-05 16:05 6dcd9f8d

View on Github →

feat: Weighted Hölder inequality, Cauchy-Schwarz with square roots (#10630) From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/MeanInequalities.lean

added theorem ENNReal.inner_le_weight_mul_Lp_of_nonneg

added theorem NNReal.inner_le_weight_mul_Lp

added theorem Real.inner_le_weight_mul_Lp_of_nonneg

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem ENNReal.rpow_eq_zero_iff_of_pos

added theorem NNReal.rpow_inv_rpow

added theorem NNReal.rpow_of_add_eq

added theorem NNReal.rpow_rpow_inv

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Real.rpow_of_add_eq

Modified Mathlib/Data/Real/Sqrt.lean

deleted theorem Finset.sum_mul_le_sqrt_mul_sqrt

added theorem NNReal.sum_mul_le_sqrt_mul_sqrt

added theorem NNReal.sum_sqrt_mul_sqrt_le

added theorem Real.sum_mul_le_sqrt_mul_sqrt

added theorem Real.sum_sqrt_mul_sqrt_le