OAI/Analysis/RotationWeights/TrialBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.product_many_failures_bound line 43
  2. lemma OAI.CircleSampling.product_many_failures_exp_bound line 77
  3. def OAI.CircleSampling.phaseUnionBound line 93
  4. lemma OAI.CircleSampling.phase_failure_count_lower line 96
  5. lemma OAI.CircleSampling.phase_union_numeric line 102
  6. lemma OAI.CircleSampling.tendsto_phaseUnionBound line 131
  7. lemma OAI.CircleSampling.eventually_phase_failure_small line 143
  8. lemma OAI.CircleSampling.phase_few_successes_subset line 152
  9. lemma OAI.CircleSampling.phase_cover_union_bound line 168
  10. lemma OAI.CircleSampling.intervalLaw_ae_inner line 216
  11. lemma OAI.CircleSampling.intervalLaw_ae_phase line 221
  12. lemma OAI.CircleSampling.pi_intervalLaw_ae_good line 231
  13. lemma OAI.CircleSampling.pi_intervalLaw_ae_all_integerPhases line 252
  14. lemma OAI.CircleSampling.finite_threshold_bound line 277
  15. lemma OAI.CircleSampling.exists_good_finite_family line 293
  16. lemma OAI.CircleSampling.eventually_trial_budget line 331
  17. lemma OAI.CircleSampling.exists_ideal_trial line 337