OAI/NumberTheory/TwoPoint/Bounds/DeletionErrorScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-catalog error in the three deletion estimates is negligible even when every bin uses a different interval.

  1. lemma OAI.TwoPointCorrelations.deletion_comparison_error_bound line 15
  2. theorem OAI.TwoPointCorrelations.eventually_deletion_comparison_error line 80