SplitReindex.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Reindexing a site and its first split by the two disjoint parts

theorem OAI.JointDickman.first_split_reindex line 14
Source documentation
The site-first and coefficient-first descriptions of one fair split have identical finite expectations, with no asymptotic error.
```
theorem first_split_reindex (P A : Finset ℕ) (hA : A ⊆ P) (F : Finset ℕ → ℝ) :
    (∑ S ∈ P.powerset, bernoulliSubsetMass P (fun p => 1 / (p : ℝ)) S *
      subsetRetentionMass S A * F (S \ A)) =
      ∑ R ∈ P.powerset, fairSelectedRemainingMass P A R * F R := by
…
```
Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.subsetRetentionMass, OAI.JointDickman.fairSelectedRemainingMass

theorem OAI.JointDickman.second_split_reindex line 62

Source documentation

Given the first parts, the second fair split is exactly the independent retention of coefficient primes and addition of remaining primes.

theorem second_split_reindex (A R : Finset ℕ) (hd : Disjoint A R)
    (F : Finset ℕ → Finset ℕ → ℝ) :
    (∑ C ∈ (A ∪ R).powerset, subsetRetentionMass (A ∪ R) C * F C ((A ∪ R) \ C)) =
      ∑ I ∈ A.powerset, ∑ U ∈ R.powerset,
        subsetRetentionMass A I * subsetRetentionMass R U *
          F (I ∪ U) ((A \ I) ∪ (R \ U)) := by
…

Mentions: OAI.JointDickman.subsetRetentionMass