VaughanDyadicEstimate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.Vaughan.typeIIBlock_eq_bilinear line 11
lemma OAI.Problem337.Vaughan.dyadic_row_length_le line 34
lemma OAI.Problem337.Vaughan.mangoldt_column_energy_le line 44
Source documentation
The elementary bounded-weight column energy, used only as a normalization inside the actual Type II block estimate.
```
lemma mangoldt_column_energy_le (V T : ℕ) :
    (∑ n ∈ Ioc V T, ‖(Λ n : ℂ)‖ ^ 2) ≤ (T : ℝ) * (Real.log T) ^ 2 := by
…
```

theorem OAI.Problem337.Vaughan.typeIIBlock_sq_le_raw line 62

Source documentation

A genuine rational-approximation estimate for one actual Vaughan block. All coefficient energies and correlations have been evaluated explicitly.

theorem typeIIBlock_sq_le_raw
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N U V j : ℕ) :
    ‖typeIIBlock N U V j (fun k => VaughanBilinear.phase (θ * k))‖ ^ 2 ≤
      ((2 ^ (j + 1) : ℕ) * (1 + Real.log (2 ^ (j + 1) : ℕ)) ^ 3) *
        ((2 * ((N / 2 ^ j : ℕ) : ℝ) / q + 1) *
          (2 * ((2 ^ j : ℕ) : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))))) *
            (((N / 2 ^ j : ℕ) : ℝ) * (Real.log (N / 2 ^ j : ℕ)) ^ 2) := by
…

Mentions: OAI.Problem337.Vaughan.typeIIBlock, OAI.Problem337.VaughanBilinear.phase