OAI/NumberTheory/JointDickman/Amplification/CandidateRepeatEvent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.pairSplitChoices line 12
2. def OAI.JointDickman.CandidateRepeatWitness line 16
3. def OAI.JointDickman.PairRepeatEvent line 22
4. theorem OAI.JointDickman.coincident_candidates_pair_event line 30

   Source documentation

   This event is a consequence of actual candidate membership and equal rational roots, not a premise about independence.

   theorem coincident_candidates_pair_event {B L T H M : ℕ} {τ C : ℝ}
       {S : Fin M → Finset ℕ} {e f : BlockCandidateIndex M}
       (he : e ∈ blockCandidates B L T H M τ C S)
       (hf : f ∈ blockCandidates B L T H M τ C S)
       (hp : e.1 ≠ f.1) (hr : blockCandidateRoot e = blockCandidateRoot f) :
       PairRepeatEvent B L T H M τ C e.1.1 e.1.2 S := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.blockCandidateRoot, OAI.JointDickman.PairRepeatEvent

5. theorem OAI.JointDickman.repeatWitness_merge_iff line 45
6. theorem OAI.JointDickman.repeatWitness_remaining_probability line 65

   Source documentation

   Exposing the two endpoints leaves the third-site witness bounded by M/(T c), even though its prescribed coefficients depend on those endpoints.

   theorem repeatWitness_remaining_probability {B L T H M : ℕ} {τ C : ℝ}
       (hT : 0 < T) {e : BlockCandidateIndex M}
       (he : BlockCandidateAdmissible B L T H τ C e)
       (a : ({e.1.1,e.1.2} : Finset (Fin M)) → (auxiliaryPrimes B).powerset) :
       finiteProbability
         (siteProductMass (fun _ : {s : Fin M // s ∉ ({e.1.1,e.1.2} : Finset (Fin M))} =>
           independentPrimeSetMass B))
         (fun b => CandidateRepeatWitness T e
           (fun i => (mergeSitePartition {e.1.1,e.1.2} a b i).val)) ≤
         (M : ℝ)/((T : ℝ)*Real.exp B) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.finiteProbability, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.CandidateRepeatWitness, OAI.JointDickman.mergeSitePartition