OAI/NumberTheory/Ostmann/QuadraticCenter/FiniteQuadraticScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quadraticDensitySum_scale_sub_bound line 12
2. theorem OAI.Ostmann.positiveQuadraticSum_scale_sub_bound line 78

   Source documentation

   Both original infinite series are replaced by the same support at Rmax; the finite scale estimate then applies without a cutoff error.

   theorem positiveQuadraticSum_scale_sub_bound {q : ℕ} [NeZero q]
       (g : ZMod q → ℂ) (B : ℝ) (hg : ∀ x, ‖g x‖ ≤ B)
       (a : ZMod q) (θ : ℝ) (Φ : 𝓢(ℝ, ℂ)) (R R' Rmax v H : ℝ) (s : ℕ)
       (hR : 1 ≤ R) (hR' : 1 ≤ R') (hRR : R ≤ Rmax) (hR'R : R' ≤ Rmax)
       (hv : 0 < v) (hH : 0 ≤ H) (hs : 0 < s)
       (hΦ : ∀ x : ℝ, H < x → Φ x = 0) :
       let W := ⌊Real.sqrt (H * Rmax * q / ((s : ℝ) * v))⌋₊
   …