Hölder triples

This file 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.

class ENNReal.HolderTriple (p q : ENNReal) (r : semiOutParam ENNReal) : Prop

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.Memℒp.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.

• inv_add_inv' : p⁻¹ + q⁻¹ = r⁻¹

@[reducible, inline]

abbrev ENNReal.HolderConjugate (p q : ENNReal) : Prop

An abbreviation for ENNReal.HolderTriple p q 1, this class states p⁻¹ + q⁻¹ = 1.

Equations

• p.HolderConjugate q = p.HolderTriple q 1

Hölder triples

theorem ENNReal.HolderTriple.of (p q : ENNReal) : p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹

This is not marked as an instance so that Lean doesn't always find this one and a more canonical value of r can be used.

instance ENNReal.HolderTriple.symm {p q r : ENNReal} [hpqr : p.HolderTriple q r] : q.HolderTriple p r

instance ENNReal.HolderTriple.instInfty (p : ENNReal) : p.HolderTriple ⊤ p

instance ENNReal.HolderTriple.instZero (p : ENNReal) : p.HolderTriple 0 0

theorem ENNReal.HolderTriple.inv_add_inv_eq_inv (p q r : ENNReal) [p.HolderTriple q r] : p⁻¹ + q⁻¹ = r⁻¹

theorem ENNReal.HolderTriple.inv_eq (p q r : ENNReal) [p.HolderTriple q r] : r⁻¹ = p⁻¹ + q⁻¹

theorem ENNReal.HolderTriple.one_div_add_one_div (p q r : ENNReal) [p.HolderTriple q r] : 1 / p + 1 / q = 1 / r

theorem ENNReal.HolderTriple.one_div_eq (p q r : ENNReal) [p.HolderTriple q r] : 1 / r = 1 / p + 1 / q

theorem ENNReal.HolderTriple.inv_inv_add_inv (p q r : ENNReal) [p.HolderTriple q r] : (p⁻¹ + q⁻¹)⁻¹ = r

theorem ENNReal.HolderTriple.le (p q r : ENNReal) [p.HolderTriple q r] : r ≤ p

theorem ENNReal.HolderTriple.inv_le_inv (p q r : ENNReal) [p.HolderTriple q r] : p⁻¹ ≤ r⁻¹

theorem ENNReal.HolderTriple.inv_sub_inv_eq_inv (p q : ENNReal) {r : ENNReal} [p.HolderTriple q r] (hr : r ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹

theorem ENNReal.HolderTriple.inv_sub_inv_eq_inv' (p q r : ENNReal) [p.HolderTriple q r] (hq : q ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹

assumes q ≠ 0 instead of r ≠ 0.

Hölder conjugates

instance ENNReal.HolderConjugate.instTwoTwo : HolderConjugate 2 2

instance ENNReal.HolderConjugate.instOneInfty : HolderConjugate 1 ⊤

theorem ENNReal.HolderConjugate.one_le (p q : ENNReal) [p.HolderConjugate q] : 1 ≤ p

theorem ENNReal.HolderConjugate.pos (p q : ENNReal) [p.HolderConjugate q] : 0 < p

theorem ENNReal.HolderConjugate.inv_add_inv_eq_one (p q : ENNReal) [p.HolderConjugate q] : p⁻¹ + q⁻¹ = 1

theorem ENNReal.HolderConjugate.one_sub_inv (p q : ENNReal) [p.HolderConjugate q] : 1 - p⁻¹ = q⁻¹

theorem ENNReal.HolderConjugate.eq_top_iff_eq_one (p q : ENNReal) [p.HolderConjugate q] : p = ⊤ ↔ q = 1

theorem ENNReal.HolderConjugate.ne_top_iff_ne_one (p q : ENNReal) [p.HolderConjugate q] : p ≠ ⊤ ↔ q ≠ 1

theorem ENNReal.HolderConjugate.lt_top_iff_one_lt (p q : ENNReal) [p.HolderConjugate q] : p < ⊤ ↔ 1 < q

theorem ENNReal.HolderConjugate.sub_one_mul_inv (p q : ENNReal) [p.HolderConjugate q] (hp : p ≠ ⊤) : (p - 1) * p⁻¹ = q⁻¹