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_inv_left_eq_smul_right, llr_smul_left, llr_smul_nnreal_left, llr_smul_nnreal_right, llr_smul_nnreal_same, llr_smul_right, llr_smul_same, llr_tilted_left, llr_tilted_right, measurable_llr, neg_llr, stronglyMeasurable_llr	25
Total	26

MeasureTheory

Definitions

Name	Category	Theorems
llr 📖	CompOp	39 math math: InformationTheory.integrable_klFun_rnDeriv_iff, llr_self, llr_smul_inv_left_eq_smul_right, InformationTheory.integral_llr_add_mul_log_nonneg, llr_smul_nnreal_same, exp_llr_of_ac', InformationTheory.klDiv_eq_top_iff, InformationTheory.toReal_klDiv, llr_tilted_right, InformationTheory.integral_llr_add_sub_measure_univ_nonneg, integral_llr_tilted_left, InformationTheory.integral_klFun_rnDeriv, InformationTheory.klDiv_of_ac_of_integrable, InformationTheory.klDiv_def, InformationTheory.integrable_llr_compProd_iff, InformationTheory.integrable_llr_of_integrable_llr_compProd, InformationTheory.klDiv_ne_top_iff, llr_smul_nnreal_left, InformationTheory.klDiv_eq_integral_klFun, llr_smul_same, stronglyMeasurable_llr, InformationTheory.integral_llr_compProd_eq_add, integral_rnDeriv_mul_log, InformationTheory.toReal_klDiv_of_measure_eq, exp_neg_llr, exp_neg_llr', measurable_llr, integrable_llr_tilted_right, llr_tilted_left, exp_llr_of_ac, integrable_llr_tilted_left, llr_smul_right, llr_def, integral_llr_tilted_right, exp_llr, llr_smul_left, llr_smul_nnreal_right, 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	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing llr Measure.tilted	—	integrable_congr llr_tilted_left IsFiniteMeasure.toSigmaFinite Integrable.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing llr Measure.tilted	—	integrable_congr llr_tilted_right IsFiniteMeasure.toSigmaFinite Integrable.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField llr Measure.tilted Real.instSub Real.instAdd Real.log Real.exp	—	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 Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField llr Measure.tilted Real.instAdd Real.instSub Real.log Real.exp	—	integral_congr_ae llr_tilted_right IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure integral_neg integral_add Integrable.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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_inv_left_eq_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 ENNReal.instInv	—	Filter.mp_mem Measure.instOuterMeasureClass IsScalarTower.right llr_smul_right llr_smul_left Filter.univ_mem' ENNReal.toReal_inv Real.log_inv sub_eq_add_neg
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_nnreal_left 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr NNReal Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.instAdd Real.log NNReal.toReal	—	Measure.instOuterMeasureClass IsScalarTower.right Measure.coe_nnreal_smul Filter.mp_mem llr_smul_left Filter.univ_mem'
llr_smul_nnreal_right 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr NNReal Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real.instSub Real.log NNReal.toReal	—	Measure.instOuterMeasureClass IsScalarTower.right Measure.coe_nnreal_smul Filter.mp_mem llr_smul_right Filter.univ_mem'
llr_smul_nnreal_same 📖	mathematical	Measure.AbsolutelyContinuous	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr NNReal Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	Measure.instOuterMeasureClass IsScalarTower.right Filter.mp_mem llr_smul_same Filter.univ_mem'
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_smul_same 📖	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	—	Measure.instOuterMeasureClass IsScalarTower.right CanLift.prf ENNReal.canLift Filter.mp_mem Measure.AbsolutelyContinuous.ae_le Measure.rnDeriv_smul_same Nat.cast_zero Filter.univ_mem'
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 Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr Measure.tilted Real.instAdd Real.instSub Real.log integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.exp	—	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 Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass llr Measure.tilted Real.instAdd Real.instNeg Real.log integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.exp	—	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