MinorArcOriginCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The support of four simultaneous short windows has size O(X H³).

lemma OAI.TwoPointCorrelations.minor_arc_origin_interval_card line 12

theorem OAI.TwoPointCorrelations.minor_arc_origin_quadruples line 19

Source documentation

Only the first origin costs X; each of the other three origins costs at most 3H+1, independently of the prime quadruple.

theorem minor_arc_origin_quadruples (X H A B C D : ℕ) (hA : 0 < A)
    (hB : B ≤ 2 * A) (hC : C ≤ 2 * A) (hD : D ≤ 2 * A)
    (T : Finset ((ℕ × ℕ) × (ℕ × ℕ)))
    (hT : ∀ v ∈ T, v.1.1 < X ∧ ∃ m : ℕ,
      (v.1.1 < A * m ∧ A * m ≤ v.1.1 + H) ∧
      (v.1.2 < B * m ∧ B * m ≤ v.1.2 + H) ∧
      (v.2.1 < C * m ∧ C * m ≤ v.2.1 + H) ∧
      (v.2.2 < D * m ∧ D * m ≤ v.2.2 + H)) :
    T.card ≤ X * (3 * H + 1) ^ 3 := by
…