OAI/Combinatorics/ContingencyTables/Machines/CellMinimumProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Computing an attained minimum through the complementary table

Complementation changes the lower endpoint query to the upper endpoint query and preserves every cell capacity.

  1. def OAI.ContingencyTables.CellMinimumProgram.complemented line 16
  2. def OAI.ContingencyTables.CellMinimumProgram.complementedRealizer line 18
  3. lemma OAI.ContingencyTables.CellMinimumProgram.polynomial_complemented line 22
  4. def OAI.ContingencyTables.CellMinimumProgram.minimum line 26
  5. def OAI.ContingencyTables.CellMinimumProgram.minimumRealizer line 29
  6. lemma OAI.ContingencyTables.CellMinimumProgram.polynomial_minimum line 37
  7. lemma OAI.ContingencyTables.CellMinimumProgram.complemented_code line 42
  8. theorem OAI.ContingencyTables.CellMinimumProgram.minimum_correct line 52

    Source documentation

    The returned lower endpoint is attained and is no larger than the selected coordinate of any feasible bounded table.

    theorem minimum_correct {m n : ℕ} (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (i : Fin m) (j : Fin n)
    (hne : ∃ X,HasMargins X r c ∧ ∀ u v,X u v≤b u v) :
    ∃ X,HasMargins X r c ∧ (∀ u v,X u v≤b u v) ∧
      X i j=minimum (NetworkVertexCode.data r c b,(i.val,j.val)) ∧
      ∀ Y,HasMargins Y r c → (∀ u v,Y u v≤b u v) → X i j≤Y i j := by
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.CellMinimumProgram.minimum, OAI.ContingencyTables.NetworkVertexCode.data