MaximumForest.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The companion's maximum-capacity forest

Among finite acyclic subgraphs choose one of maximum total capacity. Positive capacities make it spanning in each large-cell component. A free edge can replace every tree edge on its path; optimality therefore gives the exact path-capacity inequality used in the forest estimates.

def OAI.ContingencyTables.MaximumForest.weight line 25
lemma OAI.ContingencyTables.MaximumForest.weight_eq line 28
theorem OAI.ContingencyTables.MaximumForest.exists_maximum line 37
lemma OAI.ContingencyTables.MaximumForest.weight_sup_edge line 48

lemma OAI.ContingencyTables.MaximumForest.not_reachable_delete_path_edge line 55

Source documentation

Deleting an edge of the unique tree path separates its endpoints.

lemma not_reachable_delete_path_edge (T : SimpleGraph V) (hT : T.IsAcyclic)
    {u v : V} (p : T.Walk u v) (hp : p.IsPath) (t : Sym2 V) (ht : t∈p.edges) :
    ¬(T.deleteEdges {t}).Reachable u v := by
…

theorem OAI.ContingencyTables.MaximumForest.free_edge_le_path_edge line 69

Source documentation

This is the source's actual maximum-forest path inequality.

theorem free_edge_le_path_edge (G T : SimpleGraph V) (b : Sym2 V → ℕ)
    (hTG : T ≤ G) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph V, F ≤ G → F.IsAcyclic → weight F b ≤ weight T b)
    {u v : V} (hG : G.Adj u v) (hfree : ¬T.Adj u v)
    (p : T.Walk u v) (hp : p.IsPath) (t : Sym2 V) (ht : t∈p.edges) :
    b s(u,v) ≤ b t := by
…

Mentions: OAI.ContingencyTables.MaximumForest.weight

theorem OAI.ContingencyTables.MaximumForest.free_edge_le_separating_edge line 94

Source documentation

The same exchange argument applies directly to a separating cut; this avoids choosing a path when using the forest's component cuts.

theorem free_edge_le_separating_edge (G T : SimpleGraph V) (b : Sym2 V → ℕ)
    (hTG : T ≤ G) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph V, F ≤ G → F.IsAcyclic → weight F b ≤ weight T b)
    (t : Sym2 V) (ht : t∈T.edgeSet) {u v : V}
    (hG : G.Adj u v) (hfree : ¬T.Adj u v)
    (hcut : ¬(T.deleteEdges {t}).Reachable u v) : b s(u,v) ≤ b t := by
…

Mentions: OAI.ContingencyTables.MaximumForest.weight

def OAI.ContingencyTables.MaximumForest.side line 117
lemma OAI.ContingencyTables.MaximumForest.side_self line 120
lemma OAI.ContingencyTables.MaximumForest.side_eq_of_reachable line 124
lemma OAI.ContingencyTables.MaximumForest.not_reachable_of_side_ne line 131
lemma OAI.ContingencyTables.MaximumForest.side_eq_of_tree_edge line 137
Source documentation
Every other tree edge is internal to a deletion component.
```
lemma side_eq_of_tree_edge (T : SimpleGraph V) (t : Sym2 V) (u : V) {v w : V}
    (h : T.Adj v w) (hne : s(v,w)≠t) :
    side (T.deleteEdges {t}) u v=side (T.deleteEdges {t}) u w := by
…
```
Mentions: OAI.ContingencyTables.MaximumForest.side

lemma OAI.ContingencyTables.MaximumForest.exists_root_avoiding_side line 146

Source documentation

One deletion component contains an endpoint of the removed edge and avoids the chosen root. This also works for isolated components.

lemma exists_root_avoiding_side (T : SimpleGraph V) (hT : T.IsAcyclic)
    {u v : V} (ht : T.Adj u v) (root : V) (hroot : T.Reachable root u) :
    ∃ r : V, T.Reachable root r ∧ side (T.deleteEdges {s(u,v)}) r root=false ∧
      side (T.deleteEdges {s(u,v)}) r u≠side (T.deleteEdges {s(u,v)}) r v := by
…

Mentions: OAI.ContingencyTables.MaximumForest.side

theorem OAI.ContingencyTables.MaximumForest.crossing_free_edge_le line 167

Source documentation

Capacities of actual free edges crossing a deletion component are bounded by the capacity of its unique deleted tree edge.

theorem crossing_free_edge_le (G T : SimpleGraph V) (b : Sym2 V → ℕ)
    (hTG : T ≤ G) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph V, F ≤ G → F.IsAcyclic → weight F b ≤ weight T b)
    (t : Sym2 V) (ht : t∈T.edgeSet) (r : V) {u v : V}
    (hG : G.Adj u v) (hfree : ¬T.Adj u v)
    (hcross : side (T.deleteEdges {t}) r u≠side (T.deleteEdges {t}) r v) :
    b s(u,v) ≤ b t :=
…

Mentions: OAI.ContingencyTables.MaximumForest.weight, OAI.ContingencyTables.MaximumForest.side

theorem OAI.ContingencyTables.MaximumForest.maximum_spans line 179

Source documentation

Positive capacities force the maximizing acyclic subgraph to span every original connected component, including isolated vertices.

theorem maximum_spans (G T : SimpleGraph V) (b : Sym2 V → ℕ)
    (hTG : T ≤ G) (hT : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph V, F ≤ G → F.IsAcyclic → weight F b ≤ weight T b)
    (hb : ∀ e∈G.edgeSet, 0 < b e) : T.Reachable=G.Reachable := by
…

Mentions: OAI.ContingencyTables.MaximumForest.weight