OAI/NumberTheory/TwoPoint/Bounds/RoughCutoffProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite rough sieve with its cutoff left explicit, for both one linear form and the additive four-form system.

  1. theorem OAI.TwoPointCorrelations.rough_interval_probability_cutoff line 13
  2. theorem OAI.TwoPointCorrelations.rough_cube_probability_cutoff line 45