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