OAI/NumberTheory/TwoPoint/Fourier/MinorArcRamareError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The combined denominator and prime-extraction error for the additive short-window argument. Both errors are supported on prime squares.

  1. def OAI.TwoPointCorrelations.minorArcRamareApprox line 13
  2. lemma OAI.TwoPointCorrelations.minor_arc_ramare_pointwise line 17
  3. lemma OAI.TwoPointCorrelations.minor_arc_typical_ramare_pointwise line 51