OAI/NumberTheory/JointDickman/Amplification/IndependentForcedHits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.independent_subset_intersects_bound line 13
2. def OAI.JointDickman.candidateForcedPrimes line 42
3. theorem OAI.JointDickman.candidate_forced_hit_bound line 48

   Source documentation

   Once a candidate's endpoints have been exposed, an independent third site meets one of its forced primes with probability O(B/P0).

   theorem candidate_forced_hit_bound {B L T H M : ℕ} {τ C : ℝ}
       (hB : 2 ≤ B) (hT : (T : ℝ) ≤ Real.exp B) (hM : (M : ℝ) ≤ Real.exp B)
       (hP : 0 < auxiliaryCutoff B) {e : BlockCandidateIndex M}
       (he : BlockCandidateAdmissible B L T H τ C e) (s : Fin M) :
       finiteExpectation (independentPrimeSetMass B) (fun R =>
         if ∃ p ∈ candidateForcedPrimes B e s, p ∈ R.val then 1 else 0) ≤
           (5*(B : ℝ))/(Real.log 2*auxiliaryCutoff B) := by
   …

   Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.candidateForcedPrimes