Documentation

Mathlib.Data.ENNReal.Holder

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.MemLp.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) :

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.

inv_add_inv_eq_inv : p⁻¹ + q⁻¹ = r⁻¹

Instances

theorem ENNReal.holderTriple_iff (p q : ENNReal) (r : semiOutParam ENNReal) :

p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹

@[reducible, inline]

abbrev ENNReal.HolderConjugate (p q : ENNReal) :

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

Equations

p.HolderConjugate q = p.HolderTriple q 1

Instances For

theorem ENNReal.holderConjugate_iff {p q : ENNReal} :

p.HolderConjugate q ↔ p⁻¹ + 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_eq (p q r : ENNReal) [p.HolderTriple q r] :

r⁻¹ = p⁻¹ + q⁻¹

theorem ENNReal.HolderTriple.unique (p q r : ENNReal) [p.HolderTriple q r] (r' : ENNReal) [hr' : p.HolderTriple q r'] :

r = r'

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.

theorem ENNReal.HolderTriple.unique_of_ne_zero (p q : ENNReal) {r : ENNReal} [p.HolderTriple q r] (q' : ENNReal) (hr : r ≠ 0) [p.HolderTriple q' r] :

q = q'

theorem ENNReal.HolderTriple.holderConjugate_div_div (p q r : ENNReal) [p.HolderTriple q r] (hr₀ : r ≠ 0) (hr : r ≠ ⊤) :

(p / r).HolderConjugate (q / r)

Hölder conjugates #

instance ENNReal.HolderConjugate.symm {p q : ENNReal} [hpq : p.HolderConjugate q] :

q.HolderConjugate p

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.ne_zero (p q : ENNReal) [p.HolderConjugate q] :

p ≠ 0

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.unique (p q : ENNReal) [p.HolderConjugate q] (q' : ENNReal) [hq' : p.HolderConjugate q'] :

q = 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⁻¹