OAI/NumberTheory/JointDickman/Amplification/ChernoffParameters.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.exists_prefix_tilt line 12
2. theorem OAI.JointDickman.tail_tilt_margin line 40
3. theorem OAI.JointDickman.regularity_prefix_chernoff_decay line 49

   Source documentation

   The two prefix Markov factors tend to zero, uniformly in the choice of any fixed finite grid after its points are instantiated.

   theorem regularity_prefix_chernoff_decay
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {τ : ℝ} (hτ : 0 < τ) :
       ∃ s : ℝ, 0 < s ∧ Real.exp s ≤ 2 ∧ Real.exp (-s) ≤ 2 ∧
         ∀ c g : ℝ, 0 < c → 0 < g → g ≤ 1 →
         Tendsto (fun B : ℕ => Real.exp (-s * (g / 2 + τ) * auxiliaryLogLength B +
           ((Real.exp s - 1) / 2) *
             (∑ p ∈ largePrimeSet (Real.exp (c * (B : ℝ) ^ g)) (auxiliaryCutoff B), 1 / (p : ℝ))))
           atTop (𝓝 0) ∧
         Tendsto (fun B : ℕ => Real.exp (s * (g / 2 - τ) * auxiliaryLogLength B +
           ((Real.exp (-s) - 1) / 2) *
             (∑ p ∈ largePrimeSet (Real.exp (c * (B : ℝ) ^ g)) (auxiliaryCutoff B), 1 / (p : ℝ))))
           atTop (𝓝 0) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.largePrimeSet, OAI.JointDickman.auxiliaryCutoff