MinorArcWindowInterval.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact finite cofactor intervals for discrete short-sum origins.

def OAI.TwoPointCorrelations.minorArcWindowInterval line 12
Source documentation
The upper cofactor cutoff is exclusive.
```
def minorArcWindowInterval (M A k H : ℕ) : Finset ℕ :=
…
```
lemma OAI.TwoPointCorrelations.mem_minorArcWindowInterval line 15
lemma OAI.TwoPointCorrelations.minor_arc_interval_length line 27
lemma OAI.TwoPointCorrelations.minor_arc_geometric_mono line 44
lemma OAI.TwoPointCorrelations.minor_arc_geometric_window line 51
lemma OAI.TwoPointCorrelations.minor_arc_four_window_kernel line 60
Source documentation
The intersection of four origin windows is again one interval; its length is controlled by the first prime, regardless of the other origins.
```
lemma minor_arc_four_window_kernel (M A B C D k l r s H : ℕ)
    (hA : 0 < A) (α : ℝ) :
    ‖∑ m ∈ (minorArcWindowInterval M A k H ∩ minorArcWindowInterval M B l H) ∩
        (minorArcWindowInterval M C r H ∩ minorArcWindowInterval M D s H),
      additiveCharacter α m‖ ≤ minorArcGeometricBound ((H : ℝ) / A + 1) α := by
…
```
Mentions: OAI.TwoPointCorrelations.minorArcWindowInterval, OAI.TwoPointCorrelations.additiveCharacter, OAI.TwoPointCorrelations.minorArcGeometricBound