Commit 2025-02-14 03:53 5caf4f88

feat: Hölder triples / conjugates as a type class (#21854) 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.