OAI/NumberTheory/JointDickman/Probability/TwoSiteConditionalLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.twoSiteSplit_conditional line 13

   Source documentation

   The exact joint law, with both first remaining sets sampled from their proved conditional parameters. No independence replacement or coupling occurs.

   theorem twoSiteSplit_conditional (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (F : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ →
         Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
       (∑ x : TwoSiteSplit P, twoSiteSplitMass P x *
         F x.first₁.val (x.site₁.val \ x.first₁.val) x.second₁.val (x.site₁.val \ x.second₁.val)
           x.first₂.val (x.site₂.val \ x.first₂.val) x.second₂.val (x.site₂.val \ x.second₂.val)) =
         ∑ A ∈ P.powerset, bernoulliSubsetMass P (fun p => (1 / 2 : ℝ) / p) A *
         ∑ R ∈ P.powerset, bernoulliSubsetMass P (remainingPrimeParameter A) R *
         ∑ I ∈ A.powerset, ∑ U ∈ R.powerset, subsetRetentionMass A I * subsetRetentionMass R U *
         (∑ D ∈ P.powerset, bernoulliSubsetMass P (fun p => (1 / 2 : ℝ) / p) D *
         ∑ Q ∈ P.powerset, bernoulliSubsetMass P (remainingPrimeParameter D) Q *
         ∑ J ∈ D.powerset, ∑ V ∈ Q.powerset, subsetRetentionMass D J * subsetRetentionMass Q V *
   …

   Mentions: OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.twoSiteSplitMass, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.remainingPrimeParameter, OAI.JointDickman.subsetRetentionMass