feat: Generalise special case of Jensen

[YaelDillies]

trafficstars

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

---