[Merged by Bors] - feat: Hölder triples / conjugates as a type class

[j-loreaux]

This PR defines a new class, ENNReal.HolderTriple, which takes arguments p q r : ℝ≥0∞,
with r marked as a semiOutParam, and states that p⁻¹ + q⁻¹ = r⁻¹. This is exactly the
condition for which Hölder's inequality is valid (see MeasureTheory.Memℒp.smul).
This allows us to declare a heterogeneous scalar multiplication (HSMul) instance on
MeasureTheory.Lp spaces.

In this file we provide many convenience lemmas in the presence of a HolderTriple instance.
All these are easily provable from facts about ℝ≥0∞, but it's convenient not to be forced
to reprove them each time.

For convenience we also define ENNReal.HolderConjugate (with arguments p q) as an
abbreviation for ENNReal.HolderTriple p q 1.

---

[github-actions]

PR summary 24c879fe44

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.ENNReal.Holder (new file)	694

---

Declarations diff

+ HolderConjugate
+ HolderTriple
+ eq_top_iff_eq_one
+ instInfty
+ instOneInfty
+ instTwoTwo
+ instZero
+ inv_add_inv_eq_inv
+ inv_add_inv_eq_one
+ inv_eq
+ inv_inv_add_inv
+ inv_le_inv
+ inv_sub_inv_eq_inv
+ inv_sub_inv_eq_inv'
+ le
+ lt_top_iff_one_lt
+ ne_top_iff_ne_one
+ of
+ one_div_add_one_div
+ one_div_eq
+ one_le
+ one_sub_inv
+ pos
+ sub_one_mul_inv
+ symm

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style