OAI/NumberTheory/JointDickman/Probability/TwoSiteSplitSums.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Expanding the two-site configuration sum

  1. def OAI.JointDickman.twoSiteCoordinates line 11
  2. theorem OAI.JointDickman.twoSiteSplit_sum line 18
  3. theorem OAI.JointDickman.twoSiteSplit_expectation line 56

    Source documentation

    The two-site probability is the corresponding pair of one-site expectations. The function sees each coefficient and remaining subset.

    theorem twoSiteSplit_expectation (P : Finset ℕ)
    (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)) =
      twoSplitSiteAverage P (fun A R D Q => twoSplitSiteAverage P (fun C T E U => F A R D Q C T E U)) := by
…

    Mentions: OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.twoSiteSplitMass, OAI.JointDickman.twoSplitSiteAverage