OAI/NumberTheory/TwoPoint/Fourier/MinorArcTypicalRemoval.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the typical-set restriction costs its actual missing density. This comparison is uniform in the additive frequency and pays the discarded integers once, before either the major- or minor-arc estimate is applied.

  1. lemma OAI.TwoPointCorrelations.minor_arc_typical_pointwise_error line 16
  2. lemma OAI.TwoPointCorrelations.minor_arc_typical_error_sum line 26
  3. lemma OAI.TwoPointCorrelations.minor_arc_typical_density_sum line 52
  4. theorem OAI.TwoPointCorrelations.minor_arc_remove_typical line 73