OAI/NumberTheory/TwoPoint/Circuits/CircuitDyadicErrors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two losses in Braverman's comparison fit a common dyadic error budget. These are scalar inequalities, independent of the circuit.

  1. lemma OAI.TwoPointCorrelations.dyadic_cancel line 10
  2. lemma OAI.TwoPointCorrelations.braverman_exception_loss line 17
  3. lemma OAI.TwoPointCorrelations.braverman_spectral_loss line 36
  4. lemma OAI.TwoPointCorrelations.braverman_total_loss line 58