OAI/NumberTheory/Ostmann/QuadraticCenter/HighWeightDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_high_weight_residue_mass line 17

   Source documentation

   The high-weight estimate at the manuscript's moment and kernel scales. The set consists of actual squarefree integers in a dyadic residue class; neither a reciprocal-mass estimate nor a half-kernel count is assumed.

   theorem eventual_high_weight_residue_mass (C : ℝ) :
       ∀ᶠ T : ℝ in atTop, ∀ (N L a : ℕ) (S : Finset ℕ) (u : ℝ),
         0 < L → 2 * L ^ 2 ≤ N → (2 * N : ℝ) ≤ Real.exp (C * T) →
         (∀ s ∈ S, Squarefree s) →
         (∀ s ∈ S, s ∈ Finset.Ioc N (2 * N)) →
         (∀ s ∈ S, Nat.ModEq L s a) → (∀ s ∈ S, L.Coprime s) →
         2 ≤ u → u ≤ 4 * T ^ (1 / 1000000 : ℝ) →
         (∀ s ∈ S, Real.exp (T ^ (9999999 / 10000000 : ℝ) / 200) < u ^ s.primeFactors.card) →
         (∑ s ∈ S, u ^ s.primeFactors.card) ≤
           ((N : ℝ) / L) * Real.exp (-10 * T ^ (9999999 / 10000000 : ℝ)) := by
   …