Real conjugate exponents
p.is_conjugate_exponent 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.conjugate_exponent for p / (p-1). When p > 1, it is conjugate to p.
The conjugate exponent of p is q = p/(p-1), so that 1/p + 1/q = 1.
Equations
- p.conjugate_exponent = p / (p - 1)
theorem
real.is_conjugate_exponent.sub_one_ne_zero
{p q : ℝ} :
p.is_conjugate_exponent q → p - 1 ≠ 0
theorem
real.is_conjugate_exponent.one_div_nonneg
{p q : ℝ} :
p.is_conjugate_exponent q → 0 ≤ 1 / p
theorem
real.is_conjugate_exponent.one_div_ne_zero
{p q : ℝ} :
p.is_conjugate_exponent q → 1 / p ≠ 0
theorem
real.is_conjugate_exponent.conj_eq
{p q : ℝ} :
p.is_conjugate_exponent q → q = p / (p - 1)
theorem
real.is_conjugate_exponent.conjugate_eq
{p q : ℝ} :
p.is_conjugate_exponent q → p.conjugate_exponent = q
theorem
real.is_conjugate_exponent.sub_one_mul_conj
{p q : ℝ} :
p.is_conjugate_exponent q → (p - 1) * q = p
theorem
real.is_conjugate_exponent.mul_eq_add
{p q : ℝ} :
p.is_conjugate_exponent q → p * q = p + q
theorem
real.is_conjugate_exponent.symm
{p q : ℝ} :
p.is_conjugate_exponent q → q.is_conjugate_exponent p
theorem
real.is_conjugate_exponent_conjugate_exponent
{p : ℝ} :
1 < p → p.is_conjugate_exponent p.conjugate_exponent