Real conjugate exponents #
This file defines Hölder triple and Hölder conjugate exponents in ℝ
and ℝ≥0
. Real numbers p
,
q
and r
form a Hölder triple if 0 < p
and 0 < q
and p⁻¹ + q⁻¹ = r⁻¹
(which of course
implies 0 < r
). We say p
and q
are Hölder conjugate if p
, q
and 1
are a Hölder triple.
In this case, 1 < p
and 1 < q
. This property shows up often in analysis, especially when dealing
with L^p
spaces.
These notions mimic the same notions for extended nonnegative reals where p q r : ℝ≥0∞
are allowed
to take the values 0
and ∞
.
Main declarations #
Real.HolderTriple
: Predicate for two real numbers to be a Hölder triple.Real.HolderConjugate
: Predicate for two real numbers to be Hölder conjugate.Real.conjExponent
: Conjugate exponent of a real number.NNReal.HolderTriple
: Predicate for two nonnegative real numbers to be a Hölder triple.NNReal.HolderConjugate
: Predicate for two nonnegative real numbers to be Hölder conjugate.NNReal.conjExponent
: Conjugate exponent of a nonnegative real number.ENNReal.conjExponent
: Conjugate exponent of an extended nonnegative real number.
TODO #
- Eradicate the
1 / p
spelling in lemmas.
Real numbers p q : ℝ
are Hölder conjugate if they are positive and satisfy the
equality p⁻¹ + q⁻¹ = 1
. This is an abbreviation for Real.HolderTriple p q 1
. This condition
shows up in many theorems in analysis, notably related to L^p
norms.
It is equivalent that 1 < p
and p⁻¹ + q⁻¹ = 1
. See Real.holderConjugate_iff
.
Equations
- p.HolderConjugate q = p.HolderTriple q 1
Instances For
The conjugate exponent of p
is q = p / (p-1)
, so that p⁻¹ + q⁻¹ = 1
.
Equations
- p.conjExponent = p / (p - 1)
Instances For
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
Nonnegative real numbers p q : ℝ≥0
are Hölder conjugate if they are positive and satisfy
the equality p⁻¹ + q⁻¹ = 1
. This is an abbreviation for NNReal.HolderTriple p q 1
. This
condition shows up in many theorems in analysis, notably related to L^p
norms.
It is equivalent that 1 < p
and p⁻¹ + q⁻¹ = 1
. See NNReal.holderConjugate_iff
.
Equations
- p.HolderConjugate q = p.HolderTriple q 1
Instances For
The conjugate exponent of p
is q = p/(p-1)
, so that p⁻¹ + q⁻¹ = 1
.
Equations
- p.conjExponent = p / (p - 1)
Instances For
Alias of the reverse direction of NNReal.holderTriple_coe_iff
.
Alias of the reverse direction of NNReal.holderConjugate_coe_iff
.
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
For r
, instead of p
The conjugate exponent of p
is q = 1 + (p - 1)⁻¹
, so that p⁻¹ + q⁻¹ = 1
.
Equations
- p.conjExponent = 1 + (p - 1)⁻¹
Instances For
Alias of the reverse direction of ENNReal.holderTriple_coe_iff
.
Alias of the reverse direction of ENNReal.holderConjugate_coe_iff
.
Alias of Real.HolderConjugate
.
Real numbers p q : ℝ
are Hölder conjugate if they are positive and satisfy the
equality p⁻¹ + q⁻¹ = 1
. This is an abbreviation for Real.HolderTriple p q 1
. This condition
shows up in many theorems in analysis, notably related to L^p
norms.
It is equivalent that 1 < p
and p⁻¹ + q⁻¹ = 1
. See Real.holderConjugate_iff
.
Equations
Instances For
Alias of Real.holderConjugate_iff
.
Alias of Real.HolderTriple.lt
.
Alias of Real.HolderConjugate.inv_add_inv_eq_one
.
Alias of Real.HolderTriple.pos
.
Alias of Real.HolderTriple.nonneg
.
Alias of Real.HolderTriple.ne_zero
.
Alias of Real.HolderConjugate.sub_one_pos
.
Alias of Real.HolderConjugate.sub_one_ne_zero
.
Alias of Real.HolderTriple.inv_pos
.
Alias of Real.HolderTriple.inv_nonneg
.
Alias of Real.HolderTriple.inv_ne_zero
.
Alias of Real.HolderTriple.one_div_pos
.
Alias of Real.HolderTriple.one_div_nonneg
.
Alias of Real.HolderTriple.one_div_ne_zero
.
Alias of Real.HolderConjugate.conjugate_eq
.
Alias of Real.HolderConjugate.conjExponent_eq
.
Alias of Real.HolderConjugate.one_sub_inv
.
Alias of Real.HolderConjugate.inv_sub_one
.
Alias of Real.HolderConjugate.sub_one_mul_conj
.
Alias of Real.HolderConjugate.mul_eq_add
.
Alias of Real.HolderConjugate.symm
.
Alias of Real.HolderConjugate.div_conj_eq_sub_one
.
Alias of Real.HolderConjugate.inv_inv
.
Alias of Real.HolderConjugate.inv_one_sub_inv
.
Alias of Real.HolderConjugate.one_sub_inv_inv
.
Alias of Real.HolderConjugate.inv_add_inv_ennreal
.
Alias of Real.holderConjugate_comm
.
Alias of Real.holderConjugate_iff_eq_conjExponent
.
Alias of Real.HolderConjugate.conjExponent
.
Alias of Real.holderConjugate_one_div
.
Alias of NNReal.HolderConjugate
.
Nonnegative real numbers p q : ℝ≥0
are Hölder conjugate if they are positive and satisfy
the equality p⁻¹ + q⁻¹ = 1
. This is an abbreviation for NNReal.HolderTriple p q 1
. This
condition shows up in many theorems in analysis, notably related to L^p
norms.
It is equivalent that 1 < p
and p⁻¹ + q⁻¹ = 1
. See NNReal.holderConjugate_iff
.
Equations
Instances For
Alias of NNReal.holderConjugate_iff
.
Alias of NNReal.HolderTriple.lt
.
Alias of NNReal.holderConjugate_coe_iff
.
Alias of the reverse direction of NNReal.holderConjugate_coe_iff
.
Alias of the reverse direction of NNReal.holderConjugate_coe_iff
.
Alias of NNReal.HolderTriple.lt
.
Alias of NNReal.HolderTriple.pos
.
Alias of NNReal.HolderTriple.nonneg
.
Alias of NNReal.HolderTriple.ne_zero
.
Alias of NNReal.HolderConjugate.sub_one_pos
.
Alias of NNReal.HolderConjugate.sub_one_ne_zero
.
Alias of NNReal.HolderTriple.inv_pos
.
Alias of NNReal.HolderTriple.inv_nonneg
.
Alias of NNReal.HolderTriple.inv_ne_zero
.
Alias of NNReal.HolderTriple.one_div_pos
.
Alias of NNReal.HolderTriple.one_div_nonneg
.
Alias of NNReal.HolderTriple.one_div_ne_zero
.
Alias of NNReal.HolderConjugate.conjugate_eq
.
Alias of NNReal.HolderConjugate.conjExponent_eq
.
Alias of NNReal.HolderConjugate.one_sub_inv
.
Alias of NNReal.HolderConjugate.sub_one_mul_conj
.
Alias of NNReal.HolderConjugate.mul_eq_add
.
Alias of NNReal.HolderConjugate.symm
.
Alias of NNReal.HolderConjugate.inv_inv
.
Alias of NNReal.HolderConjugate.inv_one_sub_inv
.
Alias of NNReal.HolderConjugate.one_sub_inv_inv
.
Alias of NNReal.holderConjugate_comm
.
Alias of NNReal.HolderConjugate.conjExponent
.
Alias of NNReal.holderConjugate_one_div
.
Alias of Real.HolderTriple.toNNReal
.
Alias of ENNReal.HolderConjugate
.
An abbreviation for ENNReal.HolderTriple p q 1
, this class states p⁻¹ + q⁻¹ = 1
.
Instances For
Alias of ENNReal.holderConjugate_iff
.
Alias of ENNReal.holderConjugate_coe_iff
.
Alias of the reverse direction of ENNReal.holderConjugate_coe_iff
.
Alias of the reverse direction of ENNReal.holderConjugate_coe_iff
.
Alias of ENNReal.HolderConjugate.conjExponent
.
Alias of ENNReal.HolderConjugate.symm
.
Alias of ENNReal.HolderTriple.le
.
Alias of ENNReal.HolderConjugate.pos
.
Alias of ENNReal.HolderConjugate.ne_zero
.
Alias of ENNReal.HolderConjugate.one_sub_inv
.
Alias of ENNReal.HolderConjugate.conjExponent_eq
.
Alias of ENNReal.HolderConjugate.conj_eq
.
Alias of ENNReal.HolderConjugate.mul_eq_add
.
Alias of ENNReal.HolderConjugate.inv_inv
.
Alias of ENNReal.HolderConjugate.inv_one_sub_inv
.
Alias of ENNReal.HolderConjugate.one_sub_inv_inv
.
Alias of ENNReal.HolderConjugate.top_one
.
Alias of ENNReal.HolderConjugate.one_top
.