Structures · Data types

ENNReal.HolderTriple

A class stating that p q r : ℝ≥0∞ satisfy p⁻¹ + q⁻¹ = r⁻¹. This is exactly the condition for which Hölder's inequality is valid (see MeasureTheory.MemLp.smul). When r := 1, one generally says that p q are Hölder conjugate. This class exists so that we can define a heterogeneous scalar multiplication on MeasureTheory.Lp, and this is why r must be marked as a semiOutParam. We don't mark it as an outParam because this would prevent Lean from using HolderTriple p q r and HolderTriple p q r' within a single proof, as may be occasionally convenient.

Defined in

Mathlib.Data.ENNReal.Holder

Shape

3 explicit arguments · adds inv_add_inv_eq_inv