OAI/NumberTheory/JointDickman/Amplification/CandidateForcedProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.ForcedCandidateHit line 12
2. theorem OAI.JointDickman.forcedCandidateHit_pair_event line 17
3. theorem OAI.JointDickman.pairForcedEvent_probability line 26
4. theorem OAI.JointDickman.forcedCandidateHit_probability line 42

   Source documentation

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

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

   Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.finiteProbability, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.ForcedCandidateHit, OAI.JointDickman.auxiliaryCutoff