Documentation

Mathlib.Data.Real.ConjExponents

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.

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

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

theorem Real.holderTriple_iff (p q r : ℝ) :

p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q

@[reducible, inline]

abbrev Real.HolderConjugate (p q : ℝ) :

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

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)

theorem Real.HolderTriple.of_pos {p q : ℝ} (hp : 0 < p) (hq : 0 < q) :

p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹

theorem Real.HolderTriple.symm {p q r : ℝ} (h : p.HolderTriple q r) :

q.HolderTriple p r

theorem Real.HolderTriple.pos {p q r : ℝ} (h : p.HolderTriple q r) :

0 < p

theorem Real.HolderTriple.nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

0 ≤ p

theorem Real.HolderTriple.ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

p ≠ 0

theorem Real.HolderTriple.inv_pos {p q r : ℝ} (h : p.HolderTriple q r) :

theorem Real.HolderTriple.inv_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

theorem Real.HolderTriple.inv_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

theorem Real.HolderTriple.one_div_pos {p q r : ℝ} (h : p.HolderTriple q r) :

0 < 1 / p

theorem Real.HolderTriple.one_div_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

0 ≤ 1 / p

theorem Real.HolderTriple.one_div_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

1 / p ≠ 0

theorem Real.HolderTriple.pos' {p q r : ℝ} (h : p.HolderTriple q r) :

0 < r

For r, instead of p

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

0 ≤ r

For r, instead of p

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

r ≠ 0

For r, instead of p

theorem Real.HolderTriple.inv_pos' {p q r : ℝ} (h : p.HolderTriple q r) :

For r, instead of p

theorem Real.HolderTriple.inv_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) :

For r, instead of p

theorem Real.HolderTriple.inv_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) :

For r, instead of p

theorem Real.HolderTriple.one_div_pos' {p q r : ℝ} (h : p.HolderTriple q r) :

0 < 1 / r

For r, instead of p

theorem Real.HolderTriple.one_div_nonneg' {p q r : ℝ} (h : p.HolderTriple q r) :

0 ≤ 1 / r

For r, instead of p

theorem Real.HolderTriple.one_div_ne_zero' {p q r : ℝ} (h : p.HolderTriple q r) :

1 / r ≠ 0

For r, instead of p

theorem Real.HolderTriple.inv_eq {p q r : ℝ} (h : p.HolderTriple q r) :

r⁻¹ = p⁻¹ + q⁻¹

theorem Real.HolderTriple.one_div_add_one_div {p q r : ℝ} (h : p.HolderTriple q r) :

1 / p + 1 / q = 1 / r

theorem Real.HolderTriple.one_div_eq {p q r : ℝ} (h : p.HolderTriple q r) :

1 / r = 1 / p + 1 / q

theorem Real.HolderTriple.inv_inv_add_inv {p q r : ℝ} (h : p.HolderTriple q r) :

(p⁻¹ + q⁻¹)⁻¹ = r

theorem Real.HolderTriple.inv_lt_inv {p q r : ℝ} (h : p.HolderTriple q r) :

p⁻¹ < r⁻¹

theorem Real.HolderTriple.lt {p q r : ℝ} (h : p.HolderTriple q r) :

r < p

theorem Real.HolderTriple.inv_sub_inv_eq_inv {p q r : ℝ} (h : p.HolderTriple q r) :

r⁻¹ - q⁻¹ = p⁻¹

theorem Real.HolderTriple.holderConjugate_div_div {p q r : ℝ} (h : p.HolderTriple q r) :

(p / r).HolderConjugate (q / r)

theorem Real.HolderConjugate.two_two :

HolderConjugate 2 2

theorem Real.HolderConjugate.symm {p q : ℝ} (h : p.HolderConjugate q) :

q.HolderConjugate p

theorem Real.HolderConjugate.inv_add_inv_eq_one {p q : ℝ} (h : p.HolderConjugate q) :

p⁻¹ + q⁻¹ = 1

theorem Real.HolderConjugate.sub_one_pos {p q : ℝ} (h : p.HolderConjugate q) :

0 < p - 1

theorem Real.HolderConjugate.sub_one_ne_zero {p q : ℝ} (h : p.HolderConjugate q) :

p - 1 ≠ 0

theorem Real.HolderConjugate.conjugate_eq {p q : ℝ} (h : p.HolderConjugate q) :

q = p / (p - 1)

theorem Real.HolderConjugate.conjExponent_eq {p q : ℝ} (h : p.HolderConjugate q) :

p.conjExponent = q

theorem Real.HolderConjugate.one_sub_inv {p q : ℝ} (h : p.HolderConjugate q) :

1 - p⁻¹ = q⁻¹

theorem Real.HolderConjugate.inv_sub_one {p q : ℝ} (h : p.HolderConjugate q) :

p⁻¹ - 1 = -q⁻¹

theorem Real.HolderConjugate.sub_one_mul_conj {p q : ℝ} (h : p.HolderConjugate q) :

(p - 1) * q = p

theorem Real.HolderConjugate.mul_eq_add {p q : ℝ} (h : p.HolderConjugate q) :

p * q = p + q

theorem Real.HolderConjugate.div_conj_eq_sub_one {p q : ℝ} (h : p.HolderConjugate q) :

p / q = p - 1

theorem Real.HolderConjugate.inv_add_inv_ennreal {p q : ℝ} (h : p.HolderConjugate q) :

(ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

theorem Real.holderConjugate_iff {p q : ℝ} :

p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

theorem Real.HolderConjugate.inv_inv {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

theorem Real.HolderConjugate.inv_one_sub_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

theorem Real.HolderConjugate.one_sub_inv_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

theorem Real.holderConjugate_comm {p q : ℝ} :

p.HolderConjugate q ↔ q.HolderConjugate p

theorem Real.holderConjugate_iff_eq_conjExponent {p q : ℝ} (hp : 1 < p) :

p.HolderConjugate q ↔ q = p / (p - 1)

theorem Real.HolderConjugate.conjExponent {p : ℝ} (h : 1 < p) :

p.HolderConjugate p.conjExponent

theorem Real.holderConjugate_one_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

(1 / a).HolderConjugate (1 / b)

structure NNReal.HolderTriple (p q r : NNReal) :

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

theorem NNReal.holderTriple_iff (p q r : NNReal) :

p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q

@[reducible, inline]

abbrev NNReal.HolderConjugate (p q : NNReal) :

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

def NNReal.conjExponent (p : NNReal) :

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

Equations

p.conjExponent = p / (p - 1)

@[simp]

theorem NNReal.holderTriple_coe_iff {p q r : NNReal} :

(↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

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.

@[simp]

theorem NNReal.holderConjugate_coe_iff {p q : NNReal} :

(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

theorem NNReal.HolderConjugate.coe {p q : NNReal} :

p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

theorem NNReal.HolderTriple.of_pos {p q : NNReal} (hp : 0 < p) (hq : 0 < q) :

p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹

theorem NNReal.HolderTriple.symm {p q r : NNReal} (h : p.HolderTriple q r) :

q.HolderTriple p r

theorem NNReal.HolderTriple.pos {p q r : NNReal} (h : p.HolderTriple q r) :

0 < p

theorem NNReal.HolderTriple.nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

0 ≤ p

theorem NNReal.HolderTriple.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

p ≠ 0

theorem NNReal.HolderTriple.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) :

theorem NNReal.HolderTriple.inv_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

theorem NNReal.HolderTriple.inv_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

theorem NNReal.HolderTriple.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) :

0 < 1 / p

theorem NNReal.HolderTriple.one_div_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

0 ≤ 1 / p

theorem NNReal.HolderTriple.one_div_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

1 / p ≠ 0

theorem NNReal.HolderTriple.pos' {p q r : NNReal} (h : p.HolderTriple q r) :

0 < r

For r, instead of p

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

0 ≤ r

For r, instead of p

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

r ≠ 0

For r, instead of p

theorem NNReal.HolderTriple.inv_pos' {p q r : NNReal} (h : p.HolderTriple q r) :

For r, instead of p

theorem NNReal.HolderTriple.inv_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :

For r, instead of p

theorem NNReal.HolderTriple.inv_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :

For r, instead of p

theorem NNReal.HolderTriple.one_div_pos' {p q r : NNReal} (h : p.HolderTriple q r) :

0 < 1 / r

For r, instead of p

theorem NNReal.HolderTriple.one_div_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :

0 ≤ 1 / r

For r, instead of p

theorem NNReal.HolderTriple.one_div_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :

1 / r ≠ 0

For r, instead of p

theorem NNReal.HolderTriple.inv_eq {p q r : NNReal} (h : p.HolderTriple q r) :

r⁻¹ = p⁻¹ + q⁻¹

theorem NNReal.HolderTriple.one_div_add_one_div {p q r : NNReal} (h : p.HolderTriple q r) :

1 / p + 1 / q = 1 / r

theorem NNReal.HolderTriple.one_div_eq {p q r : NNReal} (h : p.HolderTriple q r) :

1 / r = 1 / p + 1 / q

theorem NNReal.HolderTriple.inv_inv_add_inv {p q r : NNReal} (h : p.HolderTriple q r) :

(p⁻¹ + q⁻¹)⁻¹ = r

theorem NNReal.HolderTriple.inv_lt_inv {p q r : NNReal} (h : p.HolderTriple q r) :

p⁻¹ < r⁻¹

theorem NNReal.HolderTriple.lt {p q r : NNReal} (h : p.HolderTriple q r) :

r < p

theorem NNReal.HolderTriple.inv_sub_inv_eq_inv {p q r : NNReal} (h : p.HolderTriple q r) :

r⁻¹ - q⁻¹ = p⁻¹

theorem NNReal.HolderTriple.holderConjugate_div_div {p q r : NNReal} (h : p.HolderTriple q r) :

(p / r).HolderConjugate (q / r)

theorem NNReal.HolderConjugate.two_two :

HolderConjugate 2 2

theorem NNReal.HolderConjugate.symm {p q : NNReal} (h : p.HolderConjugate q) :

q.HolderConjugate p

theorem NNReal.HolderConjugate.inv_add_inv_eq_one {p q : NNReal} (h : p.HolderConjugate q) :

p⁻¹ + q⁻¹ = 1

theorem NNReal.HolderConjugate.sub_one_pos {p q : NNReal} (h : p.HolderConjugate q) :

0 < p - 1

theorem NNReal.HolderConjugate.sub_one_ne_zero {p q : NNReal} (h : p.HolderConjugate q) :

p - 1 ≠ 0

theorem NNReal.HolderConjugate.conjugate_eq {p q : NNReal} (h : p.HolderConjugate q) :

q = p / (p - 1)

theorem NNReal.HolderConjugate.conjExponent_eq {p q : NNReal} (h : p.HolderConjugate q) :

p.conjExponent = q

theorem NNReal.HolderConjugate.one_sub_inv {p q : NNReal} (h : p.HolderConjugate q) :

1 - p⁻¹ = q⁻¹

theorem NNReal.HolderConjugate.sub_one_mul_conj {p q : NNReal} (h : p.HolderConjugate q) :

(p - 1) * q = p

theorem NNReal.HolderConjugate.mul_eq_add {p q : NNReal} (h : p.HolderConjugate q) :

p * q = p + q

theorem NNReal.HolderConjugate.div_conj_eq_sub_one {p q : NNReal} (h : p.HolderConjugate q) :

p / q = p - 1

theorem NNReal.HolderConjugate.inv_add_inv_ennreal {p q : NNReal} (h : p.HolderConjugate q) :

↑p⁻¹ + ↑q⁻¹ = 1

theorem NNReal.holderConjugate_iff {p q : NNReal} :

p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

theorem NNReal.HolderConjugate.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

theorem NNReal.HolderConjugate.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

theorem NNReal.HolderConjugate.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

theorem NNReal.holderConjugate_comm {p q : NNReal} :

p.HolderConjugate q ↔ q.HolderConjugate p

theorem NNReal.holderConjugate_iff_eq_conjExponent {p q : NNReal} (hp : 1 < p) :

p.HolderConjugate q ↔ q = p / (p - 1)

theorem NNReal.HolderConjugate.conjExponent {p : NNReal} (h : 1 < p) :

p.HolderConjugate p.conjExponent

theorem NNReal.holderConjugate_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

(1 / a).HolderConjugate (1 / b)

theorem Real.HolderTriple.toNNReal {p q r : ℝ} (h : p.HolderTriple q r) :

p.toNNReal.HolderTriple q.toNNReal r.toNNReal

theorem Real.HolderConjugate.toNNReal {p q : ℝ} (h : p.HolderConjugate q) :

p.toNNReal.HolderConjugate q.toNNReal

noncomputable def ENNReal.conjExponent (p : ENNReal) :

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

Equations

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

theorem ENNReal.coe_conjExponent {p : NNReal} (hp : 1 < p) :

↑p.conjExponent = (↑p).conjExponent

@[simp]

theorem ENNReal.holderTriple_coe_iff {p q r : NNReal} (hr : r ≠ 0) :

(↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

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.

@[simp]

theorem ENNReal.holderConjugate_coe_iff {p q : NNReal} :

(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

theorem NNReal.HolderConjugate.coe_ennreal {p q : NNReal} :

p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

theorem Real.HolderTriple.ennrealOfReal {p q r : ℝ} (h : p.HolderTriple q r) :

(ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)

theorem Real.HolderConjugate.ennrealOfReal {p q : ℝ} (h : p.HolderConjugate q) :

(ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)

theorem ENNReal.HolderTriple.of_toReal {p q r : ENNReal} (h : p.toReal.HolderTriple q.toReal r.toReal) :

p.HolderTriple q r

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

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

theorem ENNReal.HolderTriple.of_toNNReal {p q r : ENNReal} (h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal) :

p.HolderTriple q r

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

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

theorem ENNReal.HolderConjugate.of_toReal {p q : ENNReal} (h : p.toReal.HolderConjugate q.toReal) :

p.HolderConjugate q

theorem ENNReal.HolderConjugate.toReal_iff {p q : ENNReal} (hp : 1 < p.toReal) :

p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q

theorem ENNReal.HolderConjugate.toReal {p q : ENNReal} (hp : 1 < p.toReal) [p.HolderConjugate q] :

p.toReal.HolderConjugate q.toReal

theorem ENNReal.HolderConjugate.of_toNNReal {p q : ENNReal} (h : p.toNNReal.HolderConjugate q.toNNReal) :

p.HolderConjugate q

theorem ENNReal.HolderConjugate.toNNReal_iff {p q : ENNReal} (hp : 1 < p.toNNReal) :

p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q

theorem ENNReal.HolderConjugate.toNNReal {p q : ENNReal} (hp : 1 < p.toNNReal) [p.HolderConjugate q] :

p.toNNReal.HolderConjugate q.toNNReal

theorem ENNReal.HolderConjugate.conjExponent {p : ENNReal} (hp : 1 ≤ p) :

p.HolderConjugate p.conjExponent

instance ENNReal.HolderConjugate.instConjExponentOfFactLeOfNat {p : ENNReal} [Fact (1 ≤ p)] :

p.HolderConjugate p.conjExponent

theorem ENNReal.HolderConjugate.conjExponent_eq {p q : ENNReal} [h : p.HolderConjugate q] :

p.conjExponent = q

theorem ENNReal.HolderConjugate.conj_eq {p q : ENNReal} [h : p.HolderConjugate q] :

q = 1 + (p - 1)⁻¹

theorem ENNReal.HolderConjugate.mul_eq_add {p q : ENNReal} [h : p.HolderConjugate q] :

p * q = p + q

theorem ENNReal.HolderConjugate.div_conj_eq_sub_one {p q : ENNReal} [h : p.HolderConjugate q] :

p / q = p - 1

theorem ENNReal.HolderConjugate.inv_inv {a b : ENNReal} (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

theorem ENNReal.HolderConjugate.inv_one_sub_inv {a : ENNReal} (ha : a ≤ 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

theorem ENNReal.HolderConjugate.one_sub_inv_inv {a : ENNReal} (ha : a ≤ 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

theorem ENNReal.HolderConjugate.top_one :

⊤.HolderConjugate 1

theorem ENNReal.HolderConjugate.one_top :

HolderConjugate 1 ⊤

theorem ENNReal.isConjExponent_comm {p q : ENNReal} :

p.HolderConjugate q ↔ q.HolderConjugate p

theorem ENNReal.isConjExponent_iff_eq_conjExponent {p q : ENNReal} (hp : 1 ≤ p) :

p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹

@[deprecated Real.HolderConjugate (since := "2025-03-14")]

def Real.IsConjExponent (p q : ℝ) :

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

Real.IsConjExponent = Real.HolderConjugate

@[deprecated Real.holderConjugate_iff (since := "2025-03-14")]

theorem Real.isConjExponent_iff {p q : ℝ} :

p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Alias of Real.holderConjugate_iff.

@[deprecated Real.HolderTriple.lt (since := "2025-03-14")]

theorem Real.IsConjExponent.one_lt {p q r : ℝ} (h : p.HolderTriple q r) :

r < p

Alias of Real.HolderTriple.lt.

@[deprecated Real.HolderConjugate.inv_add_inv_eq_one (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_add_inv_conj {p q : ℝ} (h : p.HolderConjugate q) :

p⁻¹ + q⁻¹ = 1

Alias of Real.HolderConjugate.inv_add_inv_eq_one.

@[deprecated Real.HolderTriple.pos (since := "2025-03-14")]

theorem Real.IsConjExponent.pos {p q r : ℝ} (h : p.HolderTriple q r) :

0 < p

Alias of Real.HolderTriple.pos.

@[deprecated Real.HolderTriple.nonneg (since := "2025-03-14")]

theorem Real.IsConjExponent.nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

0 ≤ p

Alias of Real.HolderTriple.nonneg.

@[deprecated Real.HolderTriple.ne_zero (since := "2025-03-14")]

theorem Real.IsConjExponent.ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

p ≠ 0

Alias of Real.HolderTriple.ne_zero.

@[deprecated Real.HolderConjugate.sub_one_pos (since := "2025-03-14")]

theorem Real.IsConjExponent.sub_one_pos {p q : ℝ} (h : p.HolderConjugate q) :

0 < p - 1

Alias of Real.HolderConjugate.sub_one_pos.

@[deprecated Real.HolderConjugate.sub_one_ne_zero (since := "2025-03-14")]

theorem Real.IsConjExponent.sub_one_ne_zero {p q : ℝ} (h : p.HolderConjugate q) :

p - 1 ≠ 0

Alias of Real.HolderConjugate.sub_one_ne_zero.

@[deprecated Real.HolderTriple.inv_pos (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_pos {p q r : ℝ} (h : p.HolderTriple q r) :

Alias of Real.HolderTriple.inv_pos.

@[deprecated Real.HolderTriple.inv_nonneg (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

Alias of Real.HolderTriple.inv_nonneg.

@[deprecated Real.HolderTriple.inv_ne_zero (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

Alias of Real.HolderTriple.inv_ne_zero.

@[deprecated Real.HolderTriple.one_div_pos (since := "2025-03-14")]

theorem Real.IsConjExponent.one_div_pos {p q r : ℝ} (h : p.HolderTriple q r) :

0 < 1 / p

Alias of Real.HolderTriple.one_div_pos.

@[deprecated Real.HolderTriple.one_div_nonneg (since := "2025-03-14")]

theorem Real.IsConjExponent.one_div_nonneg {p q r : ℝ} (h : p.HolderTriple q r) :

0 ≤ 1 / p

Alias of Real.HolderTriple.one_div_nonneg.

@[deprecated Real.HolderTriple.one_div_ne_zero (since := "2025-03-14")]

theorem Real.IsConjExponent.one_div_ne_zero {p q r : ℝ} (h : p.HolderTriple q r) :

1 / p ≠ 0

Alias of Real.HolderTriple.one_div_ne_zero.

@[deprecated Real.HolderConjugate.conjugate_eq (since := "2025-03-14")]

theorem Real.IsConjExponent.conj_eq {p q : ℝ} (h : p.HolderConjugate q) :

q = p / (p - 1)

Alias of Real.HolderConjugate.conjugate_eq.

@[deprecated Real.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

theorem Real.IsConjExponent.conjExponent_eq {p q : ℝ} (h : p.HolderConjugate q) :

p.conjExponent = q

Alias of Real.HolderConjugate.conjExponent_eq.

@[deprecated Real.HolderConjugate.one_sub_inv (since := "2025-03-14")]

theorem Real.IsConjExponent.one_sub_inv {p q : ℝ} (h : p.HolderConjugate q) :

1 - p⁻¹ = q⁻¹

Alias of Real.HolderConjugate.one_sub_inv.

@[deprecated Real.HolderConjugate.inv_sub_one (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_sub_one {p q : ℝ} (h : p.HolderConjugate q) :

p⁻¹ - 1 = -q⁻¹

Alias of Real.HolderConjugate.inv_sub_one.

@[deprecated Real.HolderConjugate.sub_one_mul_conj (since := "2025-03-14")]

theorem Real.IsConjExponent.sub_one_mul_conj {p q : ℝ} (h : p.HolderConjugate q) :

(p - 1) * q = p

Alias of Real.HolderConjugate.sub_one_mul_conj.

@[deprecated Real.HolderConjugate.mul_eq_add (since := "2025-03-14")]

theorem Real.IsConjExponent.mul_eq_add {p q : ℝ} (h : p.HolderConjugate q) :

p * q = p + q

Alias of Real.HolderConjugate.mul_eq_add.

@[deprecated Real.HolderConjugate.symm (since := "2025-03-14")]

theorem Real.IsConjExponent.symm {p q : ℝ} (h : p.HolderConjugate q) :

q.HolderConjugate p

Alias of Real.HolderConjugate.symm.

@[deprecated Real.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]

theorem Real.IsConjExponent.div_conj_eq_sub_one {p q : ℝ} (h : p.HolderConjugate q) :

p / q = p - 1

Alias of Real.HolderConjugate.div_conj_eq_sub_one.

@[deprecated Real.HolderConjugate.inv_inv (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_inv {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

Alias of Real.HolderConjugate.inv_inv.

@[deprecated Real.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_one_sub_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

Alias of Real.HolderConjugate.inv_one_sub_inv.

@[deprecated Real.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]

theorem Real.IsConjExponent.one_sub_inv_inv {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

Alias of Real.HolderConjugate.one_sub_inv_inv.

@[deprecated Real.HolderConjugate.inv_add_inv_ennreal (since := "2025-03-14")]

theorem Real.IsConjExponent.inv_add_inv_conj_ennreal {p q : ℝ} (h : p.HolderConjugate q) :

(ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

Alias of Real.HolderConjugate.inv_add_inv_ennreal.

@[deprecated Real.holderConjugate_comm (since := "2025-03-14")]

theorem Real.isConjExponent_comm {p q : ℝ} :

p.HolderConjugate q ↔ q.HolderConjugate p

Alias of Real.holderConjugate_comm.

@[deprecated Real.holderConjugate_iff_eq_conjExponent (since := "2025-03-14")]

theorem Real.isConjExponent_iff_eq_conjExponent {p q : ℝ} (hp : 1 < p) :

p.HolderConjugate q ↔ q = p / (p - 1)

Alias of Real.holderConjugate_iff_eq_conjExponent.

@[deprecated Real.HolderConjugate.conjExponent (since := "2025-03-14")]

theorem Real.IsConjExponent.conjExponent {p : ℝ} (h : 1 < p) :

p.HolderConjugate p.conjExponent

Alias of Real.HolderConjugate.conjExponent.

@[deprecated Real.holderConjugate_one_div (since := "2025-03-14")]

theorem Real.isConjExponent_one_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

(1 / a).HolderConjugate (1 / b)

Alias of Real.holderConjugate_one_div.

@[deprecated NNReal.HolderConjugate (since := "2025-03-14")]

def NNReal.IsConjExponent (p q : NNReal) :

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

NNReal.IsConjExponent = NNReal.HolderConjugate

@[deprecated NNReal.holderConjugate_iff (since := "2025-03-14")]

theorem NNReal.isConjExponent_iff {p q : NNReal} :

p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Alias of NNReal.holderConjugate_iff.

@[deprecated NNReal.HolderTriple.lt (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_lt {p q r : NNReal} (h : p.HolderTriple q r) :

r < p

Alias of NNReal.HolderTriple.lt.

@[deprecated NNReal.HolderConjugate.inv_add_inv_eq_one (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_add_inv_conj {p q : NNReal} (h : p.HolderConjugate q) :

p⁻¹ + q⁻¹ = 1

Alias of NNReal.HolderConjugate.inv_add_inv_eq_one.

@[deprecated NNReal.holderConjugate_coe_iff (since := "2025-03-14")]

theorem NNReal.isConjExponent_coe {p q : NNReal} :

(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

Alias of NNReal.holderConjugate_coe_iff.

@[deprecated NNReal.HolderConjugate.coe (since := "2025-03-14")]

theorem NNReal.IsConjExponent.coe {p q : NNReal} :

p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

@[deprecated NNReal.HolderTriple.lt (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_le {p q r : NNReal} (h : p.HolderTriple q r) :

r < p

Alias of NNReal.HolderTriple.lt.

@[deprecated NNReal.HolderTriple.pos (since := "2025-03-14")]

theorem NNReal.IsConjExponent.pos {p q r : NNReal} (h : p.HolderTriple q r) :

0 < p

Alias of NNReal.HolderTriple.pos.

@[deprecated NNReal.HolderTriple.nonneg (since := "2025-03-14")]

theorem NNReal.IsConjExponent.nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

0 ≤ p

Alias of NNReal.HolderTriple.nonneg.

@[deprecated NNReal.HolderTriple.ne_zero (since := "2025-03-14")]

theorem NNReal.IsConjExponent.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

p ≠ 0

Alias of NNReal.HolderTriple.ne_zero.

@[deprecated NNReal.HolderConjugate.sub_one_pos (since := "2025-03-14")]

theorem NNReal.IsConjExponent.sub_one_pos {p q : NNReal} (h : p.HolderConjugate q) :

0 < p - 1

Alias of NNReal.HolderConjugate.sub_one_pos.

@[deprecated NNReal.HolderConjugate.sub_one_ne_zero (since := "2025-03-14")]

theorem NNReal.IsConjExponent.sub_one_ne_zero {p q : NNReal} (h : p.HolderConjugate q) :

p - 1 ≠ 0

Alias of NNReal.HolderConjugate.sub_one_ne_zero.

@[deprecated NNReal.HolderTriple.inv_pos (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) :

Alias of NNReal.HolderTriple.inv_pos.

@[deprecated NNReal.HolderTriple.inv_nonneg (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

Alias of NNReal.HolderTriple.inv_nonneg.

@[deprecated NNReal.HolderTriple.inv_ne_zero (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

Alias of NNReal.HolderTriple.inv_ne_zero.

@[deprecated NNReal.HolderTriple.one_div_pos (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) :

0 < 1 / p

Alias of NNReal.HolderTriple.one_div_pos.

@[deprecated NNReal.HolderTriple.one_div_nonneg (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_div_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :

0 ≤ 1 / p

Alias of NNReal.HolderTriple.one_div_nonneg.

@[deprecated NNReal.HolderTriple.one_div_ne_zero (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_div_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :

1 / p ≠ 0

Alias of NNReal.HolderTriple.one_div_ne_zero.

@[deprecated NNReal.HolderConjugate.conjugate_eq (since := "2025-03-14")]

theorem NNReal.IsConjExponent.conj_eq {p q : NNReal} (h : p.HolderConjugate q) :

q = p / (p - 1)

Alias of NNReal.HolderConjugate.conjugate_eq.

@[deprecated NNReal.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

theorem NNReal.IsConjExponent.conjExponent_eq {p q : NNReal} (h : p.HolderConjugate q) :

p.conjExponent = q

Alias of NNReal.HolderConjugate.conjExponent_eq.

@[deprecated NNReal.HolderConjugate.one_sub_inv (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_sub_inv {p q : NNReal} (h : p.HolderConjugate q) :

1 - p⁻¹ = q⁻¹

Alias of NNReal.HolderConjugate.one_sub_inv.

@[deprecated NNReal.HolderConjugate.sub_one_mul_conj (since := "2025-03-14")]

theorem NNReal.IsConjExponent.sub_one_mul_conj {p q : NNReal} (h : p.HolderConjugate q) :

(p - 1) * q = p

Alias of NNReal.HolderConjugate.sub_one_mul_conj.

@[deprecated NNReal.HolderConjugate.mul_eq_add (since := "2025-03-14")]

theorem NNReal.IsConjExponent.mul_eq_add {p q : NNReal} (h : p.HolderConjugate q) :

p * q = p + q

Alias of NNReal.HolderConjugate.mul_eq_add.

@[deprecated NNReal.HolderConjugate.symm (since := "2025-03-14")]

theorem NNReal.IsConjExponent.symm {p q : NNReal} (h : p.HolderConjugate q) :

q.HolderConjugate p

Alias of NNReal.HolderConjugate.symm.

@[deprecated NNReal.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]

theorem NNReal.IsConjExponent.div_conj_eq_sub_one {p q : NNReal} (h : p.HolderConjugate q) :

p / q = p - 1

Alias of NNReal.HolderConjugate.div_conj_eq_sub_one.

@[deprecated NNReal.HolderConjugate.inv_inv (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

Alias of NNReal.HolderConjugate.inv_inv.

@[deprecated NNReal.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

Alias of NNReal.HolderConjugate.inv_one_sub_inv.

@[deprecated NNReal.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]

theorem NNReal.IsConjExponent.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

Alias of NNReal.HolderConjugate.one_sub_inv_inv.

@[deprecated NNReal.HolderConjugate.inv_add_inv_ennreal (since := "2025-03-14")]

theorem NNReal.IsConjExponent.inv_add_inv_conj_ennreal {p q : NNReal} (h : p.HolderConjugate q) :

↑p⁻¹ + ↑q⁻¹ = 1

Alias of NNReal.HolderConjugate.inv_add_inv_ennreal.

@[deprecated NNReal.holderConjugate_comm (since := "2025-03-14")]

theorem NNReal.isConjExponent_comm {p q : NNReal} :

p.HolderConjugate q ↔ q.HolderConjugate p

Alias of NNReal.holderConjugate_comm.

@[deprecated NNReal.holderConjugate_iff_eq_conjExponent (since := "2025-03-14")]

theorem NNReal.isConjExponent_iff_eq_conjExponent {p q : NNReal} (hp : 1 < p) :

p.HolderConjugate q ↔ q = p / (p - 1)

Alias of NNReal.holderConjugate_iff_eq_conjExponent.

@[deprecated NNReal.HolderConjugate.conjExponent (since := "2025-03-14")]

theorem NNReal.IsConjExponent.conjExponent {p : NNReal} (h : 1 < p) :

p.HolderConjugate p.conjExponent

Alias of NNReal.HolderConjugate.conjExponent.

@[deprecated NNReal.holderConjugate_one_div (since := "2025-03-14")]

theorem NNReal.isConjExponent_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

(1 / a).HolderConjugate (1 / b)

Alias of NNReal.holderConjugate_one_div.

@[deprecated Real.HolderTriple.toNNReal (since := "2025-03-14")]

theorem Real.IsConjExponent.toNNReal {p q r : ℝ} (h : p.HolderTriple q r) :

p.toNNReal.HolderTriple q.toNNReal r.toNNReal

Alias of Real.HolderTriple.toNNReal.

@[deprecated ENNReal.HolderConjugate (since := "2025-03-14")]

def ENNReal.IsConjExponent (p q : ENNReal) :

Alias of ENNReal.HolderConjugate.

An abbreviation for ENNReal.HolderTriple p q 1, this class states p⁻¹ + q⁻¹ = 1.

Equations

ENNReal.IsConjExponent = ENNReal.HolderConjugate

@[deprecated ENNReal.holderConjugate_iff (since := "2025-03-14")]

theorem ENNReal.isConjExponent_iff {p q : ENNReal} :

p.HolderConjugate q ↔ p⁻¹ + q⁻¹ = 1

Alias of ENNReal.holderConjugate_iff.

@[deprecated ENNReal.holderConjugate_coe_iff (since := "2025-03-14")]

theorem ENNReal.isConjExopnent_coe {p q : NNReal} :

(↑p).HolderConjugate ↑q ↔ p.HolderConjugate q

Alias of ENNReal.holderConjugate_coe_iff.

@[deprecated NNReal.HolderConjugate.coe_ennreal (since := "2025-03-14")]

theorem NNReal.IsConjExponent.coe_ennreal {p q : NNReal} :

p.HolderConjugate q → (↑p).HolderConjugate ↑q

Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

@[deprecated ENNReal.HolderConjugate.conjExponent (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.conjExponent {p : ENNReal} (hp : 1 ≤ p) :

p.HolderConjugate p.conjExponent

Alias of ENNReal.HolderConjugate.conjExponent.

@[deprecated ENNReal.HolderConjugate.symm (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.symm {p q : ENNReal} [hpq : p.HolderConjugate q] :

q.HolderConjugate p

Alias of ENNReal.HolderConjugate.symm.

@[deprecated ENNReal.HolderTriple.le (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.one_le (p q r : ENNReal) [p.HolderTriple q r] :

r ≤ p

Alias of ENNReal.HolderTriple.le.

@[deprecated ENNReal.HolderConjugate.pos (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.pos (p q : ENNReal) [p.HolderConjugate q] :

0 < p

Alias of ENNReal.HolderConjugate.pos.

@[deprecated ENNReal.HolderConjugate.ne_zero (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.ne_zero (p q : ENNReal) [p.HolderConjugate q] :

p ≠ 0

Alias of ENNReal.HolderConjugate.ne_zero.

@[deprecated ENNReal.HolderConjugate.one_sub_inv (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.one_sub_inv (p q : ENNReal) [p.HolderConjugate q] :

1 - p⁻¹ = q⁻¹

Alias of ENNReal.HolderConjugate.one_sub_inv.

@[deprecated ENNReal.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.conjExponent_eq {p q : ENNReal} [h : p.HolderConjugate q] :

p.conjExponent = q

Alias of ENNReal.HolderConjugate.conjExponent_eq.

@[deprecated ENNReal.HolderConjugate.conj_eq (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.conj_eq {p q : ENNReal} [h : p.HolderConjugate q] :

q = 1 + (p - 1)⁻¹

Alias of ENNReal.HolderConjugate.conj_eq.

@[deprecated ENNReal.HolderConjugate.mul_eq_add (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.mul_eq_add {p q : ENNReal} [h : p.HolderConjugate q] :

p * q = p + q

Alias of ENNReal.HolderConjugate.mul_eq_add.

@[deprecated ENNReal.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.div_conj_eq_sub_one {p q : ENNReal} [h : p.HolderConjugate q] :

p / q = p - 1

Alias of ENNReal.HolderConjugate.div_conj_eq_sub_one.

@[deprecated ENNReal.HolderConjugate.inv_inv (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.inv_inv {a b : ENNReal} (hab : a + b = 1) :

a⁻¹.HolderConjugate b⁻¹

Alias of ENNReal.HolderConjugate.inv_inv.

@[deprecated ENNReal.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.inv_one_sub_inv {a : ENNReal} (ha : a ≤ 1) :

a⁻¹.HolderConjugate (1 - a)⁻¹

Alias of ENNReal.HolderConjugate.inv_one_sub_inv.

@[deprecated ENNReal.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.one_sub_inv_inv {a : ENNReal} (ha : a ≤ 1) :

(1 - a)⁻¹.HolderConjugate a⁻¹

Alias of ENNReal.HolderConjugate.one_sub_inv_inv.

@[deprecated ENNReal.HolderConjugate.top_one (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.top_one :

⊤.HolderConjugate 1

Alias of ENNReal.HolderConjugate.top_one.

@[deprecated ENNReal.HolderConjugate.one_top (since := "2025-03-14")]

theorem ENNReal.IsConjExponent.one_top :

HolderConjugate 1 ⊤

Alias of ENNReal.HolderConjugate.one_top.