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.

TODO

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

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

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

def Real.conjExponent (p : ℝ) : ℝ

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.IsConjExponent.inv_add_inv_conj_ennreal {p : ℝ} {q : ℝ} (h : Real.IsConjExponent p 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) : Real.IsConjExponent a⁻¹ b⁻¹

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

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

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

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

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

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

structure NNReal.IsConjExponent (p : NNReal) (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

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

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

@[simp]

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

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

Alias of the reverse direction of NNReal.isConjExponent_coe.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NNReal.IsConjExponent.inv_inv {a : NNReal} {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_iff_eq_conjExponent {p : NNReal} {q : NNReal} (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1)

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

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