Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `avgRisk`, `bayesRisk`, `minimaxRisk`	3
Theorems `avgRisk_of_isEmpty`, `avgRisk_of_isEmpty'`, `avgRisk_of_isEmpty''`, `avgRisk_zero_left`, `avgRisk_zero_prior`, `avgRisk_zero_right`, `bayesRisk_of_isEmpty`, `bayesRisk_of_isEmpty'`, `bayesRisk_of_isEmpty''`, `bayesRisk_zero_left`, `bayesRisk_zero_right`, `minimaxRisk_of_isEmpty`, `minimaxRisk_of_isEmpty'`, `minimaxRisk_of_isEmpty''`, `minimaxRisk_zero`	15
Total	18

ProbabilityTheory

Definitions

Name	Category	Theorems
`avgRisk` 📖	CompOp	15 math math: `avgRisk_of_isEmpty'`, `avgRisk_zero_right`, `avgRisk_le_mul'`, `bayesRisk_eq_iInf_measure_of_subsingleton`, `avgRisk_of_isEmpty''`, `avgRisk_le_iSup_risk`, `avgRisk_zero_prior`, `avgRisk_of_isEmpty`, `bayesRisk_le_avgRisk`, `avgRisk_zero_left`, `avgRisk_const_left`, `avgRisk_const_left'`, `avgRisk_le_mul`, `avgRisk_const_right`, `avgRisk_const_right'`
`bayesRisk` 📖	CompOp	24 math math: `bayesRisk_of_subsingleton`, `bayesRisk_of_subsingleton'`, `bayesRisk_eq_iInf_measure_of_subsingleton`, `bayesRisk_compProd_le_bayesRisk`, `bayesRisk_zero_left`, `bayesRisk_const_of_nonempty`, `bayesRisk_le_mul'`, `bayesRisk_le_mul`, `bayesRisk_le_avgRisk`, `bayesRisk_of_isEmpty'`, `bayesRisk_le_iInf`, `bayesRisk_lt_top`, `bayesRisk_le_bayesRisk_comp`, `bayesRisk_of_isEmpty''`, `iSup_bayesRisk_le_minimaxRisk`, `bayesRisk_le_minimaxRisk`, `bayesRisk_le_iInf'`, `bayesRisk_const_of_neZero`, `bayesRisk_const`, `bayesRisk_discard`, `bayesRisk_of_isEmpty`, `bayesRisk_zero_right`, `bayesRisk_le_bayesRisk_map`, `bayesRisk_const'`
`minimaxRisk` 📖	CompOp	6 math math: `minimaxRisk_of_isEmpty`, `iSup_bayesRisk_le_minimaxRisk`, `bayesRisk_le_minimaxRisk`, `minimaxRisk_of_isEmpty'`, `minimaxRisk_of_isEmpty''`, `minimaxRisk_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`avgRisk_of_isEmpty` 📖	mathematical	—	`avgRisk` `ENNReal` `instZeroENNReal`	—	`Kernel.instSubsingletonOfIsEmpty` `avgRisk_zero_left`
`avgRisk_of_isEmpty'` 📖	mathematical	—	`avgRisk` `ENNReal` `instZeroENNReal`	—	`Kernel.instSubsingletonOfIsEmpty` `avgRisk_zero_right`
`avgRisk_of_isEmpty''` 📖	mathematical	—	`avgRisk` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.lintegral_of_isEmpty`
`avgRisk_zero_left` 📖	mathematical	—	`avgRisk` `Kernel` `Kernel.instZero` `ENNReal` `instZeroENNReal`	—	`Kernel.comp_zero` `MeasureTheory.lintegral_zero_measure` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`avgRisk_zero_prior` 📖	mathematical	—	`avgRisk` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.lintegral_zero_measure`
`avgRisk_zero_right` 📖	mathematical	—	`avgRisk` `Kernel` `Kernel.instZero` `ENNReal` `instZeroENNReal`	—	`Kernel.zero_comp` `MeasureTheory.lintegral_zero_measure` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`bayesRisk_of_isEmpty` 📖	mathematical	—	`bayesRisk` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `avgRisk_of_isEmpty` `iInf_pos` `Kernel.instIsMarkovKernelOfIsEmpty` `ciInf_const` `bot_nonempty`
`bayesRisk_of_isEmpty'` 📖	mathematical	—	`bayesRisk` `Top.top` `ENNReal` `instTopENNReal`	—	`Kernel.not_isMarkovKernel_zero` `Kernel.instSubsingletonOfIsEmpty` `iInf_congr_Prop` `avgRisk_of_isEmpty'` `iInf_subtype'`
`bayesRisk_of_isEmpty''` 📖	mathematical	—	`bayesRisk` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `avgRisk_of_isEmpty''` `iInf_subtype'` `ciInf_const` `Kernel.instNonemptySubtypeIsMarkovKernel`
`bayesRisk_zero_left` 📖	mathematical	—	`bayesRisk` `Kernel` `Kernel.instZero` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `avgRisk_zero_left` `iInf_subtype'` `ciInf_const` `Kernel.instNonemptySubtypeIsMarkovKernel`
`bayesRisk_zero_right` 📖	mathematical	—	`bayesRisk` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `avgRisk_zero_prior` `iInf_subtype'` `ciInf_const` `Kernel.instNonemptySubtypeIsMarkovKernel`
`minimaxRisk_of_isEmpty` 📖	mathematical	—	`minimaxRisk` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `Kernel.instSubsingletonOfIsEmpty` `Kernel.comp_zero` `MeasureTheory.lintegral_zero_measure` `ENNReal.iSup_zero` `iInf_pos` `Kernel.instIsMarkovKernelOfIsEmpty` `ciInf_const` `bot_nonempty`
`minimaxRisk_of_isEmpty'` 📖	mathematical	—	`minimaxRisk` `Top.top` `ENNReal` `instTopENNReal`	—	`Kernel.not_isMarkovKernel_zero` `Kernel.instSubsingletonOfIsEmpty` `iInf_congr_Prop` `MeasureTheory.lintegral_of_isEmpty` `ENNReal.iSup_zero` `iInf_subtype'`
`minimaxRisk_of_isEmpty''` 📖	mathematical	—	`minimaxRisk` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `ciSup_of_empty` `bot_eq_zero'` `ENNReal.instCanonicallyOrderedAdd` `iInf_subtype'` `ciInf_const` `Kernel.instNonemptySubtypeIsMarkovKernel`
`minimaxRisk_zero` 📖	mathematical	—	`minimaxRisk` `Kernel` `Kernel.instZero` `ENNReal` `instZeroENNReal`	—	`iInf_congr_Prop` `Kernel.comp_zero` `MeasureTheory.lintegral_zero_measure` `ENNReal.iSup_zero` `iInf_subtype'` `ciInf_const` `Kernel.instNonemptySubtypeIsMarkovKernel`

---

← Back to Index