Real conjugate exponents #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

structure real.is_conjugate_exponent (p q : ℝ) :

Prop

one_lt : 1 < p
inv_add_inv_conj : 1 / p + 1 / q = 1

Two real exponents p, q are conjugate if they are > 1 and satisfy the equality 1/p + 1/q = 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

source

noncomputable def real.conjugate_exponent (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)

source

theorem real.is_conjugate_exponent.pos {p q : ℝ} (h : p.is_conjugate_exponent q) :

0 < p

source

theorem real.is_conjugate_exponent.nonneg {p q : ℝ} (h : p.is_conjugate_exponent q) :

0 ≤ p

source

theorem real.is_conjugate_exponent.ne_zero {p q : ℝ} (h : p.is_conjugate_exponent q) :

p ≠ 0

source

theorem real.is_conjugate_exponent.sub_one_pos {p q : ℝ} (h : p.is_conjugate_exponent q) :

0 < p - 1

source

theorem real.is_conjugate_exponent.sub_one_ne_zero {p q : ℝ} (h : p.is_conjugate_exponent q) :

p - 1 ≠ 0

source

theorem real.is_conjugate_exponent.one_div_pos {p q : ℝ} (h : p.is_conjugate_exponent q) :

0 < 1 / p

source

theorem real.is_conjugate_exponent.one_div_nonneg {p q : ℝ} (h : p.is_conjugate_exponent q) :

0 ≤ 1 / p

source

theorem real.is_conjugate_exponent.one_div_ne_zero {p q : ℝ} (h : p.is_conjugate_exponent q) :

1 / p ≠ 0

source

theorem real.is_conjugate_exponent.conj_eq {p q : ℝ} (h : p.is_conjugate_exponent q) :

q = p / (p - 1)

source

theorem real.is_conjugate_exponent.conjugate_eq {p q : ℝ} (h : p.is_conjugate_exponent q) :

p.conjugate_exponent = q

source

theorem real.is_conjugate_exponent.sub_one_mul_conj {p q : ℝ} (h : p.is_conjugate_exponent q) :

(p - 1) * q = p

source

theorem real.is_conjugate_exponent.mul_eq_add {p q : ℝ} (h : p.is_conjugate_exponent q) :

p * q = p + q

source

@[protected, symm]

theorem real.is_conjugate_exponent.symm {p q : ℝ} (h : p.is_conjugate_exponent q) :

q.is_conjugate_exponent p

source

theorem real.is_conjugate_exponent.div_conj_eq_sub_one {p q : ℝ} (h : p.is_conjugate_exponent q) :

p / q = p - 1

source

theorem real.is_conjugate_exponent.one_lt_nnreal {p q : ℝ} (h : p.is_conjugate_exponent q) :

1 < p.to_nnreal

source

theorem real.is_conjugate_exponent.inv_add_inv_conj_nnreal {p q : ℝ} (h : p.is_conjugate_exponent q) :

1 / p.to_nnreal + 1 / q.to_nnreal = 1

source

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

source

theorem real.is_conjugate_exponent_iff {p q : ℝ} (h : 1 < p) :

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

source

theorem real.is_conjugate_exponent_conjugate_exponent {p : ℝ} (h : 1 < p) :

p.is_conjugate_exponent p.conjugate_exponent

source

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

(1 / a).is_conjugate_exponent (1 / b)