OAI/NumberTheory/JointDickman/Amplification/SecondOrientedProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.secondOrientedTwoSplitTest line 12
2. theorem OAI.JointDickman.secondOrientedTwoSplitTest_conditional_bound line 22
3. theorem OAI.JointDickman.second_oriented_probability_bound line 53

   Source documentation

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

   theorem second_oriented_probability_bound {B L T i : ℕ} {τ C : ℝ} (hB : 0 < B) (hT : 0 < T) :
       twoSiteSplitProbability (auxiliaryPrimes B)
         (splitOrientationEvent (bothAmplificationSplitsGood B L T τ C) (primeTailEndpoint B i) true) ≤
       ∑ 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 D A (primeTailEndpoint B i) C (1 / (2 * 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