OAI/Geometry/LatticeCovering/Sampling.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Folded.eventually_rpow_ratio_bound line 25
  2. lemma OAI.SingleLatticeCovering.Folded.eventually_prime_power line 36
  3. lemma OAI.SingleLatticeCovering.Folded.grid_slack_of_fourth line 57
  4. lemma OAI.SingleLatticeCovering.Folded.eventually_rounding_slack line 69
  5. lemma OAI.SingleLatticeCovering.Folded.numerical_count_tail line 92
  6. lemma OAI.SingleLatticeCovering.Folded.eventually_grid_mass line 105
  7. lemma OAI.SingleLatticeCovering.Sampler.expect_prod line 176
  8. def OAI.SingleLatticeCovering.Sampler.consEquiv line 183
  9. lemma OAI.SingleLatticeCovering.Sampler.expect_cons line 189
  10. lemma OAI.SingleLatticeCovering.Sampler.expect_append line 196
  11. lemma OAI.SingleLatticeCovering.Sampler.expect_mono line 204
  12. lemma OAI.SingleLatticeCovering.Sampler.expect_nonneg line 207
  13. def OAI.SingleLatticeCovering.Sampler.probability line 216
  14. lemma OAI.SingleLatticeCovering.Sampler.probability_nonneg line 220
  15. lemma OAI.SingleLatticeCovering.Sampler.probability_le_one line 224
  16. lemma OAI.SingleLatticeCovering.Sampler.probability_mono line 228
  17. lemma OAI.SingleLatticeCovering.Sampler.probability_union_le line 237
  18. lemma OAI.SingleLatticeCovering.Sampler.probability_false line 246
  19. lemma OAI.SingleLatticeCovering.Sampler.probability_true line 249
  20. lemma OAI.SingleLatticeCovering.Sampler.probability_compl line 252
  21. lemma OAI.SingleLatticeCovering.Sampler.probability_prod line 261
  22. lemma OAI.SingleLatticeCovering.Sampler.probability_fst line 264
  23. lemma OAI.SingleLatticeCovering.Sampler.probability_cons line 273
  24. lemma OAI.SingleLatticeCovering.Sampler.probability_cons_tail line 278
  25. lemma OAI.SingleLatticeCovering.Sampler.probability_append line 285
  26. lemma OAI.SingleLatticeCovering.Sampler.probability_snd line 292
  27. lemma OAI.SingleLatticeCovering.Sampler.probability_gt_le line 298
  28. lemma OAI.SingleLatticeCovering.Sampler.probability_le_of_pointwise line 310
  29. lemma OAI.SingleLatticeCovering.Sampler.expect_sub_right line 324
  30. lemma OAI.SingleLatticeCovering.Sampler.expect_sub_left line 328
  31. lemma OAI.SingleLatticeCovering.Sampler.expect_correlation line 332
  32. def OAI.SingleLatticeCovering.Sampler.step line 338
  33. lemma OAI.SingleLatticeCovering.Sampler.step_nonneg line 340
  34. lemma OAI.SingleLatticeCovering.Sampler.step_mean line 343
  35. lemma OAI.SingleLatticeCovering.Sampler.step_second_moment line 349
  36. def OAI.SingleLatticeCovering.Sampler.binaryAverage line 364
  37. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_zero line 368
  38. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_cons line 371
  39. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_mean line 374
  40. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_nonneg line 382
  41. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_sub_const line 388
  42. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_centered_second_moment line 401
  43. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_variance line 414
  44. lemma OAI.SingleLatticeCovering.Sampler.variance_eq line 422
  45. lemma OAI.SingleLatticeCovering.Sampler.lower_tail_le_variance line 430
  46. lemma OAI.SingleLatticeCovering.Sampler.expected_bad_fraction_le line 442
  47. def OAI.SingleLatticeCovering.Sampler.subsetShift line 455
  48. lemma OAI.SingleLatticeCovering.Sampler.subsetShift_cons line 458
  49. lemma OAI.SingleLatticeCovering.Sampler.subsetShift_append line 462
  50. lemma OAI.SingleLatticeCovering.Sampler.expect_bool line 468
  51. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_eq_expect line 474
  52. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_eq_sum line 485
  53. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_append line 492
  54. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_mono line 504
  55. lemma OAI.SingleLatticeCovering.Sampler.binaryAverage_mul_const line 513
  56. def OAI.SingleLatticeCovering.Sampler.binarySum line 526
  57. lemma OAI.SingleLatticeCovering.Sampler.binarySum_zero line 529
  58. lemma OAI.SingleLatticeCovering.Sampler.binarySum_cons line 532
  59. def OAI.SingleLatticeCovering.Sampler.potential line 538
  60. lemma OAI.SingleLatticeCovering.Sampler.potential_pos line 540
  61. lemma OAI.SingleLatticeCovering.Sampler.potential_square line 544
  62. lemma OAI.SingleLatticeCovering.Sampler.potential_step_failure line 550
  63. lemma OAI.SingleLatticeCovering.Sampler.potential_iteration_failure line 564
  64. lemma OAI.SingleLatticeCovering.Sampler.exp_le_card_mul_potential line 623
  65. lemma OAI.SingleLatticeCovering.Sampler.potential_bound_pointwise line 632
  66. lemma OAI.SingleLatticeCovering.Sampler.potential_bound_binaryAverage line 642
  67. lemma OAI.SingleLatticeCovering.Sampler.indicator_initial_potential line 660
  68. lemma OAI.SingleLatticeCovering.Sampler.second_stage_failure line 693
  69. lemma OAI.SingleLatticeCovering.Sampler.two_stage_failure line 711
  70. lemma OAI.SingleLatticeCovering.Sampler.two_stage_failure_three_delta line 773
  71. lemma OAI.SingleLatticeCovering.Sampler.sampler_explicit_parameters line 793