Commit 2024-02-17 09:43 d02cf66e

View on Github →

feat: Conjugate exponents in ℝ≥0 (#10589) It happens often that we have p q : ℝ≥0 that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with ℝ≥0 conjugates clumsy. This PR

introduces NNReal.IsConjExponent, NNReal.conjExponent
renames Real.IsConjugateExponent, Real.conjugateExponent to Real.IsConjExponent, Real.conjExponent
renames a few more lemmas to match up the Real and NNReal versions From LeanAPAP

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/MeanInequalities.lean

modified theorem ENNReal.inner_le_Lp_mul_Lq

modified theorem ENNReal.young_inequality

modified theorem NNReal.inner_le_Lp_mul_Lq

modified theorem NNReal.inner_le_Lp_mul_Lq_tsum'

modified theorem NNReal.inner_le_Lp_mul_Lq_tsum

modified theorem NNReal.isGreatest_Lp

modified theorem NNReal.summable_mul_of_Lp_Lq

modified theorem NNReal.young_inequality

modified theorem NNReal.young_inequality_real

modified theorem Real.inner_le_Lp_mul_Lq

modified theorem Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg

modified theorem Real.inner_le_Lp_mul_Lq_of_nonneg

modified theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg'

modified theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg

modified theorem Real.summable_mul_of_Lp_Lq_of_nonneg

modified theorem Real.young_inequality

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Created Mathlib/Data/Real/ConjExponents.lean

added theorem NNReal.IsConjExponent.conjExponent_eq

added theorem NNReal.IsConjExponent.conj_eq

added theorem NNReal.IsConjExponent.div_conj_eq_sub_one

added theorem NNReal.IsConjExponent.inv_add_inv_conj_ennreal

added theorem NNReal.IsConjExponent.inv_ne_zero

added theorem NNReal.IsConjExponent.inv_one_sub_inv

added theorem NNReal.IsConjExponent.inv_pos

added theorem NNReal.IsConjExponent.mul_eq_add

added theorem NNReal.IsConjExponent.ne_zero

added theorem NNReal.IsConjExponent.one_le

added theorem NNReal.IsConjExponent.one_sub_inv

added theorem NNReal.IsConjExponent.one_sub_inv_inv

added theorem NNReal.IsConjExponent.pos

added theorem NNReal.IsConjExponent.sub_one_mul_conj

added theorem NNReal.IsConjExponent.sub_one_ne_zero

added theorem NNReal.IsConjExponent.sub_one_pos

added structure NNReal.IsConjExponent

added theorem NNReal.isConjExponent_coe

added theorem NNReal.isConjExponent_iff_eq_conjExponent

added theorem Real.IsConjExponent.conjExponent

added theorem Real.IsConjExponent.conjExponent_eq

added theorem Real.IsConjExponent.conj_eq

added theorem Real.IsConjExponent.div_conj_eq_sub_one

added theorem Real.IsConjExponent.inv_add_inv_conj_ennreal

added theorem Real.IsConjExponent.inv_one_sub_inv

added theorem Real.IsConjExponent.inv_sub_one

added theorem Real.IsConjExponent.mul_eq_add

added theorem Real.IsConjExponent.ne_zero

added theorem Real.IsConjExponent.nonneg

added theorem Real.IsConjExponent.one_div_ne_zero

added theorem Real.IsConjExponent.one_div_nonneg

added theorem Real.IsConjExponent.one_div_pos

added theorem Real.IsConjExponent.one_sub_inv

added theorem Real.IsConjExponent.one_sub_inv_inv

added theorem Real.IsConjExponent.pos

added theorem Real.IsConjExponent.sub_one_mul_conj

added theorem Real.IsConjExponent.sub_one_ne_zero

added theorem Real.IsConjExponent.sub_one_pos

added structure Real.IsConjExponent

added def Real.conjExponent

added theorem Real.isConjExponent_iff_eq_conjExponent

added theorem Real.isConjExponent_one_div

Deleted Mathlib/Data/Real/ConjugateExponents.lean

deleted theorem Real.IsConjugateExponent.conj_eq

deleted theorem Real.IsConjugateExponent.conjugate_eq

deleted theorem Real.IsConjugateExponent.div_conj_eq_sub_one

deleted theorem Real.IsConjugateExponent.inv_add_inv_conj_ennreal

deleted theorem Real.IsConjugateExponent.inv_add_inv_conj_nnreal

deleted theorem Real.IsConjugateExponent.mul_eq_add

deleted theorem Real.IsConjugateExponent.ne_zero

deleted theorem Real.IsConjugateExponent.nonneg

deleted theorem Real.IsConjugateExponent.one_div_ne_zero

deleted theorem Real.IsConjugateExponent.one_div_nonneg

deleted theorem Real.IsConjugateExponent.one_div_pos

deleted theorem Real.IsConjugateExponent.one_lt_nnreal

deleted theorem Real.IsConjugateExponent.pos

deleted theorem Real.IsConjugateExponent.sub_one_mul_conj

deleted theorem Real.IsConjugateExponent.sub_one_ne_zero

deleted theorem Real.IsConjugateExponent.sub_one_pos

deleted structure Real.IsConjugateExponent

deleted def Real.conjugateExponent

deleted theorem Real.isConjugateExponent_conjugateExponent

deleted theorem Real.isConjugateExponent_iff

deleted theorem Real.isConjugateExponent_inv

deleted theorem Real.isConjugateExponent_one_div

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

modified theorem MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

modified theorem ENNReal.lintegral_mul_le_Lp_mul_Lq

modified theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top

modified theorem ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one

modified theorem NNReal.lintegral_mul_le_Lp_mul_Lq

Modified Mathlib/NumberTheory/Rayleigh.lean

modified theorem beattySeq'_symmDiff_beattySeq_pos

modified theorem beattySeq_symmDiff_beattySeq'_pos

modified theorem compl_beattySeq'

modified theorem compl_beattySeq