Basic

📁 Source: Mathlib/Probability/Decision/Risk/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems avgRisk_const_left, avgRisk_const_left', avgRisk_const_right, avgRisk_const_right', avgRisk_le_iSup_risk, avgRisk_le_mul, avgRisk_le_mul', bayesRisk_compProd_le_bayesRisk, bayesRisk_const, bayesRisk_const', bayesRisk_const_of_neZero, bayesRisk_const_of_nonempty, bayesRisk_discard, bayesRisk_eq_iInf_measure_of_subsingleton, bayesRisk_le_avgRisk, bayesRisk_le_bayesRisk_comp, bayesRisk_le_bayesRisk_map, bayesRisk_le_iInf, bayesRisk_le_iInf', bayesRisk_le_minimaxRisk, bayesRisk_le_mul, bayesRisk_le_mul', bayesRisk_lt_top, bayesRisk_of_subsingleton, bayesRisk_of_subsingleton', iSup_bayesRisk_le_minimaxRisk	26
Total	26

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
avgRisk_const_left 📖	mathematical	—	avgRisk Kernel.const MeasureTheory.lintegral MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike	—	—
avgRisk_const_left' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	avgRisk Kernel.const MeasureTheory.lintegral MeasureTheory.Measure.bind DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike	—	avgRisk_const_left MeasureTheory.lintegral_lintegral_swap MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel Measurable.aemeasurable
avgRisk_const_right 📖	mathematical	—	avgRisk Kernel.const MeasureTheory.lintegral	—	avgRisk_const_right' MeasureTheory.IsProbabilityMeasure.measure_univ IsMarkovKernel.is_probability_measure' one_mul
avgRisk_const_right' 📖	mathematical	—	avgRisk Kernel.const MeasureTheory.lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike Set.univ	—	IsScalarTower.right Kernel.const_comp MeasureTheory.lintegral_smul_measure
avgRisk_le_iSup_risk 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder avgRisk iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral DFunLike.coe Kernel MeasureTheory.Measure Kernel.instFunLike Kernel.comp	—	MeasureTheory.lintegral_le_iSup
avgRisk_le_mul 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	avgRisk	—	LE.le.trans avgRisk_le_mul' isEmpty_or_nonempty Kernel.bound_eq_zero_of_isEmpty MulZeroClass.mul_zero MeasureTheory.IsProbabilityMeasure.measure_univ mul_one ENNReal.instCanonicallyOrderedAdd Kernel.bound_eq_zero_of_isEmpty' Kernel.bound_eq_one
avgRisk_le_mul' 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	avgRisk Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Kernel.bound DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	MeasureTheory.lintegral_mono_fn' le_refl MeasureTheory.lintegral_const Kernel.comp_apply' MeasurableSet.univ mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Kernel.measure_le_bound
bayesRisk_compProd_le_bayesRisk 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk Prod.instMeasurableSpace Kernel.compProd	—	Measurable.fst measurable_id' Kernel.deterministic_comp_eq_map Kernel.fst_eq Kernel.fst_compProd bayesRisk_le_bayesRisk_comp Kernel.isMarkovKernel_deterministic
bayesRisk_const 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk Kernel.const iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral	—	bayesRisk_const_of_neZero MeasureTheory.IsProbabilityMeasure.neZero MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.IsProbabilityMeasure.measure_univ mul_one
bayesRisk_const' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasureTheory.lintegral instZeroENNReal	bayesRisk Kernel.const iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	le_antisymm LE.le.trans_eq bayesRisk_le_iInf' avgRisk_const_left' Kernel.IsFiniteKernel.isSFiniteKernel IsZeroOrMarkovKernel.isFiniteKernel IsMarkovKernel.IsZeroOrMarkovKernel le_trans MeasureTheory.Measure.comp_apply_univ ENNReal.iInf_mul' iInf_mono MeasureTheory.lintegral_mul_const Measurable.fun_comp Measurable.prodMk measurable_id' measurable_const le_refl MeasureTheory.iInf_mul_le_lintegral
bayesRisk_const_of_neZero 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk Kernel.const iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	bayesRisk_const' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite instIsEmptyFalse
bayesRisk_const_of_nonempty 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk Kernel.const iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	bayesRisk_const' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite instIsEmptyFalse
bayesRisk_discard 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk PUnit.instMeasurableSpace Kernel.discard iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral	—	Kernel.discard_eq_const bayesRisk_const MeasureTheory.Measure.dirac.isProbabilityMeasure
bayesRisk_eq_iInf_measure_of_subsingleton 📖	mathematical	—	bayesRisk iInf ENNReal MeasureTheory.Measure ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.IsProbabilityMeasure avgRisk Kernel.const	—	isEmpty_or_nonempty bayesRisk_of_isEmpty iInf_congr_Prop avgRisk_of_isEmpty iInf_subtype' ciInf_const MeasureTheory.instNonemptySubtypeMeasureIsProbabilityMeasure bayesRisk.eq_1 IsMarkovKernel.isProbabilityMeasure Kernel.ext MeasureTheory.Measure.ext Subtype.coe_eta Equiv.iInf_comp
bayesRisk_le_avgRisk 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk avgRisk	—	iInf₂_le
bayesRisk_le_bayesRisk_comp 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk Kernel.comp	—	iInf_congr_Prop Kernel.comp_assoc iInf_le_of_le Kernel.IsMarkovKernel.comp le_rfl
bayesRisk_le_bayesRisk_map 📖	mathematical	Measurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk Kernel.map	—	Kernel.deterministic_comp_eq_map bayesRisk_le_bayesRisk_comp Kernel.isMarkovKernel_deterministic
bayesRisk_le_iInf 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral	—	LE.le.trans_eq bayesRisk_le_iInf' MeasureTheory.IsProbabilityMeasure.measure_univ IsMarkovKernel.is_probability_measure' mul_one
bayesRisk_le_iInf' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike Set.univ	—	iInf_le_of_le iInf_congr_Prop avgRisk_const_right' mul_comm iInf_pos Kernel.const.instIsMarkovKernel MeasureTheory.Measure.dirac.isProbabilityMeasure MeasureTheory.lintegral_mono_fn' le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid MeasureTheory.lintegral_dirac' Measurable.fun_comp Measurable.prodMk measurable_const measurable_id'
bayesRisk_le_minimaxRisk 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bayesRisk minimaxRisk	—	iInf₂_mono avgRisk_le_iSup_risk
bayesRisk_le_mul 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	bayesRisk	—	LE.le.trans bayesRisk_le_mul' isEmpty_or_nonempty Kernel.bound_eq_zero_of_isEmpty MulZeroClass.mul_zero MeasureTheory.IsProbabilityMeasure.measure_univ mul_one ENNReal.instCanonicallyOrderedAdd Kernel.bound_eq_one
bayesRisk_le_mul' 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	bayesRisk Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Kernel.bound DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	—	LE.le.trans bayesRisk_le_avgRisk Kernel.const.instIsMarkovKernel MeasureTheory.Measure.dirac.isProbabilityMeasure avgRisk_le_mul' isEmpty_or_nonempty Kernel.bound_eq_zero_of_isEmpty MulZeroClass.mul_zero Kernel.bound_eq_zero_of_isEmpty' MulZeroClass.zero_mul Kernel.bound_eq_one mul_one
bayesRisk_lt_top 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	Preorder.toLT bayesRisk Top.top instTopENNReal	—	LE.le.trans_lt bayesRisk_le_mul' Kernel.bound_lt_top ENNReal.instNoZeroDivisors
bayesRisk_of_subsingleton 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral	—	bayesRisk_of_subsingleton' MeasureTheory.IsProbabilityMeasure.measure_univ IsMarkovKernel.is_probability_measure' mul_one
bayesRisk_of_subsingleton' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	bayesRisk iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Kernel Kernel.instFunLike Set.univ	—	le_antisymm bayesRisk_le_iInf' bayesRisk_eq_iInf_measure_of_subsingleton iInf_congr_Prop avgRisk_const_right' LE.le.trans_eq MeasureTheory.iInf_le_lintegral MeasureTheory.lintegral_lintegral_swap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Kernel.measurable_coe MeasurableSet.univ AEMeasurable.mul ENNReal.instMeasurableMul₂ Measurable.comp_aemeasurable' AEMeasurable.prodMk AEMeasurable.snd aemeasurable_id AEMeasurable.fst MeasureTheory.lintegral_mul_const Measurable.fun_comp Measurable.prodMk measurable_const measurable_id' mul_comm
iSup_bayesRisk_le_minimaxRisk 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder iSup MeasureTheory.Measure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasureTheory.IsProbabilityMeasure bayesRisk minimaxRisk	—	iSup₂_le bayesRisk_le_minimaxRisk

---

← Back to Index