OAI/NumberTheory/JointDickman/Amplification/ManuscriptAdditionProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.additionPrimes line 12
2. theorem OAI.JointDickman.additionPrimes_prime line 15
3. theorem OAI.JointDickman.additionPrimes_rough line 19
4. theorem OAI.JointDickman.additionPrimes_contains_cutoff line 24
5. theorem OAI.JointDickman.manuscript_addition_interval_bound line 37
6. def OAI.JointDickman.additionLogIntervalMass line 56
7. theorem OAI.JointDickman.additionLogIntervalMass_le_integer_interval line 62
8. theorem OAI.JointDickman.manuscript_addition_small_ball line 96

   Source documentation

   Manuscript Lemma amp-small-ball, for the actual independent Bernoulli(1/(4p)) addition product and every translated interval.

   theorem manuscript_addition_small_ball
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {H : ℝ} (hH : 0 ≤ H) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ Y v : ℝ,
         Real.log (auxiliaryCutoff B) ≤ Y → Y ≤ 8 * B →
         additionLogIntervalMass B Y v H ≤ K / Y := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.additionLogIntervalMass