OAI/Probability/SignedSweeps/BalancedErrors.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.sweepColors line 10
  2. lemma OAI.SignedSweeps.sweepColors_pos line 12
  3. lemma OAI.SignedSweeps.sweepColors_le_size line 16
  4. lemma OAI.SignedSweeps.sweepColors_le_twice line 22
  5. lemma OAI.SignedSweeps.two_pow_rpow line 30
  6. lemma OAI.SignedSweeps.two_pow_le_depth_rpow line 34
  7. lemma OAI.SignedSweeps.depth_rpow_le_two_pow line 41
  8. lemma OAI.SignedSweeps.balanced_depth_sizes line 48
  9. lemma OAI.SignedSweeps.cast_nat_sqrt_le line 66
  10. lemma OAI.SignedSweeps.typedLineError_bound line 71
  11. lemma OAI.SignedSweeps.log_size_radius line 110
  12. lemma OAI.SignedSweeps.depth_power_log_eventually line 114
  13. lemma OAI.SignedSweeps.balanced_clipping_error line 141
  14. theorem OAI.SignedSweeps.balanced_recurrence_error_eventually line 190