OAI/NumberTheory/TwoPoint/Circuits/CircuitDyadicBudgets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Natural-number budgets for the fixed depth twenty-two application. Using powers of two keeps the exponential error calculation elementary.

  1. def OAI.TwoPointCorrelations.bravermanSamples line 13
  2. def OAI.TwoPointCorrelations.bravermanBase line 14
  3. def OAI.TwoPointCorrelations.bravermanNormExponent line 15
  4. def OAI.TwoPointCorrelations.bravermanErrorExponent line 17
  5. def OAI.TwoPointCorrelations.bravermanSwitches line 18
  6. def OAI.TwoPointCorrelations.bravermanDegree line 20
  7. lemma OAI.TwoPointCorrelations.bravermanSamples_pos line 23
  8. lemma OAI.TwoPointCorrelations.bravermanBase_pos line 27
  9. lemma OAI.TwoPointCorrelations.bravermanSwitches_pos line 32
  10. lemma OAI.TwoPointCorrelations.nat_log_le_of_dyadic line 36
  11. lemma OAI.TwoPointCorrelations.braverman_error_size_budget line 39