OAI/Probability/SKGap/Localization/LogQuadratic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Clock.logQuadratic line 118
  2. lemma OAI.SKGapCutoff.Clock.logQuadratic_mul_sq line 121
  3. lemma OAI.SKGapCutoff.Clock.continuousAt_logQuadratic line 130
  4. def OAI.SKGapCutoff.Clock.poissonMass line 169
  5. lemma OAI.SKGapCutoff.Clock.poissonMass_stirling line 172
  6. theorem OAI.SKGapCutoff.Clock.poisson_local_limit line 195
  7. def OAI.SKGapCutoff.Clock.centralIndex line 239
  8. lemma OAI.SKGapCutoff.Clock.center_ratio_tendsto line 242
  9. lemma OAI.SKGapCutoff.Clock.center_tendsto_atTop line 255
  10. lemma OAI.SKGapCutoff.Clock.centralIndex_atTop line 263
  11. lemma OAI.SKGapCutoff.Clock.centralIndex_deviation line 267
  12. lemma OAI.SKGapCutoff.Clock.centralIndex_ratio line 299
  13. theorem OAI.SKGapCutoff.Clock.poisson_scaled_local line 312
  14. theorem OAI.SKGapCutoff.Clock.poisson_histogram_pointwise line 352
  15. def OAI.SKGapCutoff.Clock.binomialMass line 360
  16. lemma OAI.SKGapCutoff.Clock.binomialMass_poisson line 363
  17. lemma OAI.SKGapCutoff.Clock.gaussian_formula line 385
  18. lemma OAI.SKGapCutoff.Clock.index_atTop_of_ratio line 398
  19. lemma OAI.SKGapCutoff.Clock.centralIndex_le line 405
  20. lemma OAI.SKGapCutoff.Clock.complementIndex_ratio line 414
  21. lemma OAI.SKGapCutoff.Clock.complementIndex_deviation line 422
  22. lemma OAI.SKGapCutoff.Clock.gaussian_product_quotient line 430
  23. theorem OAI.SKGapCutoff.Clock.binomial_histogram_pointwise line 458