OAI/NumberTheory/JointDickman/Probability/TwoSiteCoinLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.twoSplitSiteAverage_coin line 10
2. theorem OAI.JointDickman.twoSiteSplit_coin_law line 34

   Source documentation

   Exact disintegration by the two first coefficients, followed by the conditional remaining-set and second-coin law.

   theorem twoSiteSplit_coin_law (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 *
       ∑ D ∈ P.powerset, bernoulliSubsetMass P (fun p => (1 / 2 : ℝ) / p) D *
         conditionalCoinAverage P A D (fun R Q I J U V =>
           F A R (I ∪ U) ((A \ I) ∪ (R \ U)) D Q (J ∪ V) ((D \ J) ∪ (Q \ V))) := by
   …

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