OAI/NumberTheory/TwoPoint/Fourier/MinorArcGeometric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Literal interval exponential sums used in the minor-arc fourth moment.

  1. lemma OAI.TwoPointCorrelations.additiveCharacter_pow line 12
  2. lemma OAI.TwoPointCorrelations.minor_arc_unit_geometric line 18
  3. def OAI.TwoPointCorrelations.minorArcGeometricBound line 31

    Source documentation

    The resonant case is kept explicit, rather than assigning an infinite value to a reciprocal at zero.

    noncomputable def minorArcGeometricBound (L α : ℝ) : ℝ :=
…
  4. lemma OAI.TwoPointCorrelations.minor_arc_geometric_bound line 35