OAI/NumberTheory/JointDickman/Probability/CandidateThirdSiteProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.JointDickman.OtherCandidateSite line 12
2. theorem OAI.JointDickman.finiteProbability_eq_indicator_mean line 16
3. theorem OAI.JointDickman.independent_available_probability line 22
4. theorem OAI.JointDickman.candidate_third_site_probability line 35

   Source documentation

   This estimate conditions only on the candidate's two endpoints. Each remaining endpoint is still sampled with its original independent law.

   theorem candidate_third_site_probability {B L T H M : ℕ} {τ C : ℝ}
       (hT : 0 < T) {e : BlockCandidateIndex M}
       (he : BlockCandidateAdmissible B L T H τ C e) :
       finiteProbability (siteProductMass (fun _ : OtherCandidateSite e => independentPrimeSetMass B))
         (fun S => ∃ s : OtherCandidateSite e,
           T*candidateQuotient e ≤ (candidateSiteValue e s.val).natAbs ∧
           PrimeProductAvailable (candidateSiteValue e s.val).natAbs (S s).val) ≤
         (M : ℝ)/((T : ℝ)*candidateQuotient e) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.finiteProbability, OAI.JointDickman.OtherCandidateSite, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.candidateQuotient, OAI.JointDickman.candidateSiteValue, OAI.JointDickman.PrimeProductAvailable