# 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.

source
structure Real.HolderTriple (p q r : ℝ) :
Prop

Real numbers `p q r : ℝ` are said to be a Hölder triple if `p` and `q` are positive and `p⁻¹ + q⁻¹ = r⁻¹`.

- inv_add_inv_eq_inv : p⁻¹ + q⁻¹ = r⁻¹
- left_pos : 0 < p
- right_pos : 0 < q

Instances For

source
theorem Real.holderTriple_iff (p q r : ℝ) :
p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
source
@[reducible, inline]
abbrev Real.HolderConjugate (p q : ℝ) :
Prop

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

source
def Real.conjExponent (p : ℝ) :
ℝ

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

Equations

- p.conjExponent = p / (p - 1)

Instances For

source
theorem Real.HolderTriple.of_pos {p q : ℝ} (hp : 0 < p) (hq : 0 < q) :
p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹
source
theorem Real.HolderTriple.symm {p q r : ℝ} (h : p.HolderTriple q r) :
q.HolderTriple p r
source
theorem Real.HolderTriple.pos {p q r : ℝ} (h : p.HolderTriple q r) :
0 < p
source
theorem Real.HolderTriple.nonneg {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ p
source
theorem Real.HolderTriple.ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :
p ≠ 0
source
theorem Real.HolderTriple.inv_pos {p q r : ℝ} (h : p.HolderTriple q r) :
0 < p⁻¹
source
theorem Real.HolderTriple.inv_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ p⁻¹
source
theorem Real.HolderTriple.inv_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :
p⁻¹ ≠ 0
source
theorem Real.HolderTriple.one_div_pos {p q r : ℝ} (h : p.HolderTriple q r) :
0 < 1 / p
source
theorem Real.HolderTriple.one_div_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ 1 / p
source
theorem Real.HolderTriple.one_div_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :
1 / p ≠ 0
source
theorem Real.HolderTriple.pos' {p q r : ℝ} (h : p.HolderTriple q r) :
0 < r

For `r`, instead of `p`

source
theorem Real.HolderTriple.nonneg' {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ r

For `r`, instead of `p`

source
theorem Real.HolderTriple.ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) :
r ≠ 0

For `r`, instead of `p`

source
theorem Real.HolderTriple.inv_pos' {p q r : ℝ} (h : p.HolderTriple q r) :
0 < r⁻¹

For `r`, instead of `p`

source
theorem Real.HolderTriple.inv_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ r⁻¹

For `r`, instead of `p`

source
theorem Real.HolderTriple.inv_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) :
r⁻¹ ≠ 0

For `r`, instead of `p`

source
theorem Real.HolderTriple.one_div_pos' {p q r : ℝ} (h : p.HolderTriple q r) :
0 < 1 / r

For `r`, instead of `p`

source
theorem Real.HolderTriple.one_div_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) :
0 ≤ 1 / r

For `r`, instead of `p`

source
theorem Real.HolderTriple.one_div_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) :
1 / r ≠ 0

For `r`, instead of `p`

source
theorem Real.HolderTriple.inv_eq {p q r : ℝ} (h : p.HolderTriple q r) :
r⁻¹ = p⁻¹ + q⁻¹
source
theorem Real.HolderTriple.one_div_add_one_div {p q r : ℝ} (h : p.HolderTriple q r) :
1 / p + 1 / q = 1 / r
source
theorem Real.HolderTriple.one_div_eq {p q r : ℝ} (h : p.HolderTriple q r) :
1 / r = 1 / p + 1 / q
source
theorem Real.HolderTriple.inv_inv_add_inv {p q r : ℝ} (h : p.HolderTriple q r) :
(p⁻¹ + q⁻¹)⁻¹ = r
source
theorem Real.HolderTriple.inv_lt_inv {p q r : ℝ} (h : p.HolderTriple q r) :
p⁻¹ < r⁻¹
source
theorem Real.HolderTriple.lt {p q r : ℝ} (h : p.HolderTriple q r) :
r < p
source
theorem Real.HolderTriple.inv_sub_inv_eq_inv {p q r : ℝ} (h : p.HolderTriple q r) :
r⁻¹ - q⁻¹ = p⁻¹
source
theorem Real.HolderTriple.holderConjugate_div_div {p q r : ℝ} (h : p.HolderTriple q r) :
(p / r).HolderConjugate (q / r)
source
theorem Real.HolderConjugate.two_two :
HolderConjugate 2 2
source
theorem Real.HolderConjugate.symm {p q : ℝ} (h : p.HolderConjugate q) :
q.HolderConjugate p
source
theorem Real.HolderConjugate.inv_add_inv_eq_one {p q : ℝ} (h : p.HolderConjugate q) :
p⁻¹ + q⁻¹ = 1
source
theorem Real.HolderConjugate.sub_one_pos {p q : ℝ} (h : p.HolderConjugate q) :
0 < p - 1
source
theorem Real.HolderConjugate.sub_one_ne_zero {p q : ℝ} (h : p.HolderConjugate q) :
p - 1 ≠ 0
source
theorem Real.HolderConjugate.conjugate_eq {p q : ℝ} (h : p.HolderConjugate q) :
q = p / (p - 1)
source
theorem Real.HolderConjugate.conjExponent_eq {p q : ℝ} (h : p.HolderConjugate q) :
p.conjExponent = q
source
theorem Real.HolderConjugate.one_sub_inv {p q : ℝ} (h : p.HolderConjugate q) :
1 - p⁻¹ = q⁻¹
source
theorem Real.HolderConjugate.inv_sub_one {p q : ℝ} (h : p.HolderConjugate q) :
p⁻¹ - 1 = -q⁻¹
source
theorem Real.HolderConjugate.sub_one_mul_conj {p q : ℝ} (h : p.HolderConjugate q) :
(p - 1) * q = p
source
theorem Real.HolderConjugate.mul_eq_add {p q : ℝ} (h : p.HolderConjugate q) :
p * q = p + q
source
theorem Real.HolderConjugate.div_conj_eq_sub_one {p q : ℝ} (h : p.HolderConjugate q) :
p / q = p - 1
source
theorem Real.HolderConjugate.inv_add_inv_ennreal {p q : ℝ} (h : p.HolderConjugate q) :
(ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
source
theorem Real.holderConjugate_iff {p q : ℝ} :
p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
source
theorem Real.HolderConjugate.inv_inv {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
a⁻¹.HolderConjugate b⁻¹
source
theorem Real.HolderConjugate.inv_one_sub_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :
a⁻¹.HolderConjugate (1 - a)⁻¹
source
theorem Real.HolderConjugate.one_sub_inv_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :
(1 - a)⁻¹.HolderConjugate a⁻¹
source
theorem Real.holderConjugate_comm {p q : ℝ} :
p.HolderConjugate q ↔ q.HolderConjugate p
source
theorem Real.holderConjugate_iff_eq_conjExponent {p q : ℝ} (hp : 1 < p) :
p.HolderConjugate q ↔ q = p / (p - 1)
source
theorem Real.HolderConjugate.conjExponent {p : ℝ} (h : 1 < p) :
p.HolderConjugate p.conjExponent
source
theorem Real.holderConjugate_one_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
(1 / a).HolderConjugate (1 / b)
source
structure NNReal.HolderTriple (p q r : NNReal) :
Prop

Nonnegative real numbers `p q r : ℝ≥0` are said to be a Hölder triple if `p` and `q` are positive and `p⁻¹ + q⁻¹ = r⁻¹`.

- inv_add_inv_eq_inv : p⁻¹ + q⁻¹ = r⁻¹
- left_pos : 0 < p
- right_pos : 0 < q

Instances For

source
theorem NNReal.holderTriple_iff (p q r : NNReal) :
p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
source
@[reducible, inline]
abbrev NNReal.HolderConjugate (p q : NNReal) :
Prop

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

source
def NNReal.conjExponent (p : NNReal) :
NNReal

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

Equations

- p.conjExponent = p / (p - 1)

Instances For

source
@[simp]
theorem NNReal.holderTriple_coe_iff {p q r : NNReal} :
(↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r
source
theorem NNReal.HolderTriple.coe {p q r : NNReal} :
p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r

Alias of the reverse direction of `NNReal.holderTriple_coe_iff`.

source
@[simp]
theorem NNReal.holderConjugate_coe_iff {p q : NNReal} :
(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q
source
theorem NNReal.HolderConjugate.coe {p q : NNReal} :
p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of `NNReal.holderConjugate_coe_iff`.

source
theorem NNReal.HolderTriple.of_pos {p q : NNReal} (hp : 0 < p) (hq : 0 < q) :
p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹
source
theorem NNReal.HolderTriple.symm {p q r : NNReal} (h : p.HolderTriple q r) :
q.HolderTriple p r
source
theorem NNReal.HolderTriple.pos {p q r : NNReal} (h : p.HolderTriple q r) :
0 < p
source
theorem NNReal.HolderTriple.nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ p
source
theorem NNReal.HolderTriple.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
p ≠ 0
source
theorem NNReal.HolderTriple.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) :
0 < p⁻¹
source
theorem NNReal.HolderTriple.inv_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ p⁻¹
source
theorem NNReal.HolderTriple.inv_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
p⁻¹ ≠ 0
source
theorem NNReal.HolderTriple.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) :
0 < 1 / p
source
theorem NNReal.HolderTriple.one_div_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ 1 / p
source
theorem NNReal.HolderTriple.one_div_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
1 / p ≠ 0
source
theorem NNReal.HolderTriple.pos' {p q r : NNReal} (h : p.HolderTriple q r) :
0 < r

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ r

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :
r ≠ 0

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.inv_pos' {p q r : NNReal} (h : p.HolderTriple q r) :
0 < r⁻¹

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.inv_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ r⁻¹

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.inv_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :
r⁻¹ ≠ 0

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.one_div_pos' {p q r : NNReal} (h : p.HolderTriple q r) :
0 < 1 / r

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.one_div_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :
0 ≤ 1 / r

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.one_div_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :
1 / r ≠ 0

For `r`, instead of `p`

source
theorem NNReal.HolderTriple.inv_eq {p q r : NNReal} (h : p.HolderTriple q r) :
r⁻¹ = p⁻¹ + q⁻¹
source
theorem NNReal.HolderTriple.one_div_add_one_div {p q r : NNReal} (h : p.HolderTriple q r) :
1 / p + 1 / q = 1 / r
source
theorem NNReal.HolderTriple.one_div_eq {p q r : NNReal} (h : p.HolderTriple q r) :
1 / r = 1 / p + 1 / q
source
theorem NNReal.HolderTriple.inv_inv_add_inv {p q r : NNReal} (h : p.HolderTriple q r) :
(p⁻¹ + q⁻¹)⁻¹ = r
source
theorem NNReal.HolderTriple.inv_lt_inv {p q r : NNReal} (h : p.HolderTriple q r) :
p⁻¹ < r⁻¹
source
theorem NNReal.HolderTriple.lt {p q r : NNReal} (h : p.HolderTriple q r) :
r < p
source
theorem NNReal.HolderTriple.inv_sub_inv_eq_inv {p q r : NNReal} (h : p.HolderTriple q r) :
r⁻¹ - q⁻¹ = p⁻¹
source
theorem NNReal.HolderTriple.holderConjugate_div_div {p q r : NNReal} (h : p.HolderTriple q r) :
(p / r).HolderConjugate (q / r)
source
theorem NNReal.HolderConjugate.two_two :
HolderConjugate 2 2
source
theorem NNReal.HolderConjugate.symm {p q : NNReal} (h : p.HolderConjugate q) :
q.HolderConjugate p
source
theorem NNReal.HolderConjugate.inv_add_inv_eq_one {p q : NNReal} (h : p.HolderConjugate q) :
p⁻¹ + q⁻¹ = 1
source
theorem NNReal.HolderConjugate.sub_one_pos {p q : NNReal} (h : p.HolderConjugate q) :
0 < p - 1
source
theorem NNReal.HolderConjugate.sub_one_ne_zero {p q : NNReal} (h : p.HolderConjugate q) :
p - 1 ≠ 0
source
theorem NNReal.HolderConjugate.conjugate_eq {p q : NNReal} (h : p.HolderConjugate q) :
q = p / (p - 1)
source
theorem NNReal.HolderConjugate.conjExponent_eq {p q : NNReal} (h : p.HolderConjugate q) :
p.conjExponent = q
source
theorem NNReal.HolderConjugate.one_sub_inv {p q : NNReal} (h : p.HolderConjugate q) :
1 - p⁻¹ = q⁻¹
source
theorem NNReal.HolderConjugate.sub_one_mul_conj {p q : NNReal} (h : p.HolderConjugate q) :
(p - 1) * q = p
source
theorem NNReal.HolderConjugate.mul_eq_add {p q : NNReal} (h : p.HolderConjugate q) :
p * q = p + q
source
theorem NNReal.HolderConjugate.div_conj_eq_sub_one {p q : NNReal} (h : p.HolderConjugate q) :
p / q = p - 1
source
theorem NNReal.HolderConjugate.inv_add_inv_ennreal {p q : NNReal} (h : p.HolderConjugate q) :
↑p⁻¹ + ↑q⁻¹ = 1
source
theorem NNReal.holderConjugate_iff {p q : NNReal} :
p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
source
theorem NNReal.HolderConjugate.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
a⁻¹.HolderConjugate b⁻¹
source
theorem NNReal.HolderConjugate.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :
a⁻¹.HolderConjugate (1 - a)⁻¹
source
theorem NNReal.HolderConjugate.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :
(1 - a)⁻¹.HolderConjugate a⁻¹
source
theorem NNReal.holderConjugate_comm {p q : NNReal} :
p.HolderConjugate q ↔ q.HolderConjugate p
source
theorem NNReal.holderConjugate_iff_eq_conjExponent {p q : NNReal} (hp : 1 < p) :
p.HolderConjugate q ↔ q = p / (p - 1)
source
theorem NNReal.HolderConjugate.conjExponent {p : NNReal} (h : 1 < p) :
p.HolderConjugate p.conjExponent
source
theorem NNReal.holderConjugate_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
(1 / a).HolderConjugate (1 / b)
source
theorem Real.HolderTriple.toNNReal {p q r : ℝ} (h : p.HolderTriple q r) :
p.toNNReal.HolderTriple q.toNNReal r.toNNReal
source
theorem Real.HolderConjugate.toNNReal {p q : ℝ} (h : p.HolderConjugate q) :
p.toNNReal.HolderConjugate q.toNNReal
source
noncomputable def ENNReal.conjExponent (p : ENNReal) :
ENNReal

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

Equations

- p.conjExponent = 1 + (p - 1)⁻¹

Instances For

source
theorem ENNReal.coe_conjExponent {p : NNReal} (hp : 1 < p) :
↑p.conjExponent = (↑p).conjExponent
source
@[simp]
theorem ENNReal.holderTriple_coe_iff {p q r : NNReal} (hr : r ≠ 0) :
(↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r
source
theorem NNReal.HolderTriple.coe_ennreal {p q r : NNReal} (hr : r ≠ 0) :
p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r

Alias of the reverse direction of `ENNReal.holderTriple_coe_iff`.

source
@[simp]
theorem ENNReal.holderConjugate_coe_iff {p q : NNReal} :
(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q
source
theorem NNReal.HolderConjugate.coe_ennreal {p q : NNReal} :
p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of `ENNReal.holderConjugate_coe_iff`.

source
theorem Real.HolderTriple.ennrealOfReal {p q r : ℝ} (h : p.HolderTriple q r) :
(ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)
source
theorem Real.HolderConjugate.ennrealOfReal {p q : ℝ} (h : p.HolderConjugate q) :
(ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)
source
theorem ENNReal.HolderTriple.of_toReal {p q r : ENNReal} (h : p.toReal.HolderTriple q.toReal r.toReal) :
p.HolderTriple q r
source
theorem ENNReal.HolderTriple.toReal_iff {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toReal) (hq : 0 < q.toReal) :
p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
source
theorem ENNReal.HolderTriple.toReal {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toReal) (hq : 0 < q.toReal) [p.HolderTriple q r] :
p.toReal.HolderTriple q.toReal r.toReal
source
theorem ENNReal.HolderTriple.of_toNNReal {p q r : ENNReal} (h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal) :
p.HolderTriple q r
source
theorem ENNReal.HolderTriple.toNNReal_iff {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) :
p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r
source
theorem ENNReal.HolderTriple.toNNReal {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) [p.HolderTriple q r] :
p.toNNReal.HolderTriple q.toNNReal r.toNNReal
source
theorem ENNReal.HolderConjugate.of_toReal {p q : ENNReal} (h : p.toReal.HolderConjugate q.toReal) :
p.HolderConjugate q
source
theorem ENNReal.HolderConjugate.toReal_iff {p q : ENNReal} (hp : 1 < p.toReal) :
p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q
source
theorem ENNReal.HolderConjugate.toReal {p q : ENNReal} (hp : 1 < p.toReal) [p.HolderConjugate q] :
p.toReal.HolderConjugate q.toReal
source
theorem ENNReal.HolderConjugate.of_toNNReal {p q : ENNReal} (h : p.toNNReal.HolderConjugate q.toNNReal) :
p.HolderConjugate q
source
theorem ENNReal.HolderConjugate.toNNReal_iff {p q : ENNReal} (hp : 1 < p.toNNReal) :
p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q
source
theorem ENNReal.HolderConjugate.toNNReal {p q : ENNReal} (hp : 1 < p.toNNReal) [p.HolderConjugate q] :
p.toNNReal.HolderConjugate q.toNNReal
source
theorem ENNReal.HolderConjugate.conjExponent {p : ENNReal} (hp : 1 ≤ p) :
p.HolderConjugate p.conjExponent
source
instance ENNReal.HolderConjugate.instConjExponentOfFactLeOfNat {p : ENNReal} [Fact (1 ≤ p)] :
p.HolderConjugate p.conjExponent
source
theorem ENNReal.HolderConjugate.conjExponent_eq {p q : ENNReal} [h : p.HolderConjugate q] :
p.conjExponent = q
source
theorem ENNReal.HolderConjugate.conj_eq {p q : ENNReal} [h : p.HolderConjugate q] :
q = 1 + (p - 1)⁻¹
source
theorem ENNReal.HolderConjugate.mul_eq_add {p q : ENNReal} [h : p.HolderConjugate q] :
p * q = p + q
source
theorem ENNReal.HolderConjugate.div_conj_eq_sub_one {p q : ENNReal} [h : p.HolderConjugate q] :
p / q = p - 1
source
theorem ENNReal.HolderConjugate.inv_inv {a b : ENNReal} (hab : a + b = 1) :
a⁻¹.HolderConjugate b⁻¹
source
theorem ENNReal.HolderConjugate.inv_one_sub_inv {a : ENNReal} (ha : a ≤ 1) :
a⁻¹.HolderConjugate (1 - a)⁻¹
source
theorem ENNReal.HolderConjugate.inv_one_sub_inv' {a : ENNReal} (ha : 1 ≤ a) :
a.HolderConjugate (1 - a⁻¹)⁻¹
source
theorem ENNReal.HolderConjugate.one_sub_inv_inv {a : ENNReal} (ha : a ≤ 1) :
(1 - a)⁻¹.HolderConjugate a⁻¹
source
theorem ENNReal.HolderConjugate.top_one :
⊤.HolderConjugate 1
source
theorem ENNReal.HolderConjugate.one_top :
HolderConjugate 1 ⊤
source
theorem ENNReal.isConjExponent_comm {p q : ENNReal} :
p.HolderConjugate q ↔ q.HolderConjugate p
source
theorem ENNReal.isConjExponent_iff_eq_conjExponent {p q : ENNReal} (hp : 1 ≤ p) :
p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹