OAI/Probability/SKBarriers/Coverage/FiniteCoverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.finiteMass line 14
2. def OAI.SK.Analytic.conditionalWeights line 16
3. theorem OAI.SK.Analytic.finiteMass_nonneg line 19
4. theorem OAI.SK.Analytic.finiteMass_mono line 22
5. theorem OAI.SK.Analytic.conditionalWeights_nonneg line 26
6. theorem OAI.SK.Analytic.conditionalWeights_sum line 33
7. def OAI.SK.Analytic.finiteOverlapMass line 41
8. theorem OAI.SK.Analytic.weightedOverlapMass_conditional line 44
9. theorem OAI.SK.Analytic.finiteOverlapMass_eq_rows line 72
10. theorem OAI.SK.Analytic.finite_coverage_of_pair_bound line 81