OAI/NumberTheory/JointDickman/Probability/SymmetricSplitLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.twoSplitSiteAverage line 11
2. theorem OAI.JointDickman.twoSplitSiteAverage_swap line 18

   Source documentation

   Exchangeability of the two conditionally independent fair splits.

   theorem twoSplitSiteAverage_swap (P : Finset ℕ)
       (F : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
       twoSplitSiteAverage P F = twoSplitSiteAverage P (fun A R D Q => F D Q A R) := by
   …

   Mentions: OAI.JointDickman.twoSplitSiteAverage

3. theorem OAI.JointDickman.subsetRetentionMass_sum_support line 31
4. theorem OAI.JointDickman.twoSplitSiteAverage_reindex line 44

   Source documentation

   First fix the selected coefficient, then sample its actual conditional remaining set, and finally split each of those two sets by independent fair coins.

   theorem twoSplitSiteAverage_reindex (P : Finset ℕ)
       (F : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
       twoSplitSiteAverage P F =
         ∑ A ∈ P.powerset, ∑ R ∈ P.powerset, fairSelectedRemainingMass P A R *
           ∑ I ∈ A.powerset, ∑ U ∈ R.powerset,
             subsetRetentionMass A I * subsetRetentionMass R U *
               F A R (I ∪ U) ((A \ I) ∪ (R \ U)) := by
   …

   Mentions: OAI.JointDickman.twoSplitSiteAverage, OAI.JointDickman.fairSelectedRemainingMass, OAI.JointDickman.subsetRetentionMass

5. theorem OAI.JointDickman.twoSplitSiteAverage_conditional line 83

   Source documentation

   The conditional remaining-prime parameters enter by a proved finite identity; the main two-split law is not assumed.

   theorem twoSplitSiteAverage_conditional (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (F : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
       twoSplitSiteAverage P F =
         ∑ 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 *
                 F A R (I ∪ U) ((A \ I) ∪ (R \ U)) := by
   …

   Mentions: OAI.JointDickman.twoSplitSiteAverage, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.remainingPrimeParameter, OAI.JointDickman.subsetRetentionMass