Real conjugate exponents

This file defines Hölder triple and Hölder conjugate exponents in ℝ and ℝ≥0. Real numbers p, q and r form a Hölder triple if 0 < p and 0 < q and p⁻¹ + q⁻¹ = r⁻¹ (which of course implies 0 < r). We say p and q are Hölder conjugate if p, q and 1 are a Hölder triple. In this case, 1 < p and 1 < q. This property shows up often in analysis, especially when dealing with L^p spaces.

These notions mimic the same notions for extended nonnegative reals where p q r : ℝ≥0∞ are allowed to take the values 0 and ∞.

Main declarations

• Real.HolderTriple: Predicate for two real numbers to be a Hölder triple.
• Real.HolderConjugate: Predicate for two real numbers to be Hölder conjugate.
• Real.conjExponent: Conjugate exponent of a real number.
• NNReal.HolderTriple: Predicate for two nonnegative real numbers to be a Hölder triple.
• NNReal.HolderConjugate: Predicate for two nonnegative real numbers to be Hölder conjugate.
• NNReal.conjExponent: Conjugate exponent of a nonnegative real number.
• ENNReal.conjExponent: Conjugate exponent of an extended nonnegative real number.

TODO

• Eradicate the 1 / p spelling in lemmas.

structure Real.HolderTriple (p q r : ℝ) : Prop

Real numbers p q r : ℝ are said to be a Hölder triple if p and q are positive and p⁻¹ + q⁻¹ = r⁻¹.

• inv_add_inv_eq_inv : p⁻¹ + q⁻¹ = r⁻¹
• left_pos : 0 < p
• right_pos : 0 < q

theorem Real.holderTriple_iff (p q r : ℝ) : p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q

@[reducible, inline]

abbrev Real.HolderConjugate (p q : ℝ) : Prop

Real numbers p q : ℝ are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for Real.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See Real.holderConjugate_iff.

def Real.conjExponent (p : ℝ) : ℝ

The conjugate exponent of p is q = p / (p-1), so that p⁻¹ + q⁻¹ = 1.

theorem Real.HolderTriple.of_pos {p q : ℝ} (hp : 0 < p) (hq : 0 < q) : p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹

theorem Real.HolderTriple.symm {p q r : ℝ} (h : p.HolderTriple q r) : q.HolderTriple p r

theorem Real.HolderTriple.pos {p q r : ℝ} (h : p.HolderTriple q r) : 0 < p

theorem Real.HolderTriple.nonneg {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ p

theorem Real.HolderTriple.ne_zero {p q r : ℝ} (h : p.HolderTriple q r) : p ≠ 0

theorem Real.HolderTriple.inv_pos {p q r : ℝ} (h : p.HolderTriple q r) : 0 < p⁻¹

theorem Real.HolderTriple.inv_nonneg {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ p⁻¹

theorem Real.HolderTriple.inv_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) : p⁻¹ ≠ 0

theorem Real.HolderTriple.one_div_pos {p q r : ℝ} (h : p.HolderTriple q r) : 0 < 1 / p

theorem Real.HolderTriple.one_div_nonneg {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ 1 / p

theorem Real.HolderTriple.one_div_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) : 1 / p ≠ 0

theorem Real.HolderTriple.pos' {p q r : ℝ} (h : p.HolderTriple q r) : 0 < r

For r, instead of p

theorem Real.HolderTriple.nonneg' {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ r

For r, instead of p

theorem Real.HolderTriple.ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) : r ≠ 0

For r, instead of p

theorem Real.HolderTriple.inv_pos' {p q r : ℝ} (h : p.HolderTriple q r) : 0 < r⁻¹

For r, instead of p

theorem Real.HolderTriple.inv_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ r⁻¹

For r, instead of p

theorem Real.HolderTriple.inv_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) : r⁻¹ ≠ 0

For r, instead of p

theorem Real.HolderTriple.one_div_pos' {p q r : ℝ} (h : p.HolderTriple q r) : 0 < 1 / r

For r, instead of p

theorem Real.HolderTriple.one_div_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) : 0 ≤ 1 / r

For r, instead of p

theorem Real.HolderTriple.one_div_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) : 1 / r ≠ 0

For r, instead of p

theorem Real.HolderTriple.inv_eq {p q r : ℝ} (h : p.HolderTriple q r) : r⁻¹ = p⁻¹ + q⁻¹

theorem Real.HolderTriple.one_div_add_one_div {p q r : ℝ} (h : p.HolderTriple q r) : 1 / p + 1 / q = 1 / r

theorem Real.HolderTriple.one_div_eq {p q r : ℝ} (h : p.HolderTriple q r) : 1 / r = 1 / p + 1 / q

theorem Real.HolderTriple.inv_inv_add_inv {p q r : ℝ} (h : p.HolderTriple q r) : (p⁻¹ + q⁻¹)⁻¹ = r

theorem Real.HolderTriple.inv_lt_inv {p q r : ℝ} (h : p.HolderTriple q r) : p⁻¹ < r⁻¹

theorem Real.HolderTriple.lt {p q r : ℝ} (h : p.HolderTriple q r) : r < p

theorem Real.HolderTriple.inv_sub_inv_eq_inv {p q r : ℝ} (h : p.HolderTriple q r) : r⁻¹ - q⁻¹ = p⁻¹

theorem Real.HolderTriple.holderConjugate_div_div {p q r : ℝ} (h : p.HolderTriple q r) : (p / r).HolderConjugate (q / r)

theorem Real.HolderConjugate.two_two : HolderConjugate 2 2

theorem Real.HolderConjugate.symm {p q : ℝ} (h : p.HolderConjugate q) : q.HolderConjugate p

theorem Real.HolderConjugate.inv_add_inv_eq_one {p q : ℝ} (h : p.HolderConjugate q) : p⁻¹ + q⁻¹ = 1

theorem Real.HolderConjugate.sub_one_pos {p q : ℝ} (h : p.HolderConjugate q) : 0 < p - 1

theorem Real.HolderConjugate.sub_one_ne_zero {p q : ℝ} (h : p.HolderConjugate q) : p - 1 ≠ 0

theorem Real.HolderConjugate.conjugate_eq {p q : ℝ} (h : p.HolderConjugate q) : q = p / (p - 1)

theorem Real.HolderConjugate.conjExponent_eq {p q : ℝ} (h : p.HolderConjugate q) : p.conjExponent = q

theorem Real.HolderConjugate.one_sub_inv {p q : ℝ} (h : p.HolderConjugate q) : 1 - p⁻¹ = q⁻¹

theorem Real.HolderConjugate.inv_sub_one {p q : ℝ} (h : p.HolderConjugate q) : p⁻¹ - 1 = -q⁻¹

theorem Real.HolderConjugate.sub_one_mul_conj {p q : ℝ} (h : p.HolderConjugate q) : (p - 1) * q = p

theorem Real.HolderConjugate.mul_eq_add {p q : ℝ} (h : p.HolderConjugate q) : p * q = p + q

theorem Real.HolderConjugate.div_conj_eq_sub_one {p q : ℝ} (h : p.HolderConjugate q) : p / q = p - 1

theorem Real.HolderConjugate.inv_add_inv_ennreal {p q : ℝ} (h : p.HolderConjugate q) : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

theorem Real.holderConjugate_iff {p q : ℝ} : p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

theorem Real.HolderConjugate.inv_inv {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a⁻¹.HolderConjugate b⁻¹

theorem Real.HolderConjugate.inv_one_sub_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) : a⁻¹.HolderConjugate (1 - a)⁻¹

theorem Real.HolderConjugate.one_sub_inv_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) : (1 - a)⁻¹.HolderConjugate a⁻¹

theorem Real.holderConjugate_comm {p q : ℝ} : p.HolderConjugate q ↔ q.HolderConjugate p

theorem Real.holderConjugate_iff_eq_conjExponent {p q : ℝ} (hp : 1 < p) : p.HolderConjugate q ↔ q = p / (p - 1)

theorem Real.HolderConjugate.conjExponent {p : ℝ} (h : 1 < p) : p.HolderConjugate p.conjExponent

theorem Real.holderConjugate_one_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : (1 / a).HolderConjugate (1 / b)

structure NNReal.HolderTriple (p q r : NNReal) : Prop

Nonnegative real numbers p q r : ℝ≥0 are said to be a Hölder triple if p and q are positive and p⁻¹ + q⁻¹ = r⁻¹.

• inv_add_inv_eq_inv : p⁻¹ + q⁻¹ = r⁻¹
• left_pos : 0 < p
• right_pos : 0 < q

theorem NNReal.holderTriple_iff (p q r : NNReal) : p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q

@[reducible, inline]

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

Nonnegative real numbers p q : ℝ≥0 are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for NNReal.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See NNReal.holderConjugate_iff.

def NNReal.conjExponent (p : NNReal) : NNReal

The conjugate exponent of p is q = p/(p-1), so that p⁻¹ + q⁻¹ = 1.

@[simp]

theorem NNReal.holderTriple_coe_iff {p q r : NNReal} : (↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

theorem NNReal.HolderTriple.coe {p q r : NNReal} : p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r

Alias of the reverse direction of NNReal.holderTriple_coe_iff.

@[simp]

theorem NNReal.holderConjugate_coe_iff {p q : NNReal} : (↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

theorem NNReal.HolderConjugate.coe {p q : NNReal} : p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

theorem NNReal.HolderTriple.of_pos {p q : NNReal} (hp : 0 < p) (hq : 0 < q) : p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹

theorem NNReal.HolderTriple.symm {p q r : NNReal} (h : p.HolderTriple q r) : q.HolderTriple p r

theorem NNReal.HolderTriple.pos {p q r : NNReal} (h : p.HolderTriple q r) : 0 < p

theorem NNReal.HolderTriple.nonneg {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ p

theorem NNReal.HolderTriple.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) : p ≠ 0

theorem NNReal.HolderTriple.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) : 0 < p⁻¹

theorem NNReal.HolderTriple.inv_nonneg {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ p⁻¹

theorem NNReal.HolderTriple.inv_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) : p⁻¹ ≠ 0

theorem NNReal.HolderTriple.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) : 0 < 1 / p

theorem NNReal.HolderTriple.one_div_nonneg {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ 1 / p

theorem NNReal.HolderTriple.one_div_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) : 1 / p ≠ 0

theorem NNReal.HolderTriple.pos' {p q r : NNReal} (h : p.HolderTriple q r) : 0 < r

For r, instead of p

theorem NNReal.HolderTriple.nonneg' {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ r

For r, instead of p

theorem NNReal.HolderTriple.ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) : r ≠ 0

For r, instead of p

theorem NNReal.HolderTriple.inv_pos' {p q r : NNReal} (h : p.HolderTriple q r) : 0 < r⁻¹

For r, instead of p

theorem NNReal.HolderTriple.inv_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ r⁻¹

For r, instead of p

theorem NNReal.HolderTriple.inv_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) : r⁻¹ ≠ 0

For r, instead of p

theorem NNReal.HolderTriple.one_div_pos' {p q r : NNReal} (h : p.HolderTriple q r) : 0 < 1 / r

For r, instead of p

theorem NNReal.HolderTriple.one_div_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) : 0 ≤ 1 / r

For r, instead of p

theorem NNReal.HolderTriple.one_div_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) : 1 / r ≠ 0

For r, instead of p

theorem NNReal.HolderTriple.inv_eq {p q r : NNReal} (h : p.HolderTriple q r) : r⁻¹ = p⁻¹ + q⁻¹

theorem NNReal.HolderTriple.one_div_add_one_div {p q r : NNReal} (h : p.HolderTriple q r) : 1 / p + 1 / q = 1 / r

theorem NNReal.HolderTriple.one_div_eq {p q r : NNReal} (h : p.HolderTriple q r) : 1 / r = 1 / p + 1 / q

theorem NNReal.HolderTriple.inv_inv_add_inv {p q r : NNReal} (h : p.HolderTriple q r) : (p⁻¹ + q⁻¹)⁻¹ = r

theorem NNReal.HolderTriple.inv_lt_inv {p q r : NNReal} (h : p.HolderTriple q r) : p⁻¹ < r⁻¹

theorem NNReal.HolderTriple.lt {p q r : NNReal} (h : p.HolderTriple q r) : r < p

theorem NNReal.HolderTriple.inv_sub_inv_eq_inv {p q r : NNReal} (h : p.HolderTriple q r) : r⁻¹ - q⁻¹ = p⁻¹

theorem NNReal.HolderTriple.holderConjugate_div_div {p q r : NNReal} (h : p.HolderTriple q r) : (p / r).HolderConjugate (q / r)

theorem NNReal.HolderConjugate.two_two : HolderConjugate 2 2

theorem NNReal.HolderConjugate.symm {p q : NNReal} (h : p.HolderConjugate q) : q.HolderConjugate p

theorem NNReal.HolderConjugate.inv_add_inv_eq_one {p q : NNReal} (h : p.HolderConjugate q) : p⁻¹ + q⁻¹ = 1

theorem NNReal.HolderConjugate.sub_one_pos {p q : NNReal} (h : p.HolderConjugate q) : 0 < p - 1

theorem NNReal.HolderConjugate.sub_one_ne_zero {p q : NNReal} (h : p.HolderConjugate q) : p - 1 ≠ 0

theorem NNReal.HolderConjugate.conjugate_eq {p q : NNReal} (h : p.HolderConjugate q) : q = p / (p - 1)

theorem NNReal.HolderConjugate.conjExponent_eq {p q : NNReal} (h : p.HolderConjugate q) : p.conjExponent = q

theorem NNReal.HolderConjugate.one_sub_inv {p q : NNReal} (h : p.HolderConjugate q) : 1 - p⁻¹ = q⁻¹

theorem NNReal.HolderConjugate.sub_one_mul_conj {p q : NNReal} (h : p.HolderConjugate q) : (p - 1) * q = p

theorem NNReal.HolderConjugate.mul_eq_add {p q : NNReal} (h : p.HolderConjugate q) : p * q = p + q

theorem NNReal.HolderConjugate.div_conj_eq_sub_one {p q : NNReal} (h : p.HolderConjugate q) : p / q = p - 1

theorem NNReal.HolderConjugate.inv_add_inv_ennreal {p q : NNReal} (h : p.HolderConjugate q) : ↑p⁻¹ + ↑q⁻¹ = 1

theorem NNReal.holderConjugate_iff {p q : NNReal} : p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

theorem NNReal.HolderConjugate.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a⁻¹.HolderConjugate b⁻¹

theorem NNReal.HolderConjugate.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) : a⁻¹.HolderConjugate (1 - a)⁻¹

theorem NNReal.HolderConjugate.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) : (1 - a)⁻¹.HolderConjugate a⁻¹

theorem NNReal.holderConjugate_comm {p q : NNReal} : p.HolderConjugate q ↔ q.HolderConjugate p

theorem NNReal.holderConjugate_iff_eq_conjExponent {p q : NNReal} (hp : 1 < p) : p.HolderConjugate q ↔ q = p / (p - 1)

theorem NNReal.HolderConjugate.conjExponent {p : NNReal} (h : 1 < p) : p.HolderConjugate p.conjExponent

theorem NNReal.holderConjugate_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : (1 / a).HolderConjugate (1 / b)

theorem Real.HolderTriple.toNNReal {p q r : ℝ} (h : p.HolderTriple q r) : p.toNNReal.HolderTriple q.toNNReal r.toNNReal

theorem Real.HolderConjugate.toNNReal {p q : ℝ} (h : p.HolderConjugate q) : p.toNNReal.HolderConjugate q.toNNReal

noncomputable def ENNReal.conjExponent (p : ENNReal) : ENNReal

The conjugate exponent of p is q = 1 + (p - 1)⁻¹, so that p⁻¹ + q⁻¹ = 1.

theorem ENNReal.coe_conjExponent {p : NNReal} (hp : 1 < p) : ↑p.conjExponent = (↑p).conjExponent

@[simp]

theorem ENNReal.holderTriple_coe_iff {p q r : NNReal} (hr : r ≠ 0) : (↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

theorem NNReal.HolderTriple.coe_ennreal {p q r : NNReal} (hr : r ≠ 0) : p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r

Alias of the reverse direction of ENNReal.holderTriple_coe_iff.

@[simp]

theorem ENNReal.holderConjugate_coe_iff {p q : NNReal} : (↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

theorem NNReal.HolderConjugate.coe_ennreal {p q : NNReal} : p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

theorem Real.HolderTriple.ennrealOfReal {p q r : ℝ} (h : p.HolderTriple q r) : (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)

theorem Real.HolderConjugate.ennrealOfReal {p q : ℝ} (h : p.HolderConjugate q) : (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)

theorem ENNReal.HolderTriple.of_toReal {p q r : ENNReal} (h : p.toReal.HolderTriple q.toReal r.toReal) : p.HolderTriple q r

theorem ENNReal.HolderTriple.toReal_iff {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toReal) (hq : 0 < q.toReal) : p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r

theorem ENNReal.HolderTriple.toReal {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toReal) (hq : 0 < q.toReal) [p.HolderTriple q r] : p.toReal.HolderTriple q.toReal r.toReal

theorem ENNReal.HolderTriple.of_toNNReal {p q r : ENNReal} (h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal) : p.HolderTriple q r

theorem ENNReal.HolderTriple.toNNReal_iff {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) : p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r

theorem ENNReal.HolderTriple.toNNReal {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) [p.HolderTriple q r] : p.toNNReal.HolderTriple q.toNNReal r.toNNReal

theorem ENNReal.HolderConjugate.of_toReal {p q : ENNReal} (h : p.toReal.HolderConjugate q.toReal) : p.HolderConjugate q

theorem ENNReal.HolderConjugate.toReal_iff {p q : ENNReal} (hp : 1 < p.toReal) : p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q

theorem ENNReal.HolderConjugate.toReal {p q : ENNReal} (hp : 1 < p.toReal) [p.HolderConjugate q] : p.toReal.HolderConjugate q.toReal

theorem ENNReal.HolderConjugate.of_toNNReal {p q : ENNReal} (h : p.toNNReal.HolderConjugate q.toNNReal) : p.HolderConjugate q

theorem ENNReal.HolderConjugate.toNNReal_iff {p q : ENNReal} (hp : 1 < p.toNNReal) : p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q

theorem ENNReal.HolderConjugate.toNNReal {p q : ENNReal} (hp : 1 < p.toNNReal) [p.HolderConjugate q] : p.toNNReal.HolderConjugate q.toNNReal

theorem ENNReal.HolderConjugate.conjExponent {p : ENNReal} (hp : 1 ≤ p) : p.HolderConjugate p.conjExponent

instance ENNReal.HolderConjugate.instConjExponentOfFactLeOfNat {p : ENNReal} [Fact (1 ≤ p)] : p.HolderConjugate p.conjExponent

theorem ENNReal.HolderConjugate.conjExponent_eq {p q : ENNReal} [h : p.HolderConjugate q] : p.conjExponent = q

theorem ENNReal.HolderConjugate.conj_eq {p q : ENNReal} [h : p.HolderConjugate q] : q = 1 + (p - 1)⁻¹

theorem ENNReal.HolderConjugate.mul_eq_add {p q : ENNReal} [h : p.HolderConjugate q] : p * q = p + q

theorem ENNReal.HolderConjugate.div_conj_eq_sub_one {p q : ENNReal} [h : p.HolderConjugate q] : p / q = p - 1

theorem ENNReal.HolderConjugate.inv_inv {a b : ENNReal} (hab : a + b = 1) : a⁻¹.HolderConjugate b⁻¹

theorem ENNReal.HolderConjugate.inv_one_sub_inv {a : ENNReal} (ha : a ≤ 1) : a⁻¹.HolderConjugate (1 - a)⁻¹

theorem ENNReal.HolderConjugate.inv_one_sub_inv' {a : ENNReal} (ha : 1 ≤ a) : a.HolderConjugate (1 - a⁻¹)⁻¹

theorem ENNReal.HolderConjugate.one_sub_inv_inv {a : ENNReal} (ha : a ≤ 1) : (1 - a)⁻¹.HolderConjugate a⁻¹

theorem ENNReal.HolderConjugate.top_one : ⊤.HolderConjugate 1

theorem ENNReal.HolderConjugate.one_top : HolderConjugate 1 ⊤

theorem ENNReal.isConjExponent_comm {p q : ENNReal} : p.HolderConjugate q ↔ q.HolderConjugate p

theorem ENNReal.isConjExponent_iff_eq_conjExponent {p q : ENNReal} (hp : 1 ≤ p) : p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹