Commit 2025-02-25 15:30 2f02187c

View on Github →

feat: define klFun, auxiliary function used for the Kullback-Leibler divergence (#21901) From the TestingLowerBounds project.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added theorem Real.tendsto_log_nhdsWithin_zero_left

Modified Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

added theorem Real.leftDeriv_mul_log

added theorem Real.rightDeriv_mul_log

added theorem Real.tendsto_deriv_mul_log_atTop

added theorem Real.tendsto_rightDeriv_mul_log_atTop

Created Mathlib/InformationTheory/KullbackLeibler/KLFun.lean

added theorem InformationTheory.continuous_klFun

added theorem InformationTheory.convexOn_Ioi_klFun

added theorem InformationTheory.convexOn_klFun

added theorem InformationTheory.deriv_klFun

added theorem InformationTheory.hasDerivAt_klFun

added theorem InformationTheory.integrable_klFun_rnDeriv_iff

added theorem InformationTheory.integral_klFun_rnDeriv

added theorem InformationTheory.isMinOn_klFun

added theorem InformationTheory.klFun_apply

added theorem InformationTheory.klFun_eq_zero_iff

added theorem InformationTheory.klFun_nonneg

added theorem InformationTheory.klFun_one

added theorem InformationTheory.klFun_zero

added theorem InformationTheory.leftDeriv_klFun

added theorem InformationTheory.leftDeriv_klFun_one

added theorem InformationTheory.measurable_klFun

added theorem InformationTheory.not_differentiableAt_klFun_zero

added theorem InformationTheory.not_differentiableWithinAt_klFun_Iio_zero

added theorem InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero

added theorem InformationTheory.rightDeriv_klFun

added theorem InformationTheory.rightDeriv_klFun_one

added theorem InformationTheory.strictConvexOn_klFun

added theorem InformationTheory.stronglyMeasurable_klFun

added theorem InformationTheory.tendsto_klFun_atTop

added theorem InformationTheory.tendsto_rightDeriv_klFun_atTop

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

added theorem MeasureTheory.integrable_rnDeriv_mul_log_iff

added theorem MeasureTheory.integral_rnDeriv_mul_log

added theorem MeasureTheory.llr_self