ChainRule

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

Statistics

Metric	Count
Definitions	0
Theorems integrable_llr_compProd_iff, integrable_llr_of_integrable_llr_compProd, integral_llr_compProd_eq_add, klDiv_compProd_eq_add, klDiv_compProd_left, rnDeriv_compProd_mul_log_eq_mul_add	6
Total	6

InformationTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_llr_compProd_iff 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Prod.instMeasurableSpace MeasureTheory.Measure.compProd	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.instMeasurableSpace MeasureTheory.llr MeasureTheory.Measure.compProd	—	MeasureTheory.Measure.absolutelyContinuous_compProd_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.neZero ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.integrable_rnDeriv_mul_log_iff MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.Measure.instSFiniteProdCompProd MeasureTheory.integrable_congr rnDeriv_compProd_mul_log_eq_mul_add MeasureTheory.integrable_toReal_rnDeriv_mul_iff MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.integrable_compProd_iff MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.comp_measurable MeasureTheory.stronglyMeasurable_llr Measurable.fst measurable_id' ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_mul MeasureTheory.integrable_norm_iff integrable_llr_of_integrable_llr_compProd MeasureTheory.integrable_add_iff_integrable_right' MeasureTheory.Integrable.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal
integrable_llr_of_integrable_llr_compProd 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Prod.instMeasurableSpace MeasureTheory.Measure.compProd 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	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	—	MeasureTheory.Measure.absolutelyContinuous_compProd_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.neZero ProbabilityTheory.IsMarkovKernel.is_probability_measure' ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd Continuous.stronglyMeasurable BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Real.continuous_mul_log Real.convexOn_mul_log Continuous.continuousWithinAt MeasureTheory.integrable_rnDeriv_mul_log_iff MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.Measure.instSFiniteProdCompProd MeasureTheory.instSFiniteOfSigmaFinite
integral_llr_compProd_eq_add 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Prod.instMeasurableSpace MeasureTheory.Measure.compProd 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	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Prod.instMeasurableSpace MeasureTheory.Measure.compProd MeasureTheory.llr Real.instAdd	—	MeasureTheory.Measure.absolutelyContinuous_compProd_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.neZero ProbabilityTheory.IsMarkovKernel.is_probability_measure' integrable_llr_compProd_iff MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.integrable_compProd_iff MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.comp_measurable Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.log measurable_id' Measurable.ennreal_toReal Measurable.fun_comp MeasureTheory.Measure.measurable_rnDeriv Measurable.fst ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_mul MeasureTheory.integrable_norm_iff MeasureTheory.stronglyMeasurable_llr MeasureTheory.integral_rnDeriv_mul_log MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.Measure.instSFiniteProdCompProd MeasureTheory.integral_congr_ae rnDeriv_compProd_mul_log_eq_mul_add MeasureTheory.integral_rnDeriv_smul MeasureTheory.integral_add MeasureTheory.Integrable.ofReal MeasureTheory.Measure.integral_compProd
klDiv_compProd_eq_add 📖	mathematical	—	klDiv Prod.instMeasurableSpace MeasureTheory.Measure.compProd ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	MeasureTheory.Measure.absolutelyContinuous_compProd_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.neZero ProbabilityTheory.IsMarkovKernel.is_probability_measure' integrable_llr_compProd_iff klDiv_of_ac_of_integrable ENNReal.ofReal_add integral_llr_add_sub_measure_univ_nonneg MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.compProd_apply_univ MeasureTheory.instSFiniteOfSigmaFinite add_sub_cancel_right integral_llr_compProd_eq_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.add_pf_add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg add_zero klDiv_of_not_integrable top_add add_top klDiv_of_not_ac
klDiv_compProd_left 📖	mathematical	—	klDiv Prod.instMeasurableSpace MeasureTheory.Measure.compProd	—	klDiv_eq_lintegral_klFun_of_ac MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.IsProbabilityMeasure.neZero ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.rnDeriv_measure_compProd_left Filter.univ_mem' MeasureTheory.Measure.lintegral_compProd Measurable.ennreal_ofReal Measurable.fun_comp measurable_klFun Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv Measurable.fst measurable_id' MeasureTheory.lintegral_const MeasureTheory.IsProbabilityMeasure.measure_univ mul_one klDiv_of_not_ac
rnDeriv_compProd_mul_log_eq_mul_add 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Prod.instMeasurableSpace MeasureTheory.Measure.compProd	Filter.Eventually Real Real.instMul ENNReal.toReal MeasureTheory.Measure.rnDeriv Prod.instMeasurableSpace MeasureTheory.Measure.compProd Real.log Real.instAdd MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.rnDeriv_compProd ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel Filter.univ_mem' ENNReal.toReal_mul MulZeroClass.zero_mul Real.log_zero MulZeroClass.mul_zero zero_add add_zero Real.log_mul

---

← Back to Index