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_lintegral_klFun_of_ac, klDiv_eq_top_iff, klDiv_eq_zero_iff, klDiv_ne_top, klDiv_ne_top_iff, klDiv_of_ac_of_integrable, klDiv_of_not_ac, klDiv_of_not_integrable, klDiv_self, klDiv_smul_right_eq_smul_left, klDiv_smul_same, 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, toReal_klDiv_smul_left, toReal_klDiv_smul_right, toReal_klDiv_smul_right_eq_smul_left, toReal_klDiv_smul_same	28
Total	29

InformationTheory

Definitions

Name	Category	Theorems
klDiv 📖	CompOp	26 math math: mul_log_le_klDiv, klDiv_smul_right_eq_smul_left, toReal_klDiv_eq_integral_klFun, klDiv_eq_top_iff, klDiv_self, toReal_klDiv, klDiv_zero_right, klDiv_zero_left, klDiv_eq_lintegral_klFun_of_ac, klDiv_of_ac_of_integrable, klDiv_def, klDiv_eq_lintegral_klFun, klDiv_eq_zero_iff, klDiv_compProd_eq_add, mul_log_le_toReal_klDiv, klDiv_eq_integral_klFun, klDiv_of_not_integrable, toReal_klDiv_of_measure_eq, toReal_klDiv_smul_right_eq_smul_left, toReal_klDiv_smul_right, toReal_klDiv_smul_same, klDiv_of_not_ac, klDiv_smul_same, toReal_klDiv_smul_left, mul_klFun_le_toReal_klDiv, klDiv_compProd_left

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 Real.instLE Real.instZero Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.llr 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 Real.instLE Real.instZero Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.llr 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_lintegral_klFun_of_ac 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	klDiv MeasureTheory.lintegral ENNReal.ofReal klFun ENNReal.toReal MeasureTheory.Measure.rnDeriv	—	klDiv_eq_lintegral_klFun
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 📖	—	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_ne_top_iff
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 Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.llr 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_smul_right_eq_smul_left 📖	mathematical	—	klDiv NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.ofNNReal NNReal.instInv	—	IsScalarTower.right smul_smul mul_inv_cancel₀ one_smul inv_mul_cancel₀ MeasureTheory.Measure.AbsolutelyContinuous.smul_right MeasureTheory.Integrable.smul_measure_nnreal MeasureTheory.integrable_congr MeasureTheory.llr_smul_nnreal_left MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Integrable.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.integrable_const MeasureTheory.llr_smul_nnreal_right MeasureTheory.Integrable.sub' ENNReal.ofReal_toReal klDiv_ne_top toReal_klDiv_smul_right_eq_smul_left ENNReal.ofReal_mul ENNReal.ofReal_coe_nnreal MeasureTheory.Measure.AbsolutelyContinuous.smul_left klDiv_of_not_integrable MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.instOuterMeasureClass Real.log_inv sub_neg_eq_add MeasureTheory.Measure.haveLebesgueDecompositionSMul ENNReal.mul_top klDiv_of_not_ac
klDiv_smul_same 📖	mathematical	—	klDiv NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.ofNNReal	—	IsScalarTower.right zero_smul klDiv_self MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasureZero MulZeroClass.zero_mul smul_smul inv_mul_cancel₀ one_smul ENNReal.ofReal_toReal klDiv_ne_top MeasureTheory.Measure.AbsolutelyContinuous.smul MeasureTheory.Integrable.smul_measure_nnreal MeasureTheory.integrable_congr MeasureTheory.llr_smul_nnreal_same MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite toReal_klDiv_smul_same ENNReal.ofReal_mul ENNReal.ofReal_coe_nnreal klDiv_of_not_integrable MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.haveLebesgueDecompositionSMul MeasureTheory.Measure.haveLebesgueDecompositionSMulRight ENNReal.mul_top klDiv_of_not_ac
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 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 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 instReflLe 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 Real.instSub Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.llr 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
toReal_klDiv_smul_left 📖	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 NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.instAdd Real.instMul NNReal.toReal Real.instSub Real.instOne MeasureTheory.Measure.real Set.univ Real.log	—	IsScalarTower.right zero_smul klDiv_zero_left MulZeroClass.zero_mul sub_zero one_mul zero_add Real.log_zero MulZeroClass.mul_zero add_zero MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.llr_smul_nnreal_left MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite toReal_klDiv MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.AbsolutelyContinuous.smul_left MeasureTheory.Integrable.smul_measure_nnreal MeasureTheory.integrable_congr MeasureTheory.Integrable.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.integrable_const MeasureTheory.integral_smul_nnreal_measure MeasureTheory.measureReal_nnreal_smul_apply MeasureTheory.integral_congr_ae MeasureTheory.integral_add MeasureTheory.integral_const Real.instCompleteSpace Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
toReal_klDiv_smul_right 📖	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 NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.instSub Real.instAdd Real.instMul NNReal.toReal Real.instOne MeasureTheory.Measure.real Set.univ Real.log	—	IsScalarTower.right toReal_klDiv_smul_right_eq_smul_left toReal_klDiv_smul_left Real.log_inv mul_neg neg_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
toReal_klDiv_smul_right_eq_smul_left 📖	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 NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.instMul NNReal.toReal NNReal.instInv	—	IsScalarTower.right zero_smul inv_zero klDiv_zero_left MulZeroClass.zero_mul eq_zero_or_neZero klDiv_self MeasureTheory.IsFiniteMeasure.toSigmaFinite klDiv_zero_right MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.llr_smul_nnreal_left MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.llr_smul_nnreal_right toReal_klDiv MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.AbsolutelyContinuous.smul_right MeasureTheory.integrable_congr MeasureTheory.Integrable.sub' MeasureTheory.integrable_const MeasureTheory.Measure.AbsolutelyContinuous.smul_left MeasureTheory.Integrable.smul_measure_nnreal MeasureTheory.Integrable.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.measureReal_nnreal_smul_apply MeasureTheory.integral_smul_nnreal_measure MeasureTheory.llr_smul_inv_left_eq_smul_right MeasureTheory.integral_congr_ae ENNReal.coe_inv mul_sub mul_add Distrib.leftDistribClass mul_inv_cancel_left₀
toReal_klDiv_smul_same 📖	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 NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.instMul NNReal.toReal	—	IsScalarTower.right zero_smul klDiv_self MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasureZero MulZeroClass.zero_mul toReal_klDiv_smul_right_eq_smul_left MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.Measure.AbsolutelyContinuous.smul_left MeasureTheory.Integrable.smul_measure_nnreal MeasureTheory.integrable_congr MeasureTheory.llr_smul_nnreal_left MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Integrable.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.integrable_const smul_smul inv_mul_cancel₀ one_smul

---

← Back to Index