ConditionalCoinReindex.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Changing the order of the exact conditional finite averages

theorem OAI.JointDickman.six_sum_reorder line 10

theorem OAI.JointDickman.conditionalCoinAverage_reindex line 27

Source documentation

Rewrite the common conditional average in site-first order, with all retention sums over the common ambient prime set.

theorem conditionalCoinAverage_reindex (P A D : Finset ℕ)
    (F : Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → Finset ℕ → ℝ) :
    conditionalCoinAverage P A D F =
    ∑ R ∈ P.powerset, bernoulliSubsetMass P (remainingPrimeParameter A) R *
    ∑ I ∈ A.powerset, ∑ U ∈ P.powerset, subsetRetentionMass A I * subsetRetentionMass R U *
    (∑ Q ∈ P.powerset, bernoulliSubsetMass P (remainingPrimeParameter D) Q *
    ∑ J ∈ D.powerset, ∑ V ∈ P.powerset, subsetRetentionMass D J * subsetRetentionMass Q V *
      F R Q I J U V) := by
…

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