ForestCapacity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual bipartite cell forests and their completion intervals

The graph vertices are the original row and column labels. Capacities are attached to unordered row-column edges. The deletion-component cut is constructed from the maximizing forest, so the hypotheses of the physical cut estimate follow from actual graph properties.

def OAI.ContingencyTables.ForestCapacity.cellAdj line 22
def OAI.ContingencyTables.ForestCapacity.cellGraph line 27
def OAI.ContingencyTables.ForestCapacity.pairCapacity line 32
def OAI.ContingencyTables.ForestCapacity.capacity line 37
lemma OAI.ContingencyTables.ForestCapacity.capacity_cell line 41
lemma OAI.ContingencyTables.ForestCapacity.cell_edge_injective line 45
def OAI.ContingencyTables.ForestCapacity.treeCell line 51

theorem OAI.ContingencyTables.ForestCapacity.completion_interval line 56

Source documentation

The actual maximum-forest cut gives the source's displacement and interval bounds for every solution of the selected nonroot equations.

theorem completion_interval (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 →
      weight F (capacity b)≤weight T (capacity b))
    (i₀ : I) (j₀ : J) (ht : T.Adj (.inl i₀) (.inr j₀)) (root : I⊕J)
    (hroot : T.Reachable root (.inl i₀))
    (x q z 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))
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j)
…

Mentions: OAI.ContingencyTables.ForestCapacity.cellGraph, OAI.ContingencyTables.ForestCapacity.capacity