OAI/NumberTheory/TwoPoint/Bounds/FinalErrorScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual rare-site and summed block-boundary errors are below the same exp(-J) saving as the principal terms.

  1. lemma OAI.TwoPointCorrelations.eventually_rare_error_saving line 12
  2. lemma OAI.TwoPointCorrelations.eventually_bin_error_saving line 24