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
> 1 and
1/p + 1/q = 1. This property shows up often in analysis, especially when dealing with
We make several basic facts available through dot notation in this situation.
We also introduce
p / (p-1). When
p > 1, it is conjugate to
- 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
The conjugate exponent of
q = p/(p-1), so that
1/p + 1/q = 1.