Real conjugate exponents

This file defines conjugate exponents in ℝ and ℝ≥0. Real numbers p and q are conjugate if they are both greater than 1 and satisfy p⁻¹ + q⁻¹ = 1. This property shows up often in analysis, especially when dealing with L^p spaces.

Main declarations

• Real.IsConjExponent: Predicate for two real numbers to be conjugate.
• Real.conjExponent: Conjugate exponent of a real number.
• NNReal.IsConjExponent: Predicate for two nonnegative real numbers to be conjugate.
• NNReal.conjExponent: Conjugate exponent of a nonnegative real number.
• ENNReal.IsConjExponent: Predicate for two extended nonnegative real numbers to be conjugate.
• ENNReal.conjExponent: Conjugate exponent of an extended nonnegative real number.

TODO

• Eradicate the 1 / p spelling in lemmas.
• Do we want an ℝ≥0∞ version?

structure Real.IsConjExponent (p q : ℝ) : Prop

Two real exponents p, q are conjugate if they are > 1 and satisfy the equality 1/p + 1/q = 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

• one_lt : 1 < p
• inv_add_inv_conj : p⁻¹ + q⁻¹ = 1

theorem Real.isConjExponent_iff (p q : ℝ) : p.IsConjExponent q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

def Real.conjExponent (p : ℝ) : ℝ

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

Equations

• p.conjExponent = p / (p - 1)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.isConjExponent_comm {p q : ℝ} : p.IsConjExponent q ↔ q.IsConjExponent p

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

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

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

structure NNReal.IsConjExponent (p q : NNReal) : Prop

Two nonnegative real exponents p, q are conjugate if they are > 1 and satisfy the equality 1/p + 1/q = 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

• one_lt : 1 < p
• inv_add_inv_conj : p⁻¹ + q⁻¹ = 1

theorem NNReal.isConjExponent_iff (p q : NNReal) : p.IsConjExponent q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

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

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

Equations

• p.conjExponent = p / (p - 1)

@[simp]

theorem NNReal.isConjExponent_coe {p q : NNReal} : (↑p).IsConjExponent ↑q ↔ p.IsConjExponent q

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

Alias of the reverse direction of NNReal.isConjExponent_coe.

theorem NNReal.IsConjExponent.one_le {p q : NNReal} (h : p.IsConjExponent q) : 1 ≤ p

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

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

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

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

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

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

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

theorem NNReal.IsConjExponent.conj_eq {p q : NNReal} (h : p.IsConjExponent q) : q = p / (p - 1)

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

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

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

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

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

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

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

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

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

theorem NNReal.isConjExponent_comm {p q : NNReal} : p.IsConjExponent q ↔ q.IsConjExponent p

theorem NNReal.isConjExponent_iff_eq_conjExponent {p q : NNReal} (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1)

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

theorem Real.IsConjExponent.toNNReal {p q : ℝ} (hpq : p.IsConjExponent q) : p.toNNReal.IsConjExponent q.toNNReal

structure ENNReal.IsConjExponent (p q : ENNReal) : Prop

Two extended nonnegative real exponents p, q are conjugate and satisfy the equality 1/p + 1/q = 1. This condition shows up in many theorems in analysis, notably related to L^p norms. Note that we permit one of the exponents to be ∞ and the other 1.

• inv_add_inv_conj : p⁻¹ + q⁻¹ = 1

theorem ENNReal.isConjExponent_iff (p q : ENNReal) : p.IsConjExponent q ↔ p⁻¹ + q⁻¹ = 1

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

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

Equations

• p.conjExponent = 1 + (p - 1)⁻¹

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

@[simp]

theorem ENNReal.isConjExponent_coe {p q : NNReal} : (↑p).IsConjExponent ↑q ↔ p.IsConjExponent q

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

Alias of the reverse direction of ENNReal.isConjExponent_coe.

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

theorem ENNReal.IsConjExponent.symm {p q : ENNReal} (h : p.IsConjExponent q) : q.IsConjExponent p

theorem ENNReal.IsConjExponent.one_le {p q : ENNReal} (h : p.IsConjExponent q) : 1 ≤ p

theorem ENNReal.IsConjExponent.pos {p q : ENNReal} (h : p.IsConjExponent q) : 0 < p

theorem ENNReal.IsConjExponent.ne_zero {p q : ENNReal} (h : p.IsConjExponent q) : p ≠ 0

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

theorem ENNReal.IsConjExponent.conjExponent_eq {p q : ENNReal} (h : p.IsConjExponent q) : p.conjExponent = q

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

theorem ENNReal.IsConjExponent.mul_eq_add {p q : ENNReal} (h : p.IsConjExponent q) : p * q = p + q

theorem ENNReal.IsConjExponent.div_conj_eq_sub_one {p q : ENNReal} (h : p.IsConjExponent q) : p / q = p - 1

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

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

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

theorem ENNReal.IsConjExponent.top_one : ⊤.IsConjExponent 1

theorem ENNReal.IsConjExponent.one_top : ENNReal.IsConjExponent 1 ⊤

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

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