Commit 2024-10-01 14:00 47ef55c5

View on Github →

refactor: Generalise special case of Jensen (#11448) Real.pow_sum_div_card_le_sum_pow and NNReal.pow_sum_div_card_le_sum_pow both state that (∑ i in s, f i) ^ (n + 1) / s.card ^ n ≤ ∑ i in s, f i ^ (n + 1), but one for f : ι → ℝ and the other for f : ι → ℝ≥0. Both lemmas can be unified by deriving the inequality for f : ι → α where [LinearOrderedSemifield α] [ExistsAddOfLE α]. This involves generalising the rearrangement inequality semirings. From LeanAPAP

Estimated changes