OAI/Probability/SKRatio/Dynamics/LogQuadratic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatioClock.Clock.logQuadratic line 14
  2. lemma OAI.SKRatioClock.Clock.logQuadratic_mul_sq line 17
  3. lemma OAI.SKRatioClock.Clock.continuousAt_logQuadratic line 26
  4. def OAI.SKRatioClock.Clock.poissonMass line 65
  5. lemma OAI.SKRatioClock.Clock.poissonMass_stirling line 68
  6. theorem OAI.SKRatioClock.Clock.poisson_local_limit line 91
  7. def OAI.SKRatioClock.Clock.centralIndex line 135
  8. lemma OAI.SKRatioClock.Clock.center_ratio_tendsto line 138
  9. lemma OAI.SKRatioClock.Clock.center_tendsto_atTop line 151
  10. lemma OAI.SKRatioClock.Clock.centralIndex_atTop line 159
  11. lemma OAI.SKRatioClock.Clock.centralIndex_deviation line 163
  12. lemma OAI.SKRatioClock.Clock.centralIndex_ratio line 195
  13. theorem OAI.SKRatioClock.Clock.poisson_scaled_local line 208
  14. theorem OAI.SKRatioClock.Clock.poisson_histogram_pointwise line 248
  15. def OAI.SKRatioClock.Clock.binomialMass line 256
  16. lemma OAI.SKRatioClock.Clock.binomialMass_poisson line 259
  17. lemma OAI.SKRatioClock.Clock.gaussian_formula line 281
  18. lemma OAI.SKRatioClock.Clock.index_atTop_of_ratio line 294
  19. lemma OAI.SKRatioClock.Clock.centralIndex_le line 301
  20. lemma OAI.SKRatioClock.Clock.complementIndex_ratio line 310
  21. lemma OAI.SKRatioClock.Clock.complementIndex_deviation line 318
  22. lemma OAI.SKRatioClock.Clock.gaussian_product_quotient line 326
  23. theorem OAI.SKRatioClock.Clock.binomial_histogram_pointwise line 354