Commit 2025-04-10 06:34 89ce5442

View on Github →

feat: p / r and q / r are Hölder conjugate if p, q, r is a Hölder triple (#23882) Also rename the inv_add_inv' field to inv_add_inv_eq_inv since we can let it have the correct explicit arguments since v4.19.0-rc1 From LeanAPAP

Estimated changes

Modified Mathlib/Data/ENNReal/Holder.lean

added theorem ENNReal.HolderTriple.holderConjugate_div_div

deleted theorem ENNReal.HolderTriple.inv_add_inv_eq_inv

modified theorem ENNReal.HolderTriple.inv_eq

modified theorem ENNReal.HolderTriple.one_div_add_one_div

Modified Mathlib/Data/Real/ConjExponents.lean

added theorem NNReal.HolderTriple.holderConjugate_div_div

deleted theorem NNReal.HolderTriple.inv_add_inv_eq_inv

added theorem Real.HolderTriple.holderConjugate_div_div

deleted theorem Real.HolderTriple.inv_add_inv_eq_inv