OAI/NumberTheory/JointDickman/Probability/SplitOrientationCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.splitOrientationEvent line 12
2. theorem OAI.JointDickman.split_orientation_cover line 18

   Source documentation

   Orientation is performed before conditioning on the first coefficients. Exchangeability accounts for the reverse direction with a factor of two.

   theorem split_orientation_cover {B N : ℕ} (hB : 1 < B)
       (hcap : 4 * (B : ℝ) ≤ (2 : ℝ)^N * Real.log (auxiliaryCutoff B))
       (E : TwoSiteSplit (auxiliaryPrimes B) → Prop) (hE : ∀ x, E x.swap ↔ E x) :
       twoSiteSplitProbability (auxiliaryPrimes B) E ≤
         twoSiteSplitProbability (auxiliaryPrimes B) (fun x => E x ∧ twoSiteNoChange x) +
           2 * ∑ i ∈ Icc 1 N,
             (twoSiteSplitProbability (auxiliaryPrimes B) (splitOrientationEvent E (primeTailEndpoint B i) false) +
              twoSiteSplitProbability (auxiliaryPrimes B) (splitOrientationEvent E (primeTailEndpoint B i) true)) := by
   …

   Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.twoSiteSplitProbability, OAI.JointDickman.twoSiteNoChange, OAI.JointDickman.splitOrientationEvent, OAI.JointDickman.primeTailEndpoint

3. theorem OAI.JointDickman.amplification_orientation_cover line 60

   Source documentation

   The orientation bound for the actual simultaneous regular amplification events.

   theorem amplification_orientation_cover {B N : ℕ} (L T : ℕ) (τ C : ℝ) (hB : 1 < B)
       (hcap : 4 * (B : ℝ) ≤ (2 : ℝ)^N * Real.log (auxiliaryCutoff B)) :
       twoSiteSplitProbability (auxiliaryPrimes B) (bothAmplificationSplitsGood B L T τ C) ≤
         twoSiteSplitProbability (auxiliaryPrimes B)
           (fun x => bothAmplificationSplitsGood B L T τ C x ∧ twoSiteNoChange x) +
         2 * ∑ i ∈ Icc 1 N,
           (twoSiteSplitProbability (auxiliaryPrimes B)
             (splitOrientationEvent (bothAmplificationSplitsGood B L T τ C) (primeTailEndpoint B i) false) +
            twoSiteSplitProbability (auxiliaryPrimes B)
             (splitOrientationEvent (bothAmplificationSplitsGood B L T τ C) (primeTailEndpoint B i) true)) :=
   …

   Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.twoSiteSplitProbability, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bothAmplificationSplitsGood, OAI.JointDickman.twoSiteNoChange, OAI.JointDickman.splitOrientationEvent, OAI.JointDickman.primeTailEndpoint