VaughanOptimized.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.Vaughan.approximationEnvelope line 11
Source documentation
The standard three-term envelope for a reduced rational approximation.
```
def approximationEnvelope (X q : ℝ) : ℝ :=
…
```
lemma OAI.Problem337.Vaughan.approximationEnvelope_nonneg line 14
lemma OAI.Problem337.Vaughan.dyadic_log_le_three_scale line 19

theorem OAI.Problem337.Vaughan.optimized_typeIIBlock_bound line 31

Source documentation

Balanced cutoffs turn each actual Type II block into the standard envelope.

theorem optimized_typeIIBlock_bound
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N j : ℕ) (hqN : q ≤ N)
    (hpow : 2 ≤ (N : ℝ) ^ (2 / 5 : ℝ)) :
    ‖typeIIBlock N (optimizedCutoff N) (optimizedCutoff N) j
      (fun k => VaughanBilinear.phase (θ * k))‖ ≤
      18 * (typeIILogScale N) ^ 3 * approximationEnvelope N q := by
…

Mentions: OAI.Problem337.Vaughan.typeIIBlock, OAI.Problem337.Vaughan.optimizedCutoff, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.typeIILogScale, OAI.Problem337.Vaughan.approximationEnvelope

theorem OAI.Problem337.Vaughan.optimized_typeII_bound line 60
Source documentation
Summing the genuine dyadic blocks costs one further logarithm, not a power of the summation length. All cancellation hypotheses are discharged.
```
theorem optimized_typeII_bound
    (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (N : ℕ) (hqN : q ≤ N)
    (hpow : 2 ≤ (N : ℝ) ^ (2 / 5 : ℝ)) :
    ‖weightedSum (Finset.Ioc 0 N) (fun k => VaughanBilinear.phase (θ * k))
      (typeIICoefficient (optimizedCutoff N) * longPart (optimizedCutoff N) Λ)‖ ≤
      54 * (typeIILogScale N) ^ 4 * approximationEnvelope N q := by
…
```
Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.optimizedCutoff, OAI.Problem337.Vaughan.longPart, OAI.Problem337.Vaughan.typeIILogScale, OAI.Problem337.Vaughan.approximationEnvelope