OAI/NumberTheory/Ostmann/ZeroDensity/PrincipalFourierGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.smallKernelParameters_principal line 14
2. theorem OAI.Ostmann.squarefreeKernelSupport_card_le line 20
3. theorem OAI.Ostmann.smallSquarefreeKernels_spec line 26
4. theorem OAI.Ostmann.largeSquarefreeKernels_spec line 34
5. theorem OAI.Ostmann.filteredKernel_card_le line 44
6. theorem OAI.Ostmann.eventual_principalFourier_grid line 50

   Source documentation

   One common index approximates both principal pieces. Its outer parameter is one, and its scale remains in the small-kernel range.

   theorem eventual_principalFourier_grid (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 N h₀ : ℕ) (θ R : ℝ),
         (Q.card : ℝ) ≤ T → (∀ p ∈ Q, 1000000 ≤ p) →
         (Q.toList.prod : ℝ) ≤ Real.exp T → Odd M → h₀ < Q.toList.prod →
         0 ≤ θ → θ ≤ 1 → 1 ≤ R → R ≤ Real.exp (14 * T) →
         (Q.toList.prod : ℝ) ^ 6 + Real.exp (-200 * T) ≤ R →
         (N : ℝ) ≤ Real.exp (14 * T) →
         ∃ i ∈ smallKernelParameters T Q.toList.prod,
           ‖principalSmallFourier Q hQ D M N h₀ θ R Φ -
             quadraticArrayStatistic (smallSquarefreeKernels Q.toList.prod N) M
   …

   Mentions: OAI.Ostmann.smallKernelParameters, OAI.Ostmann.principalSmallFourier, OAI.Ostmann.quadraticArrayStatistic, OAI.Ostmann.smallSquarefreeKernels