feat: Generalise special case of Jensen

[YaelDillies]

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

---

[YaelDillies]

I have applied the refactor I was explaining in the comments.

[github-actions[bot]]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Monoid.Canonical.Defs	177	178	+1 (+0.56%)
Mathlib.Algebra.Order.Ring.Defs	203	204	+1 (+0.49%)
Mathlib.Algebra.Order.Chebyshev	807	809	+2 (+0.25%)
Mathlib.Algebra.Order.Rearrangement	624	623	-1 (-0.16%)

[github-actions[bot]]

PR summary 515738f619

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Chebyshev	833	837	+4 (+0.48%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.Additive.Corner.Roth	1
4 files Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma	2
Mathlib.Algebra.Order.Chebyshev	4

---

Declarations diff

+ pow_sum_le_card_mul_sum_pow +-- pow_sum_div_card_le_sum_pow

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13949~~
• ~~leanprover-community/mathlib4#15815~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors[bot]]

Canceled.

[YaelDillies]

It does actually pass CI. I just rebased on a too old master

[YaelDillies]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style