OAI/NumberTheory/JointDickman/Amplification/OrientedProbabilityBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.firstCoefficientGood line 13
2. def OAI.JointDickman.orientedTwoSplitTest line 17
3. theorem OAI.JointDickman.orientedTwoSplitTest_conditional_bound line 27
4. theorem OAI.JointDickman.oriented_probability_bound line 57

   Source documentation

   The first-recipient orientation probability is bounded by the first coefficient average of the proved conditional operator.

   theorem oriented_probability_bound {B L T i : ℕ} {τ C : ℝ} (hB : 0 < B) :
       twoSiteSplitProbability (auxiliaryPrimes B)
         (splitOrientationEvent (bothAmplificationSplitsGood B L T τ C) (primeTailEndpoint B i) false) ≤
       ∑ A ∈ (auxiliaryPrimes B).powerset, bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1 / 2 : ℝ) / p) A *
       ∑ D ∈ (auxiliaryPrimes B).powerset, bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1 / 2 : ℝ) / p) D *
         (if firstCoefficientGood B L T τ C A D then orientedSplitMass B A D (primeTailEndpoint B i) C T else 0) := by
   …

   Mentions: OAI.JointDickman.twoSiteSplitProbability, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.splitOrientationEvent, OAI.JointDickman.bothAmplificationSplitsGood, OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.firstCoefficientGood, OAI.JointDickman.orientedSplitMass