OAI/NumberTheory/JointDickman/Probability/AmplificationSecondMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.amplification_second_moment_probability line 14

   Source documentation

   Both actual fair splits are good with probability O(B^{-2}). The bound uses the published upper sieve and prime reciprocal Mertens input.

   theorem amplification_second_moment_probability
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∀ (L : ℕ) (τ C : ℝ), ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ T : ℕ, 0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
         twoSiteSplitProbability (auxiliaryPrimes B) (bothAmplificationSplitsGood B L T τ C) ≤
           K / (B : ℝ)^2 := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.twoSiteSplitProbability, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bothAmplificationSplitsGood