OAI/Geometry/LatticeCovering/SamplingBounds.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.Sampler.Numeric.cStar line 28
  2. lemma OAI.SingleLatticeCovering.Sampler.Numeric.cStar_pos line 30
  3. lemma OAI.SingleLatticeCovering.Sampler.Numeric.tendsto_rpow_ratio line 32
  4. lemma OAI.SingleLatticeCovering.Sampler.Numeric.tendsto_rpow_mul_exp_neg_rpow line 40
  5. lemma OAI.SingleLatticeCovering.Sampler.Numeric.eventually_first_stage_log line 50
  6. lemma OAI.SingleLatticeCovering.Sampler.Numeric.eventually_thresholds line 68
  7. def OAI.SingleLatticeCovering.Sampler.Numeric.delta line 93
  8. def OAI.SingleLatticeCovering.Sampler.Numeric.theta line 94
  9. lemma OAI.SingleLatticeCovering.Sampler.Numeric.delta_pos line 96
  10. lemma OAI.SingleLatticeCovering.Sampler.Numeric.delta_lt_one line 98
  11. lemma OAI.SingleLatticeCovering.Sampler.Numeric.theta_pos line 101
  12. lemma OAI.SingleLatticeCovering.Sampler.Numeric.half_counts line 104
  13. lemma OAI.SingleLatticeCovering.Sampler.Numeric.rpow_delta_identity line 112
  14. lemma OAI.SingleLatticeCovering.Sampler.Numeric.theta_delta_lower line 117
  15. lemma OAI.SingleLatticeCovering.Sampler.Numeric.two_pow_eq_exp line 126
  16. lemma OAI.SingleLatticeCovering.Sampler.Numeric.two_pow_lower line 129
  17. lemma OAI.SingleLatticeCovering.Sampler.Numeric.potential_errors_le line 139
  18. lemma OAI.SingleLatticeCovering.Sampler.Numeric.delta_sq line 167
  19. lemma OAI.SingleLatticeCovering.Sampler.Numeric.log_eight line 174
  20. lemma OAI.SingleLatticeCovering.Sampler.Numeric.log_four line 178
  21. lemma OAI.SingleLatticeCovering.Sampler.Numeric.first_stage_ratio_le line 183
  22. lemma OAI.SingleLatticeCovering.Sampler.Numeric.failure_tail_le line 232
  23. lemma OAI.SingleLatticeCovering.Sampler.Numeric.failure_tail_le_rpow line 248
  24. lemma OAI.SingleLatticeCovering.Sampler.variance_le_exp line 274
  25. lemma OAI.SingleLatticeCovering.Sampler.sampler_at_thresholds line 286
  26. theorem OAI.SingleLatticeCovering.Sampler.uniform_boolean_sampling line 321
  27. def OAI.SingleLatticeCovering.Bits.bitMass line 366
  28. def OAI.SingleLatticeCovering.Bits.productMass line 368
  29. def OAI.SingleLatticeCovering.Bits.integral line 370
  30. lemma OAI.SingleLatticeCovering.Bits.bitMass_nonneg line 372
  31. lemma OAI.SingleLatticeCovering.Bits.productMass_nonneg line 375
  32. lemma OAI.SingleLatticeCovering.Bits.sum_bitMass line 379
  33. lemma OAI.SingleLatticeCovering.Bits.sum_productMass line 383
  34. lemma OAI.SingleLatticeCovering.Bits.integral_const line 388
  35. lemma OAI.SingleLatticeCovering.Bits.integral_add line 391
  36. lemma OAI.SingleLatticeCovering.Bits.integral_sub line 395
  37. lemma OAI.SingleLatticeCovering.Bits.integral_smul line 399
  38. lemma OAI.SingleLatticeCovering.Bits.integral_sum line 406
  39. lemma OAI.SingleLatticeCovering.Bits.integral_mono line 411
  40. lemma OAI.SingleLatticeCovering.Bits.integral_prod line 417
  41. lemma OAI.SingleLatticeCovering.Bits.integral_coordinate line 423
  42. lemma OAI.SingleLatticeCovering.Bits.integral_two_coordinates line 437
  43. def OAI.SingleLatticeCovering.Bits.count line 463
  44. def OAI.SingleLatticeCovering.Bits.meanCount line 465
  45. lemma OAI.SingleLatticeCovering.Bits.integral_count line 467
  46. lemma OAI.SingleLatticeCovering.Bits.count_sub_mean line 475
  47. lemma OAI.SingleLatticeCovering.Bits.variance_count line 479
  48. theorem OAI.SingleLatticeCovering.Bits.few_selected_probability line 505
  49. def OAI.SingleLatticeCovering.Bits.fairRate line 528
  50. def OAI.SingleLatticeCovering.Bits.likelyBit line 529
  51. def OAI.SingleLatticeCovering.Bits.conditionalBit line 530
  52. def OAI.SingleLatticeCovering.Bits.conditionalMass line 533
  53. lemma OAI.SingleLatticeCovering.Bits.fairRate_nonneg line 536
  54. lemma OAI.SingleLatticeCovering.Bits.fairRate_le_one line 540
  55. lemma OAI.SingleLatticeCovering.Bits.conditionalBit_nonneg line 546
  56. lemma OAI.SingleLatticeCovering.Bits.sum_conditionalBit line 550
  57. lemma OAI.SingleLatticeCovering.Bits.bit_mixture line 555
  58. lemma OAI.SingleLatticeCovering.Bits.conditionalMass_nonneg line 568
  59. lemma OAI.SingleLatticeCovering.Bits.sum_conditionalMass line 571
  60. theorem OAI.SingleLatticeCovering.Bits.product_mixture line 577
  61. theorem OAI.SingleLatticeCovering.Bits.integral_mixture line 585
  62. abbrev OAI.SingleLatticeCovering.Bits.Selected line 606
  63. abbrev OAI.SingleLatticeCovering.Bits.Frozen line 607
  64. def OAI.SingleLatticeCovering.Bits.cubeSplit line 609
  65. def OAI.SingleLatticeCovering.Bits.filled line 612
  66. lemma OAI.SingleLatticeCovering.Bits.conditionalMass_split line 615
  67. lemma OAI.SingleLatticeCovering.Bits.conditional_integral_eq_subcube line 630
  68. lemma OAI.SingleLatticeCovering.Bits.count_eq_card_selected line 652
  69. theorem OAI.SingleLatticeCovering.Bits.mixture_lower_bound line 658
  70. lemma OAI.SingleLatticeCovering.Bits.expect_restrict line 689