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.conjugate_eq
{p q : ℝ}
(h : p.is_conjugate_exponent q) :
p.conjugate_exponent = q
@[protected, symm]
theorem
real.is_conjugate_exponent.inv_add_inv_conj_nnreal
{p q : ℝ}
(h : p.is_conjugate_exponent q) :
theorem
real.is_conjugate_exponent.inv_add_inv_conj_ennreal
{p q : ℝ}
(h : p.is_conjugate_exponent q) :
1 / ennreal.of_real p + 1 / ennreal.of_real q = 1
theorem
real.is_conjugate_exponent_iff
{p q : ℝ}
(h : 1 < p) :
p.is_conjugate_exponent q ↔ q = p / (p - 1)