OAI/NumberTheory/TwoPoint/Circuits/CircuitMixedLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The half-uniform input law in Braverman's proof. Small exceptional probability for this law bounds both the uniform and supplied probabilities.

  1. def OAI.TwoPointCorrelations.cubeDensityLaw line 13
  2. lemma OAI.TwoPointCorrelations.cubeDensityLaw_average line 19
  3. lemma OAI.TwoPointCorrelations.half_uniform_density_mean line 28
  4. def OAI.TwoPointCorrelations.mixedCubeLaw line 37
  5. lemma OAI.TwoPointCorrelations.mixedCubeLaw_probability line 42
  6. theorem OAI.TwoPointCorrelations.mixedCubeLaw_exception_bounds line 57