OAI/Combinatorics/ContingencyTables/Rooted/ComputedLargeForest.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The executed maximum-capacity forest on the original cell vertices

The program uses the concrete row-then-column natural indexing. The returned adjacency list is decoded and transported back to the original bipartite vertex type. Its catalog and optimality obligations follow from the stored capacities, rather than supplied correctness predicates.

  1. abbrev OAI.ContingencyTables.ComputedLargeForest.vertexEquiv line 22
  2. def OAI.ContingencyTables.ComputedLargeForest.small line 24
  3. def OAI.ContingencyTables.ComputedLargeForest.graph line 27
  4. def OAI.ContingencyTables.ComputedLargeForest.capacities line 30
  5. lemma OAI.ContingencyTables.ComputedLargeForest.graph_edge line 33
  6. lemma OAI.ContingencyTables.ComputedLargeForest.capacities_cell line 41
  7. lemma OAI.ContingencyTables.ComputedLargeForest.catalog_correct line 45
  8. lemma OAI.ContingencyTables.ComputedLargeForest.capacity_positive line 88
  9. lemma OAI.ContingencyTables.ComputedLargeForest.empty_code line 118
  10. def OAI.ContingencyTables.ComputedLargeForest.computed line 128

    Source documentation

    The output list itself determines the forest.

    noncomputable def computed (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ) (W : ℕ) :
    SimpleGraph (Fin m⊕Fin n) :=
…
  11. lemma OAI.ContingencyTables.ComputedLargeForest.weight_transport line 132
  12. theorem OAI.ContingencyTables.ComputedLargeForest.computed_spec line 145

    Source documentation

    The executed list program gives a maximum-capacity forest on the actual row and column vertices.

    theorem computed_spec (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (W : ℕ) (hW : 1≤W) :
    computed r c b W≤cellGraph (small b W) ∧ (computed r c b W).IsAcyclic ∧
    ∀ F : SimpleGraph (Fin m⊕Fin n),F≤cellGraph (small b W) → F.IsAcyclic →
      weight F (capacity b)≤weight (computed r c b W) (capacity b) := by
…

    Mentions: OAI.ContingencyTables.ComputedLargeForest.computed, OAI.ContingencyTables.ComputedLargeForest.small