OAI/Combinatorics/ContingencyTables/Rooted/ForestPhysicalCompletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The companion's actual small/free profiles and tree intervals

Residual margins subtract the two separate small views and the fixed free values. The integral graph completion satisfies every nonroot line. The maximum-forest cut bound then supplies, rather than assumes, the physical tree interval used by the signature/count marginal.

  1. def OAI.ContingencyTables.ForestPhysicalCompletion.fixedRow line 22
  2. def OAI.ContingencyTables.ForestPhysicalCompletion.fixedColumn line 26
  3. def OAI.ContingencyTables.ForestPhysicalCompletion.rowResidual line 30
  4. def OAI.ContingencyTables.ForestPhysicalCompletion.columnResidual line 34
  5. def OAI.ContingencyTables.ForestPhysicalCompletion.solved line 38
  6. def OAI.ContingencyTables.ForestPhysicalCompletion.completed line 42
  7. lemma OAI.ContingencyTables.ForestPhysicalCompletion.row_pointwise line 46
  8. lemma OAI.ContingencyTables.ForestPhysicalCompletion.column_pointwise line 57
  9. lemma OAI.ContingencyTables.ForestPhysicalCompletion.row_completed_sum line 68
  10. lemma OAI.ContingencyTables.ForestPhysicalCompletion.column_completed_sum line 77
  11. lemma OAI.ContingencyTables.ForestPhysicalCompletion.nonroot_of_root_component line 87
  12. theorem OAI.ContingencyTables.ForestPhysicalCompletion.solved_in_intervals line 96

    Source documentation

    The completion interval holds for the literal residual margin equations, including every box-valid unbalanced small profile.

    theorem solved_in_intervals (small : I → J → Bool) (b : I → J → ℕ)
    (T : SimpleGraph (I⊕J)) (hTG : T≤cellGraph small) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph (I⊕J), F≤cellGraph small → F.IsAcyclic →
      MaximumForest.weight F (capacity b)≤MaximumForest.weight T (capacity b))
    (r : I → ℤ) (c : J → ℤ) (x q free X : I → J → ℤ) (d W : ℕ)
    (hd : 1≤d) (hcard : Fintype.card I*Fintype.card J≤d)
    (hlarge : ∀ i j, small i j=false → W≤b i j ∧ 1≤b i j)
    (hsmall : ∀ i j, small i j=true → b i j<W ∧
      (0≤x i j ∧ x i j≤b i j) ∧ (0≤q i j ∧ q i j≤b i j))
    (hfree : ∀ i j, small i j=false → ¬T.Adj (.inl i) (.inr j) →
      0≤free i j ∧ free i j≤b i j)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
…

    Mentions: OAI.ContingencyTables.MaximumForest.weight

  13. theorem OAI.ContingencyTables.ForestPhysicalCompletion.tree_indicator_sum line 178

    Source documentation

    For the literal small/free residual margins, the equality-limit sum over the prescribed tree intervals retains exactly one term, with precisely the weight of the source's solved tree values.

    theorem tree_indicator_sum (small : I → J → Bool) (b : I → J → ℕ)
    (T : SimpleGraph (I⊕J)) (hTG : T≤cellGraph small) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph (I⊕J), F≤cellGraph small → F.IsAcyclic →
      MaximumForest.weight F (capacity b)≤MaximumForest.weight T (capacity b))
    (r : I → ℤ) (c : J → ℤ) (x q free X : I → J → ℤ) (d W : ℕ)
    (hd : 1≤d) (hcard : Fintype.card I*Fintype.card J≤d)
    (hlarge : ∀ i j, small i j=false → W≤b i j ∧ 1≤b i j)
    (hsmall : ∀ i j, small i j=true → b i j<W ∧
      (0≤x i j ∧ x i j≤b i j) ∧ (0≤q i j ∧ q i j≤b i j))
    (hfree : ∀ i j, small i j=false → ¬T.Adj (.inl i) (.inr j) →
      0≤free i j ∧ free i j≤b i j)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
…

    Mentions: OAI.ContingencyTables.MaximumForest.weight