# 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 : ) :
p.IsConjExponent q 1 < p p⁻¹ + q⁻¹ = 1
structure Real.IsConjExponent (p : ) (q : ) :

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.

Instances For
theorem Real.IsConjExponent.one_lt {p : } {q : } (self : p.IsConjExponent q) :
1 < p
theorem Real.IsConjExponent.inv_add_inv_conj {p : } {q : } (self : p.IsConjExponent q) :

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

Equations
• p.conjExponent = p / (p - 1)
Instances For
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) :
theorem Real.IsConjExponent.inv_ne_zero {p : } {q : } (h : p.IsConjExponent q) :
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) :
theorem Real.IsConjExponent.inv_sub_one {p : } {q : } (h : p.IsConjExponent 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) :
= 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_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)
theorem NNReal.isConjExponent_iff (p : NNReal) (q : NNReal) :
p.IsConjExponent q 1 < p p⁻¹ + q⁻¹ = 1
structure NNReal.IsConjExponent (p : NNReal) (q : NNReal) :

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.

Instances For
theorem NNReal.IsConjExponent.one_lt {p : NNReal} {q : NNReal} (self : p.IsConjExponent q) :
1 < p
theorem NNReal.IsConjExponent.inv_add_inv_conj {p : NNReal} {q : NNReal} (self : p.IsConjExponent q) :
noncomputable def NNReal.conjExponent (p : NNReal) :

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

Equations
• p.conjExponent = p / (p - 1)
Instances For
@[simp]
theorem NNReal.isConjExponent_coe {p : NNReal} {q : NNReal} :
(p).IsConjExponent q p.IsConjExponent q
theorem NNReal.IsConjExponent.coe {p : NNReal} {q : NNReal} :
p.IsConjExponent q(p).IsConjExponent 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) :
theorem NNReal.IsConjExponent.one_sub_inv {p : NNReal} {q : NNReal} (h : p.IsConjExponent 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) :
p.conjExponent = 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 p.conjExponent
theorem Real.IsConjExponent.toNNReal {p : } {q : } (hpq : p.IsConjExponent q) :
p.toNNReal.IsConjExponent q.toNNReal