OAI/NumberTheory/Ostmann/QuadraticCenter/UniformQuadraticGrid.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_uniform_quadratic_grid line 14

   Source documentation

   The quantifier order matters: the chosen grid point depends only on the original phase and scale, and works for all moduli and kernels.

   theorem eventual_uniform_quadratic_grid (H : ℝ) (Φ : 𝓢(ℝ, ℂ))
       (hH : 0 ≤ H) (hΦ : ∀ x : ℝ, H < x → Φ x = 0) :
       ∀ᶠ T : ℝ in atTop, ∀ θ R : ℝ,
         0 ≤ θ → θ ≤ 1 → 1 ≤ R → R ≤ Real.exp (14 * T) →
         ∃ j ∈ quadraticParameterGrid (Real.exp (14 * T)) (Real.exp (-200 * T)),
           0 ≤ quadraticGridPhase (Real.exp (-200 * T)) j ∧
           quadraticGridPhase (Real.exp (-200 * T)) j ≤ 1 ∧
           1 ≤ quadraticGridScale (Real.exp (-200 * T)) j ∧
           quadraticGridScale (Real.exp (-200 * T)) j ≤ Real.exp (14 * T) ∧
           |R - quadraticGridScale (Real.exp (-200 * T)) j| ≤ Real.exp (-200 * T) ∧
           ∀ (q s : ℕ) [NeZero q] (g : ZMod q → ℂ) (B : ℝ) (a : ZMod q) (v h₀ : ℝ),
             (∀ x, ‖g x‖ ≤ B) → 1 ≤ q → (q : ℝ) ≤ Real.exp T →
   …

   Mentions: OAI.Ostmann.quadraticParameterGrid, OAI.Ostmann.quadraticGridPhase, OAI.Ostmann.quadraticGridScale