Real conjugate exponents

p.IsConjugateExponent q registers the fact that the real numbers p and q are > 1 and satisfy 1/p + 1/q = 1. This property shows up often in analysis, especially when dealing with L^p spaces.

We make several basic facts available through dot notation in this situation.

We also introduce p.conjugateExponent for p / (p-1). When p > 1, it is conjugate to p.

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

• one_lt : 1 < p
• inv_add_inv_conj : 1 / p + 1 / q = 1

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.

def Real.conjugateExponent (p : ℝ) : ℝ

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

Equations

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

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

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

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

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

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

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

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

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

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

theorem Real.IsConjugateExponent.conjugate_eq {p : ℝ} {q : ℝ} (h : Real.IsConjugateExponent p q) : Real.conjugateExponent p = q

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

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

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

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

theorem Real.IsConjugateExponent.one_lt_nnreal {p : ℝ} {q : ℝ} (h : Real.IsConjugateExponent p q) : 1 < Real.toNNReal p

theorem Real.IsConjugateExponent.inv_add_inv_conj_nnreal {p : ℝ} {q : ℝ} (h : Real.IsConjugateExponent p q) : 1 / Real.toNNReal p + 1 / Real.toNNReal q = 1

theorem Real.IsConjugateExponent.inv_add_inv_conj_ennreal {p : ℝ} {q : ℝ} (h : Real.IsConjugateExponent p q) : 1 / ENNReal.ofReal p + 1 / ENNReal.ofReal q = 1

theorem Real.isConjugateExponent_iff {p : ℝ} {q : ℝ} (h : 1 < p) : Real.IsConjugateExponent p q ↔ q = p / (p - 1)

theorem Real.isConjugateExponent_conjugateExponent {p : ℝ} (h : 1 < p) : Real.IsConjugateExponent p (Real.conjugateExponent p)

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