OAI/NumberTheory/JointDickman/Amplification/CandidateRepeatConditional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.pairRepeatEvent_conditional_bound line 14

   Source documentation

   There are at most B squared local candidates after both endpoints are exposed, so their third-site probabilities remain negligible.

   theorem pairRepeatEvent_conditional_bound {L : ℕ} (hL : 1 ≤ L) {τ : ℝ}
       (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
       ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T H M : ℕ), 0 < T → ∀ (i k : Fin M),
         ∀ a : ({i,k} : Finset (Fin M)) → (auxiliaryPrimes B).powerset,
         finiteProbability (siteProductMass
           (fun _ : {s : Fin M // s ∉ ({i,k} : Finset (Fin M))} => independentPrimeSetMass B))
           (fun b => PairRepeatEvent B L T H M τ C i k
             (fun s => (mergeSitePartition {i,k} a b s).val)) ≤
           (B : ℝ)^2*(M : ℝ)/((T : ℝ)*Real.exp B) := by
   …

   Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.finiteProbability, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.PairRepeatEvent, OAI.JointDickman.mergeSitePartition