OAI/NumberTheory/JointDickman/Amplification/TiltedPrefixMeans.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.prefix_reciprocal_mean_tendsto line 12
2. theorem OAI.JointDickman.remaining_parameter_restricted_sum line 28
3. theorem OAI.JointDickman.tilted_prefix_mean_uniform line 49

   Source documentation

   A fixed exponential product removes only a bounded total parameter error. The resulting normalized error tends to zero uniformly in that product; this will be applied to the first coefficient and a fixed addition.

   theorem tilted_prefix_mean_uniform
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {κ g : ℝ}
       (hκ : 0 < κ) (hg : 0 < g) (hg1 : g ≤ 1) {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ B : ℕ in atTop, ∀ E : Finset ℕ, E ⊆ auxiliaryPrimes B →
         (∏ p ∈ E, p : ℕ) ≤ Real.exp (κ*B) →
         |(∑ p ∈ (auxiliaryPrimes B \ E) ∩ primePrefix B g (auxiliaryPrimes B),
             1/(2*(p : ℝ)-1))/auxiliaryLogLength B-g/2| ≤ ε := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primePrefix, OAI.JointDickman.auxiliaryLogLength