Commit 2026-03-03 19:57 1b8c8e75

View on Github →

feat: klDiv and scalar multiplication (#35301) The Kullback-Leibler divergence in Mathlib is defined for finite measures, not just probability measures. This PR adds lemmas that show how klDiv changes when we multiply one or both of the measures by a scalar.

Estimated changes

Modified Mathlib/InformationTheory/KullbackLeibler/Basic.lean

added theorem InformationTheory.klDiv_ne_top

added theorem InformationTheory.klDiv_smul_right_eq_smul_left

added theorem InformationTheory.klDiv_smul_same

added theorem InformationTheory.toReal_klDiv_smul_left

added theorem InformationTheory.toReal_klDiv_smul_right

added theorem InformationTheory.toReal_klDiv_smul_right_eq_smul_left

added theorem InformationTheory.toReal_klDiv_smul_same

Modified Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

added theorem MeasureTheory.Measure.AbsolutelyContinuous.smul_right

Modified Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

added theorem MeasureTheory.Measure.rnDeriv_smul_same

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

added theorem MeasureTheory.llr_smul_inv_left_eq_smul_right

added theorem MeasureTheory.llr_smul_nnreal_left

added theorem MeasureTheory.llr_smul_nnreal_right

added theorem MeasureTheory.llr_smul_nnreal_same

added theorem MeasureTheory.llr_smul_same

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.coe_nnreal_smul