OAI/NumberTheory/Ostmann/QuadraticCenter/FixedQuadraticFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.QuadraticFamilyIndex line 12
2. def OAI.Ostmann.quadraticFamilyParameters line 14
3. def OAI.Ostmann.fixedQuadraticCoefficient line 19
4. theorem OAI.Ostmann.mem_quadraticFamilyParameters line 26
5. theorem OAI.Ostmann.quadraticFamilyParameters_card line 34
6. theorem OAI.Ostmann.eventual_quadraticFamilyParameters_card line 41
7. theorem OAI.Ostmann.eventual_fixed_quadratic_family_covers line 63

   Source documentation

   The index family is fixed before M and its translating residue are chosen. The grid index works simultaneously for every kernel s in the full support.

   theorem eventual_fixed_quadratic_family_covers (H : ℝ) (Φ : 𝓢(ℝ, ℂ))
       (hH : 0 ≤ H) (hΦ : ∀ x : ℝ, H < x → Φ x = 0) :
       ∀ᶠ T : ℝ in atTop, ∀ (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
         (D : ∀ p : ℕ, Finset (ZMod p)) (M h₀ P : ℕ) (θ R : ℝ),
         (Q.card : ℝ) ≤ T → (∀ p ∈ Q, 1000000 ≤ p) →
         (Q.toList.prod : ℝ) ≤ Real.exp T → Odd M → h₀ < Q.toList.prod →
         0 < P → (P : ℝ) ≤ Real.exp (7 * T) →
         0 ≤ θ → θ ≤ 1 → 1 ≤ R → R ≤ Real.exp (14 * T) →
         ∃ i ∈ quadraticFamilyParameters T Q.toList.prod,
           i.2.2.1 = P ∧
           |R - quadraticGridScale (Real.exp (-200 * T)) i.2.2.2| ≤ Real.exp (-200 * T) ∧
           ∀ s : ℕ, 1 ≤ s → (s : ℝ) ≤ Real.exp (14 * T) →
   …

   Mentions: OAI.Ostmann.quadraticFamilyParameters, OAI.Ostmann.quadraticGridScale