LogLikelihoodRatio

📁 Source: Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

Statistics

Metric	Count
Definitions llr	1
Theorems exp_llr, exp_llr_of_ac, exp_llr_of_ac', exp_neg_llr, exp_neg_llr', integrable_llr_tilted_left, integrable_llr_tilted_right, integrable_rnDeriv_mul_log_iff, integral_llr_tilted_left, integral_llr_tilted_right, integral_rnDeriv_mul_log, llr_def, llr_self, llr_smul_left, llr_smul_right, llr_tilted_left, llr_tilted_right, measurable_llr, neg_llr, stronglyMeasurable_llr	20
Total	21

MeasureTheory

Definitions

Name	Category	Theorems
llr 📖	CompOp	22 math math: InformationTheory.integrable_klFun_rnDeriv_iff, llr_self, exp_llr_of_ac', InformationTheory.klDiv_eq_top_iff, llr_tilted_right, InformationTheory.klDiv_def, InformationTheory.klDiv_ne_top_iff, InformationTheory.klDiv_eq_integral_klFun, stronglyMeasurable_llr, integral_rnDeriv_mul_log, InformationTheory.toReal_klDiv_of_measure_eq, exp_neg_llr, exp_neg_llr', measurable_llr, llr_tilted_left, exp_llr_of_ac, llr_smul_right, llr_def, exp_llr, llr_smul_left, integrable_rnDeriv_mul_log_iff, neg_llr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_llr 📖	mathematical	—	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.exp llr ENNReal Measure.rnDeriv instZeroENNReal LinearOrder.toDecidableEq ENNReal.instLinearOrder Real.instOne ENNReal.toReal	—	Filter.mp_mem Measure.instOuterMeasureClass Measure.rnDeriv_lt_top Filter.univ_mem' Real.log_zero Real.exp_zero llr.eq_1 Real.exp_log ENNReal.toReal_pos LT.lt.ne
exp_llr_of_ac 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.exp llr ENNReal.toReal Measure.rnDeriv	—	Filter.mp_mem Measure.instOuterMeasureClass Measure.rnDeriv_pos Measure.AbsolutelyContinuous.ae_le exp_llr Filter.univ_mem' LT.lt.ne'
exp_llr_of_ac' 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.exp llr ENNReal.toReal Measure.rnDeriv	—	Filter.mp_mem Measure.instOuterMeasureClass Measure.rnDeriv_pos' Measure.haveLebesgueDecomposition_of_sigmaFinite instSFiniteOfSigmaFinite exp_llr Filter.univ_mem' LT.lt.ne'
exp_neg_llr 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.exp Real.instNeg llr ENNReal.toReal Measure.rnDeriv	—	Filter.mp_mem Measure.instOuterMeasureClass exp_llr_of_ac' neg_llr Filter.univ_mem' Pi.neg_apply
exp_neg_llr' 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.exp Real.instNeg llr ENNReal.toReal Measure.rnDeriv	—	Filter.mp_mem Measure.instOuterMeasureClass exp_llr_of_ac Measure.haveLebesgueDecomposition_of_sigmaFinite instSFiniteOfSigmaFinite neg_llr Filter.univ_mem' neg_eq_iff_eq_neg Pi.neg_apply
integrable_llr_tilted_left 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing llr Real.exp AEMeasurable Real.measurableSpace	Measure.tilted	—	integrable_congr llr_tilted_left IsFiniteMeasure.toSigmaFinite Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Integrable.sub integrable_const
integrable_llr_tilted_right 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing llr Real.exp	Measure.tilted	—	integrable_congr llr_tilted_right IsFiniteMeasure.toSigmaFinite Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Integrable.neg integrable_const
integrable_rnDeriv_mul_log_iff 📖	mathematical	Measure.AbsolutelyContinuous	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul ENNReal.toReal Measure.rnDeriv Real.log llr	—	integrable_rnDeriv_smul_iff
integral_llr_tilted_left 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing llr Real.exp AEMeasurable Real.measurableSpace	integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.tilted Real.instSub Real.instAdd Real.log	—	integral_congr_ae llr_tilted_left IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure integral_add Integrable.sub integrable_const integral_sub integral_const Real.instCompleteSpace probReal_univ one_mul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
integral_llr_tilted_right 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp llr	integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.tilted Real.instAdd Real.instSub Real.log	—	integral_congr_ae llr_tilted_right IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure integral_neg integral_add Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Integrable.neg integrable_const integral_const Real.instCompleteSpace probReal_univ one_mul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.const_add_termg add_zero
integral_rnDeriv_mul_log 📖	mathematical	Measure.AbsolutelyContinuous	integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instMul ENNReal.toReal Measure.rnDeriv Real.log llr	—	integral_rnDeriv_smul
llr_def 📖	mathematical	—	llr Real.log ENNReal.toReal Measure.rnDeriv	—	—
llr_self 📖	mathematical	—	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr Pi.instZero Real.instZero	—	Filter.mp_mem Measure.instOuterMeasureClass Measure.rnDeriv_self Filter.univ_mem' Real.log_one
llr_smul_left 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr ENNReal Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Real.instAdd Real.log ENNReal.toReal	—	Measure.instOuterMeasureClass IsScalarTower.right Measure.rnDeriv_smul_left_of_ne_top Filter.mp_mem Measure.AbsolutelyContinuous.ae_le Measure.rnDeriv_lt_top IsFiniteMeasure.toSigmaFinite Measure.rnDeriv_pos Filter.univ_mem' ENNReal.toReal_mul Real.log_mul ENNReal.toReal_ne_zero LT.lt.ne' LT.lt.ne Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
llr_smul_right 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr ENNReal Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Real.instSub Real.log ENNReal.toReal	—	Measure.instOuterMeasureClass IsScalarTower.right Measure.rnDeriv_smul_right_of_ne_top Filter.mp_mem Measure.AbsolutelyContinuous.ae_le Measure.rnDeriv_lt_top IsFiniteMeasure.toSigmaFinite Measure.rnDeriv_pos Filter.univ_mem' ENNReal.toReal_mul Real.log_mul ENNReal.toReal_ne_zero LT.lt.ne' LT.lt.ne ENNReal.toReal_inv Real.log_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
llr_tilted_left 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp AEMeasurable Real.measurableSpace	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr Measure.tilted Real.instAdd Real.instSub Real.log integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	eq_zero_or_neZero Measure.instOuterMeasureClass ae.congr_simp ae_zero Filter.mp_mem Measure.AbsolutelyContinuous.ae_le Measure.rnDeriv_lt_top Measure.rnDeriv_pos Measure.haveLebesgueDecomposition_of_sigmaFinite instSFiniteOfSigmaFinite toReal_rnDeriv_tilted_left Filter.univ_mem' llr.eq_1 Real.log_mul LT.lt.ne' Real.exp_pos integral_exp_pos LT.lt.ne div_eq_mul_inv Real.log_exp Real.log_inv sub_eq_add_neg
llr_tilted_right 📖	mathematical	Measure.AbsolutelyContinuous Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr Measure.tilted Real.instAdd Real.instNeg Real.log integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	eq_zero_or_neZero Measure.instOuterMeasureClass Measure.ext ae.congr_simp ae_zero Filter.mp_mem Measure.AbsolutelyContinuous.ae_le Measure.rnDeriv_lt_top Measure.rnDeriv_pos Measure.haveLebesgueDecomposition_of_sigmaFinite instSFiniteOfSigmaFinite toReal_rnDeriv_tilted_right Filter.univ_mem' llr.eq_1 Real.log_mul LT.lt.ne' mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_exp_pos LT.lt.ne Real.log_exp
measurable_llr 📖	mathematical	—	Measurable Real Real.measurableSpace llr	—	Measurable.log Measurable.ennreal_toReal Measure.measurable_rnDeriv
neg_llr 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instNeg Real.instNeg llr	—	Filter.mp_mem Measure.instOuterMeasureClass Measure.inv_rnDeriv Filter.univ_mem' Pi.neg_apply llr.eq_1 Real.log_inv ENNReal.toReal_inv
stronglyMeasurable_llr 📖	mathematical	—	StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace llr	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_llr

---

← Back to Index