Commit 2024-10-03 13:49 1a9758b2

View on Github →

feat: ENNReal-valued conjugate exponents (#17353) Define ENNReal.IsConjExponent, the ENNReal analogue of Real.IsConjExponent and NNReal.IsConjExponent. This will allow stating Hölder's inequality for the L1 and Linfty norms too. From LeanAPAP

Estimated changes

Modified Mathlib/Data/ENNReal/Operations.lean

modified theorem ENNReal.coe_sub

added theorem ENNReal.top_sub

Modified Mathlib/Data/Real/ConjExponents.lean

added theorem ENNReal.IsConjExponent.conjExponent_eq

added theorem ENNReal.IsConjExponent.conj_eq

added theorem ENNReal.IsConjExponent.div_conj_eq_sub_one

added theorem ENNReal.IsConjExponent.inv_one_sub_inv

added theorem ENNReal.IsConjExponent.mul_eq_add

added theorem ENNReal.IsConjExponent.ne_zero

added theorem ENNReal.IsConjExponent.one_le

added theorem ENNReal.IsConjExponent.one_sub_inv

added theorem ENNReal.IsConjExponent.one_sub_inv_inv

added theorem ENNReal.IsConjExponent.one_top

added theorem ENNReal.IsConjExponent.pos

added theorem ENNReal.IsConjExponent.top_one

added structure ENNReal.IsConjExponent

added theorem ENNReal.coe_conjExponent

added theorem ENNReal.isConjExponent_coe

added theorem ENNReal.isConjExponent_comm

added theorem ENNReal.isConjExponent_iff_eq_conjExponent

added theorem NNReal.isConjExponent_comm

added theorem Real.isConjExponent_comm