mathlib3 documentation

data.real.conjugate_exponents

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.

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.

noncomputable def real.conjugate_exponent (p : ) :

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

Equations
theorem real.is_conjugate_exponent.conj_eq {p q : } (h : p.is_conjugate_exponent q) :
q = p / (p - 1)
@[protected, symm]
theorem real.is_conjugate_exponent_iff {p q : } (h : 1 < p) :
p.is_conjugate_exponent q q = p / (p - 1)
theorem real.is_conjugate_exponent_one_div {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :