OAI/Probability/SKGap/Localization/PoissonBinomialProbability.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGapCutoff.Clock.poisson_to_binomial_in_probability line 135
2. def OAI.SKGapCutoff.residualAttempt line 193
3. lemma OAI.SKGapCutoff.residualAttempt_apply line 197
4. lemma OAI.SKGapCutoff.attempt_eq_lazy_residual line 202
5. lemma OAI.SKGapCutoff.residualAttempt_const line 206
6. lemma OAI.SKGapCutoff.residualAttempt_pow_const line 213
7. lemma OAI.SKGapCutoff.residualAttempt_nonneg line 219
8. lemma OAI.SKGapCutoff.residualAttempt_pow_nonneg line 235
9. lemma OAI.SKGapCutoff.residualAttempt_pow_abs_le line 245
10. lemma OAI.SKGapCutoff.residual_semigroup_uniformization line 260
11. lemma OAI.SKGapCutoff.residual_poisson_hasSum line 282
12. lemma OAI.SKGapCutoff.natCastCLM_apply line 296
13. lemma OAI.SKGapCutoff.residual_binomial_sum line 302
14. lemma OAI.SKGapCutoff.residual_binomial_hasSum line 315
15. lemma OAI.SKGapCutoff.gibbsExpectation_abs_le_one line 325
16. lemma OAI.SKGapCutoff.residual_test_bound line 337
17. lemma OAI.SKGapCutoff.residual_poisson_test line 345
18. lemma OAI.SKGapCutoff.residual_binomial_test line 357
19. lemma OAI.SKGapCutoff.totalVariation_test_bound line 365
20. lemma OAI.SKGapCutoff.continuous_test_bound line 379
21. lemma OAI.SKGapCutoff.totalVariation_has_test line 388
22. lemma OAI.SKGapCutoff.worstDiscrete_has_test line 404
23. lemma OAI.SKGapCutoff.semigroup_add_eq_comp line 419
24. lemma OAI.SKGapCutoff.continuousKernel_add line 427
25. lemma OAI.SKGapCutoff.worstContinuous_add_le line 433
26. lemma OAI.SKGapCutoff.worstContinuous_mono_time line 450