HalaszSmallDefect.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed multiple of the degree gives the small quadratic defect needed in the double mean-value argument.

lemma OAI.TwoPointCorrelations.halasz_classical_ratio_block line 9
lemma OAI.TwoPointCorrelations.halasz_classical_defect_ten_blocks line 24
theorem OAI.TwoPointCorrelations.halasz_classical_selected_moment line 46
Source documentation
The selected moment has a defect at most k^2/2048, uniformly in its endpoint. Its explicit constant is bounded separately.
```
theorem halasz_classical_selected_moment : ∃ R₀ : ℕ, ∀ k : ℕ, 2≤k →
    ∀ N : ℕ, 1≤N →
    (halaszVinogradovCount ((10*k+1)*k) k N:ℝ) ≤
      (halaszIterationConstant R₀ k (10*k):ℝ)*
        (N:ℝ)^(2*(((10*k+1)*k:ℕ):ℝ)-(halaszTotalDegree k:ℝ)+(k:ℝ)^2/2048) := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszVinogradovCount, OAI.TwoPointCorrelations.halaszIterationConstant, OAI.TwoPointCorrelations.halaszTotalDegree