OAI/NumberTheory/JointDickman/Amplification/RemainderNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.remainderTiltNormalizer_nonneg line 12
2. theorem OAI.JointDickman.remainderTiltNormalizer_bounded line 23

   Source documentation

   Removing the finitely many forced coefficient primes changes the normalization by a bounded factor, uniformly in the coefficient.

   theorem remainderTiltNormalizer_bounded
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ A ⊆ auxiliaryPrimes B, (∏ p ∈ A, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
           remainderTiltNormalizer B A ≤ K := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.remainderTiltNormalizer