OAI/NumberTheory/Ostmann/Construction/OriginalAmplifiedMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_physical_amplification_lower line 14
2. theorem OAI.Ostmann.eventual_original_distinct_moment line 45

   Source documentation

   Combining the physical amplification, the exact total-weight Poisson identity and the derived repeat-removal estimate.

   theorem eventual_original_distinct_moment (cψ a c C : ℝ)
       (hcψ : 0 < cψ) (ha : 0 < a) (hc : 0 < c) (hC : 1 ≤ C) :
       ∀ᶠ T : ℝ in atTop, ∀ (Q P : Finset ℕ) (_hQ : ∀ p ∈ Q, p.Prime)
         (D : ∀ p : ℕ, Finset (ZMod p)) (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ),
         0 < X → (∀ x, 0 ≤ (ψ x).re) →
         (∀ x ∈ Set.Icc (0 : ℝ) 1, cψ ≤ (ψ x).re) →
         H < X / Q.toList.prod → (∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) →
         (𝓕 ψ 0).re ≤ C →
         ∀ (S : Finset ℤ), (∀ n ∈ S, 0 ≤ (n : ℝ) ∧ (n : ℝ) ≤ X) →
         a * Real.sqrt X / T ^ 6 ≤ (S.card : ℝ) →
         (∀ p ∈ Q, (D p).card / (p : ℝ) ≤ 2 / 3) →
         (∀ n ∈ S, ∀ p ∈ Q, (n : ZMod p) ∈ D p) →
   …