OAI/NumberTheory/GaussianMoat/SignConcentration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.fairCoin line 11
  2. instance OAI.GaussianMoat.fairCoin_probability line 12
  3. def OAI.GaussianMoat.signMeasure line 15
  4. instance OAI.GaussianMoat.signMeasure_probability line 17
  5. theorem OAI.GaussianMoat.fairCoin_mean line 21
  6. theorem OAI.GaussianMoat.sign_hoeffding line 32
  7. def OAI.GaussianMoat.SplitSieve.eligible line 56
  8. def OAI.GaussianMoat.SplitSieve.lineLog line 59
  9. theorem OAI.GaussianMoat.SplitSieve.eligible_log_bound line 63
  10. theorem OAI.GaussianMoat.SplitSieve.lineLog_mean line 85
  11. theorem OAI.GaussianMoat.SplitSieve.lineLog_tail line 104