OAI/NumberTheory/JointDickman/Probability/TwoSiteSplitProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.sitePairSplitAverage line 10
2. theorem OAI.JointDickman.twoSiteSplit_product line 16

   Source documentation

   Given the two sites, the two fair splits are independent.

   theorem twoSiteSplit_product (P : Finset ℕ)
       (F G : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
       (∑ x : TwoSiteSplit P, twoSiteSplitMass P x *
         F x.site₁.val x.site₂.val x.first₁.val x.first₂.val *
         G x.site₁.val x.site₂.val x.second₁.val x.second₂.val) =
       ∑ S ∈ P.powerset, bernoulliSubsetMass P (fun p => 1 / (p : ℝ)) S *
       ∑ T ∈ P.powerset, bernoulliSubsetMass P (fun p => 1 / (p : ℝ)) T *
         (sitePairSplitAverage P S T (F S T) * sitePairSplitAverage P S T (G S T)) := by
   …

   Mentions: OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.twoSiteSplitMass, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.sitePairSplitAverage