Commit 2026-03-18 18:48 0005884c

View on Github →

feat: generalize Hölder's inequality for sums to Real.HolderTriple (#35198) Currently the API exists only for Real.HolderConjugate. This generalizes it in anticipation of #35197, which implements the Hölder framework for lp spaces.

Estimated changes

Modified Mathlib/Analysis/MeanInequalities.lean

added theorem NNReal.Lr_le_Lp_mul_Lq

added theorem NNReal.Lr_le_Lp_mul_Lq_tsum

added theorem NNReal.Lr_rpow_le_Lp_mul_Lq

added theorem NNReal.Lr_rpow_le_Lp_mul_Lq_tsum

deleted theorem NNReal.inner_le_Lp_mul_Lq_tsum'

added theorem NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum

added theorem NNReal.summable_and_inner_le_Lp_mul_Lq_tsum

added theorem NNReal.summable_mul_rpow_of_Lp_Lq

added theorem Real.Lr_le_Lp_mul_Lq_tsum_of_nonneg

added theorem Real.Lr_rpow_le_Lp_mul_Lq

added theorem Real.Lr_rpow_le_Lp_mul_Lq_of_nonneg

added theorem Real.Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg

deleted theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg'

added theorem Real.summable_Lr_of_Lp_Lq_of_nonneg

added theorem Real.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg

added theorem Real.summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg

Modified Mathlib/Data/Real/ConjExponents.lean

added theorem NNReal.HolderTriple.all_pos

added theorem Real.HolderTriple.all_pos