Basic

📁 Source: Mathlib/InformationTheory/KullbackLeibler/Basic.lean

Statistics

Metric	Count
Definitions klDiv	1
Theorems integral_llr_add_mul_log_nonneg, integral_llr_add_sub_measure_univ_nonneg, klDiv_def, klDiv_eq_integral_klFun, klDiv_eq_lintegral_klFun, klDiv_eq_top_iff, klDiv_eq_zero_iff, klDiv_ne_top_iff, klDiv_of_ac_of_integrable, klDiv_of_not_ac, klDiv_of_not_integrable, klDiv_self, klDiv_zero_left, klDiv_zero_right, mul_klFun_le_toReal_klDiv, mul_log_le_klDiv, mul_log_le_toReal_klDiv, toReal_klDiv, toReal_klDiv_eq_integral_klFun, toReal_klDiv_of_measure_eq	20
Total	21

InformationTheory

Definitions

Name	Category	Theorems
klDiv 📖	CompOp	17 math math: mul_log_le_klDiv, toReal_klDiv_eq_integral_klFun, klDiv_eq_top_iff, klDiv_self, toReal_klDiv, klDiv_zero_right, klDiv_zero_left, klDiv_of_ac_of_integrable, klDiv_def, klDiv_eq_lintegral_klFun, klDiv_eq_zero_iff, mul_log_le_toReal_klDiv, klDiv_eq_integral_klFun, klDiv_of_not_integrable, toReal_klDiv_of_measure_eq, klDiv_of_not_ac, mul_klFun_le_toReal_klDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_llr_add_mul_log_nonneg 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	Real.instLE Real.instZero Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul MeasureTheory.Measure.real Set.univ Real.log Real.instOne	—	MeasureTheory.integral_zero_measure MulZeroClass.zero_mul add_zero zero_add sub_zero Real.instZeroLEOneClass MeasureTheory.Measure.absolutelyContinuous_zero_iff IsScalarTower.right MeasureTheory.Measure.AbsolutelyContinuous.trans MeasureTheory.Measure.absolutelyContinuous_smul integral_llr_add_sub_measure_univ_nonneg MeasureTheory.IsFiniteMeasure.average MeasureTheory.integrable_congr MeasureTheory.llr_smul_right MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Integrable.sub MeasureTheory.integrable_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.toReal_inv Real.log_inv mul_neg sub_neg_eq_add MeasureTheory.probReal_univ MeasureTheory.isProbabilityMeasureSMul smul_eq_mul MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.integral_sub MeasureTheory.integral_congr_ae
integral_llr_add_sub_measure_univ_nonneg 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	Real.instLE Real.instZero Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.real Set.univ	—	integral_klFun_rnDeriv MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal klFun_nonneg ENNReal.toReal_nonneg
klDiv_def 📖	mathematical	—	klDiv ENNReal MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr ENNReal.ofReal Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.real Set.univ Top.top instTopENNReal	—	—
klDiv_eq_integral_klFun 📖	mathematical	—	klDiv ENNReal MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal klFun ENNReal.toReal MeasureTheory.Measure.rnDeriv Top.top instTopENNReal	—	klDiv_def if_ctx_congr integral_klFun_rnDeriv
klDiv_eq_lintegral_klFun 📖	mathematical	—	klDiv ENNReal MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.lintegral ENNReal.ofReal klFun ENNReal.toReal MeasureTheory.Measure.rnDeriv Top.top instTopENNReal	—	klDiv_eq_integral_klFun MeasureTheory.lintegral_ofReal_ne_top_iff_integrable Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.fun_comp measurable_klFun Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass klFun_nonneg ENNReal.toReal_nonneg MeasureTheory.ofReal_integral_eq_lintegral_ofReal integrable_klFun_rnDeriv_iff not_iff_not
klDiv_eq_top_iff 📖	mathematical	—	klDiv Top.top ENNReal instTopENNReal MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	—	Mathlib.Tactic.Contrapose.contrapose₁ klDiv_of_ac_of_integrable or_not_of_imp klDiv_of_not_integrable klDiv_of_not_ac
klDiv_eq_zero_iff 📖	mathematical	—	klDiv ENNReal instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_eq_one_iff_eq MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite klDiv_ne_top_iff Filter.mp_mem MeasureTheory.lintegral_eq_zero_iff Measurable.ennreal_ofReal Measurable.fun_comp measurable_klFun Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv klDiv_eq_lintegral_klFun Filter.univ_mem' le_antisymm klFun_nonneg ENNReal.toReal_nonneg ENNReal.toReal_eq_one_iff klFun_eq_zero_iff klDiv_self
klDiv_ne_top_iff 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	—	—
klDiv_of_ac_of_integrable 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	klDiv ENNReal.ofReal Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.real Set.univ	—	klDiv_def
klDiv_of_not_ac 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	klDiv Top.top ENNReal instTopENNReal	—	klDiv_def
klDiv_of_not_integrable 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	klDiv Top.top ENNReal instTopENNReal	—	klDiv_def
klDiv_self 📖	mathematical	—	klDiv ENNReal instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.llr_self klDiv_def MeasureTheory.integrable_congr MeasureTheory.Measure.AbsolutelyContinuous.rfl MeasureTheory.integrable_zero MeasureTheory.integral_congr_ae MeasureTheory.integral_zero zero_add sub_self ENNReal.ofReal_zero
klDiv_zero_left 📖	mathematical	—	klDiv MeasureTheory.Measure MeasureTheory.Measure.instZero DFunLike.coe Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	MeasureTheory.integral_zero_measure zero_add sub_zero MeasureTheory.ofReal_measureReal klDiv_of_ac_of_integrable MeasureTheory.Measure.AbsolutelyContinuous.zero MeasureTheory.integrable_zero_measure
klDiv_zero_right 📖	mathematical	—	klDiv MeasureTheory.Measure MeasureTheory.Measure.instZero Top.top ENNReal instTopENNReal	—	klDiv_of_not_ac Function.mt MeasureTheory.Measure.absolutelyContinuous_zero_iff
mul_klFun_le_toReal_klDiv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	Real.instLE Real.instMul MeasureTheory.Measure.real Set.univ klFun DivInvMonoid.toDiv Real.instDivInvMonoid ENNReal.toReal klDiv	—	MeasureTheory.mul_le_integral_rnDeriv_of_ac convexOn_klFun Continuous.continuousWithinAt continuous_klFun integrable_klFun_rnDeriv_iff toReal_klDiv_eq_integral_klFun
mul_log_le_klDiv 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofReal Real Real.instSub Real.instAdd Real.instMul MeasureTheory.Measure.real Set.univ Real.log DivInvMonoid.toDiv Real.instDivInvMonoid klDiv	—	ENNReal.ofReal_toReal klDiv_ne_top_iff ENNReal.ofReal_le_ofReal mul_log_le_toReal_klDiv klDiv_of_not_integrable klDiv_of_not_ac
mul_log_le_toReal_klDiv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	Real.instLE Real.instSub Real.instAdd Real.instMul MeasureTheory.Measure.real Set.univ Real.log DivInvMonoid.toDiv Real.instDivInvMonoid ENNReal.toReal klDiv	—	zero_div Real.log_zero MulZeroClass.mul_zero zero_add sub_zero klDiv_zero_left MeasureTheory.Measure.absolutelyContinuous_zero_iff LE.le.trans le_of_eq mul_div_cancel₀ klFun.eq_1 mul_sub mul_add Distrib.leftDistribClass mul_one mul_assoc mul_klFun_le_toReal_klDiv
toReal_klDiv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	ENNReal.toReal klDiv Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.real Set.univ	—	klDiv_of_ac_of_integrable ENNReal.toReal_ofReal integral_llr_add_sub_measure_univ_nonneg
toReal_klDiv_eq_integral_klFun 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	ENNReal.toReal klDiv MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal klFun MeasureTheory.Measure.rnDeriv	—	klDiv_eq_integral_klFun ENNReal.toReal_ofReal MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal klFun_nonneg ENNReal.toReal_nonneg MeasureTheory.integral_undef integrable_klFun_rnDeriv_iff klDiv_of_not_integrable ENNReal.toReal_top
toReal_klDiv_of_measure_eq 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	ENNReal.toReal klDiv MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.llr	—	toReal_klDiv add_sub_cancel_right klDiv_of_not_integrable MeasureTheory.integral_undef ENNReal.toReal_top

---

← Back to Index