OAI/Combinatorics/ContingencyTables/Rooted/ForestLiteralCount.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Literal doubled-coordinate profiles for companion completion counts

Small views are retained separately. Every large pair is balanced, with its physical tree or free-cell value represented in the prescribed finite interval. These identities connect the concrete laminar factor family to the actual graph completion sum.

  1. def OAI.ContingencyTables.ForestLiteralCount.width line 22
  2. def OAI.ContingencyTables.ForestLiteralCount.lower line 25
  3. def OAI.ContingencyTables.ForestLiteralCount.cellCount line 28
  4. def OAI.ContingencyTables.ForestLiteralCount.profile line 32
  5. def OAI.ContingencyTables.ForestLiteralCount.largeValue line 38
  6. lemma OAI.ContingencyTables.ForestLiteralCount.cellCount_le line 43
  7. lemma OAI.ContingencyTables.ForestLiteralCount.row_profile line 56
  8. lemma OAI.ContingencyTables.ForestLiteralCount.column_profile line 72
  9. def OAI.ContingencyTables.ForestLiteralCount.actualDeviation line 101
  10. def OAI.ContingencyTables.ForestLiteralCount.actualPenalty line 108
  11. lemma OAI.ContingencyTables.ForestLiteralCount.deviation_profile line 115
  12. lemma OAI.ContingencyTables.ForestLiteralCount.penalty_profile line 139
  13. lemma OAI.ContingencyTables.ForestLiteralCount.row_pointwise line 164
  14. lemma OAI.ContingencyTables.ForestLiteralCount.column_pointwise line 178
  15. lemma OAI.ContingencyTables.ForestLiteralCount.nonroot_iff line 191
  16. theorem OAI.ContingencyTables.ForestLiteralCount.literal_tree_sum line 256

    Source documentation

    For each actual small profile and free assignment, the concrete laminar factor sum retains exactly the source's root/tree penalty at the unique integral completion, with its tree values in the prescribed completion intervals.

    theorem literal_tree_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 y free : I → J → ℕ) (X : I → J → ℤ)
    (d W : ℕ) (alpha : ℝ) (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 ∧ x i j≤b i j ∧ y i j≤b i j)
    (hf : ∀ i j, small i j=false → ¬T.Adj (.inl i) (.inr j) → free i j≤b i j)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
    (hXr : ∀ i, (∑ j, X i j)=r i) (hXc : ∀ j, (∑ i, X i j)=c j) :
    (∑ a : TreeIndex T d b, ForestPenaltyApplication.physicalWeight T b
…

    Mentions: OAI.ContingencyTables.MaximumForest.weight, OAI.ContingencyTables.ForestPenaltyApplication.physicalWeight