OAI/Probability/SKGap/Localization/PoissonWeight.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.totalVariation_mixture_le line 74
2. lemma OAI.SKGapCutoff.discreteKernel_add line 93
3. lemma OAI.SKGapCutoff.worstDiscrete_add_le line 99
4. lemma OAI.SKGapCutoff.worstDiscrete_antitone line 115
5. def OAI.SKGapCutoff.poissonWeight line 122
6. lemma OAI.SKGapCutoff.poissonWeight_nonneg line 125
7. lemma OAI.SKGapCutoff.poissonWeight_hasSum line 128
8. lemma OAI.SKGapCutoff.poissonWeight_exp_hasSum line 131
9. lemma OAI.SKGapCutoff.poisson_head_le line 144
10. lemma OAI.SKGapCutoff.continuousKernel_poisson_hasSum line 169
11. lemma OAI.SKGapCutoff.continuousKernel_poisson_integral line 183
12. lemma OAI.SKGapCutoff.integrable_discreteKernel_poisson line 190
13. lemma OAI.SKGapCutoff.totalVariation_integral_le line 198
14. lemma OAI.SKGapCutoff.integrable_totalVariation_poisson line 214
15. lemma OAI.SKGapCutoff.poisson_head_integral line 223
16. lemma OAI.SKGapCutoff.continuous_le_poisson_head_add_discrete line 236
17. lemma OAI.SKGapCutoff.exists_poisson_head_exponent line 275
18. lemma OAI.SKGapCutoff.poisson_head_tendsto_zero line 299
19. lemma OAI.SKGapCutoff.disorderLimit_one_of_clock_transfer line 320
20. lemma OAI.SKGapCutoff.cutoffTime_tendsto_atTop line 338
21. theorem OAI.SKGapCutoff.discrete_lower_from_continuous line 346