OAI/NumberTheory/TwoPoint/Circuits/CircuitSamplingGrid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A logarithmic grid of repeated Bernoulli samplers isolates a member of every nonempty marked set, with failure at most (7/8)^s.

  1. def OAI.TwoPointCorrelations.dyadicCubeLaw line 14
  2. abbrev OAI.TwoPointCorrelations.GateSamplingChoices line 21
  3. def OAI.TwoPointCorrelations.gateSamplingLaw line 23
  4. theorem OAI.TwoPointCorrelations.gateSamplingLaw_failure line 27