OAI/Combinatorics/ContingencyTables/Transport/GraphCompletionCounts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Multiplicity-one forest-coordinate sums

The finite coordinates are the actual tree cells of the row/column forest, with physical intervals [-10 d b,10 d b]. A solution of the nonroot equations contributes exactly once, with its original weight.

  1. abbrev OAI.ContingencyTables.GraphCompletionCounts.TreeCell line 21
  2. abbrev OAI.ContingencyTables.GraphCompletionCounts.TreeIndex line 24
  3. def OAI.ContingencyTables.GraphCompletionCounts.physical line 27
  4. lemma OAI.ContingencyTables.GraphCompletionCounts.physical_supported line 33
  5. lemma OAI.ContingencyTables.GraphCompletionCounts.physical_injective line 38
  6. def OAI.ContingencyTables.GraphCompletionCounts.NonrootMargins line 47
  7. def OAI.ContingencyTables.GraphCompletionCounts.solutionIndex line 52
  8. lemma OAI.ContingencyTables.GraphCompletionCounts.physical_solutionIndex line 69
  9. theorem OAI.ContingencyTables.GraphCompletionCounts.weighted_completion_sum line 86

    Source documentation

    The actual tree intervals contain the unique completion, so the finite equality-indicator sum has multiplicity exactly one.

    theorem weighted_completion_sum (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hTG : T≤cellGraph small) (hT : T.IsAcyclic)
    (r : I → ℤ) (c : J → ℤ) (d : ℕ) (b : I → J → ℕ)
    (hbox : ∀ i j, T.Adj (.inl i) (.inr j) →
      -((10*d*b i j:ℕ):ℤ)≤tableCompletion T r c i j ∧
        tableCompletion T r c i j≤(10*d*b i j:ℕ))
    (weight : (I → J → ℤ) → ℝ) :
    (∑ a : TreeIndex T d b, if NonrootMargins T r c (physical T d b a)
      then weight (physical T d b a) else 0)=weight (tableCompletion T r c) := by
…

    Mentions: OAI.ContingencyTables.GraphCompletionCounts.TreeIndex, OAI.ContingencyTables.GraphCompletionCounts.NonrootMargins, OAI.ContingencyTables.GraphCompletionCounts.physical