OAI/Geometry/LatticeCovering/GaussianRates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.GaussianNumerics.A line 11
  2. def OAI.SingleLatticeCovering.GaussianNumerics.B line 12
  3. lemma OAI.SingleLatticeCovering.GaussianNumerics.A_pos line 13
  4. lemma OAI.SingleLatticeCovering.GaussianNumerics.A_large line 14
  5. lemma OAI.SingleLatticeCovering.GaussianNumerics.B_pos line 15
  6. lemma OAI.SingleLatticeCovering.GaussianNumerics.normalizer_log line 17
  7. lemma OAI.SingleLatticeCovering.GaussianNumerics.floor_inv_bound line 21
  8. lemma OAI.SingleLatticeCovering.GaussianNumerics.floor_le_one line 39
  9. lemma OAI.SingleLatticeCovering.GaussianNumerics.polynomial_exp_decay line 48
  10. def OAI.SingleLatticeCovering.GaussianNumerics.errBound line 61
  11. def OAI.SingleLatticeCovering.GaussianNumerics.tailBound line 62
  12. lemma OAI.SingleLatticeCovering.GaussianNumerics.errBound_tendsto line 63
  13. lemma OAI.SingleLatticeCovering.GaussianNumerics.tailBound_tendsto line 66
  14. lemma OAI.SingleLatticeCovering.GaussianNumerics.gaussian_prefactor_bound line 73
  15. lemma OAI.SingleLatticeCovering.GaussianNumerics.volume_parameter_bound line 97
  16. lemma OAI.SingleLatticeCovering.GaussianNumerics.powerCoeff_bound line 120
  17. lemma OAI.SingleLatticeCovering.GaussianNumerics.uniform_error_bound line 129
  18. lemma OAI.SingleLatticeCovering.GaussianNumerics.uniform_ball_error line 153
  19. lemma OAI.SingleLatticeCovering.GaussianNumerics.kernel_normalizer_bound line 168
  20. lemma OAI.SingleLatticeCovering.GaussianNumerics.tail_exponent_bound line 181
  21. lemma OAI.SingleLatticeCovering.GaussianNumerics.uniform_tail_bound line 192
  22. def OAI.SingleLatticeCovering.GaussianNumerics.shellRate line 223
  23. def OAI.SingleLatticeCovering.GaussianNumerics.denRate line 224
  24. def OAI.SingleLatticeCovering.GaussianNumerics.shellBound line 225
  25. lemma OAI.SingleLatticeCovering.GaussianNumerics.shellRate_tendsto line 227
  26. lemma OAI.SingleLatticeCovering.GaussianNumerics.denRate_tendsto line 242
  27. lemma OAI.SingleLatticeCovering.GaussianNumerics.shellBound_tendsto line 248
  28. lemma OAI.SingleLatticeCovering.GaussianNumerics.shell_term_bound line 257
  29. lemma OAI.SingleLatticeCovering.GaussianNumerics.denominator_identity line 278
  30. lemma OAI.SingleLatticeCovering.GaussianNumerics.markov_term_bound line 287
  31. lemma OAI.SingleLatticeCovering.GaussianNumerics.uniform_shell_bound line 297
  32. lemma OAI.SingleLatticeCovering.GaussianNumerics.uniform_numeric_conditions line 315
  33. theorem OAI.SingleLatticeCovering.GaussianNumerics.eventually_local_position line 341