OAI/NumberTheory/JointDickman/Amplification/CandidateRepeatProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.RepeatedCandidateRoot line 12
2. theorem OAI.JointDickman.repeatedCandidateRoot_pair_event line 19
3. theorem OAI.JointDickman.pairRepeatEvent_probability line 28
4. theorem OAI.JointDickman.repeatedCandidateRoot_probability line 44

   Source documentation

   Exposing endpoints first makes the union bound valid for the actual candidate family, although that family depends on the random sites.

   theorem repeatedCandidateRoot_probability {L : ℕ} (hL : 1 ≤ L) {τ : ℝ}
       (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
       ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T H M : ℕ), 0 < T →
         finiteProbability (siteProductMass (fun _ : Fin M => independentPrimeSetMass B))
           (fun S => RepeatedCandidateRoot B L T H M τ C (fun s => (S s).val)) ≤
           (M : ℝ)^3*(B : ℝ)^2/((T : ℝ)*Real.exp B) := by
   …

   Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.finiteProbability, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.RepeatedCandidateRoot