OAI/Combinatorics/ContingencyTables/Machines/CellMaximumProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Computing an attained cell maximum by binary feasibility search

A finite maximum is used only to prove the result of the executed binary search. The program never enumerates feasible tables.

  1. def OAI.ContingencyTables.CellMaximumProgram.bound line 17
  2. def OAI.ContingencyTables.CellMaximumProgram.boundRealizer line 19
  3. lemma OAI.ContingencyTables.CellMaximumProgram.polynomial_bound line 22
  4. def OAI.ContingencyTables.CellMaximumProgram.maximum line 27
  5. def OAI.ContingencyTables.CellMaximumProgram.maximumRealizer line 29
  6. lemma OAI.ContingencyTables.CellMaximumProgram.polynomial_maximum line 34
  7. lemma OAI.ContingencyTables.CellMaximumProgram.bound_code line 38
  8. theorem OAI.ContingencyTables.CellMaximumProgram.maximum_correct line 45

    Source documentation

    For every feasible instance the computed value is attained, and it bounds the same coordinate of every other feasible table.

    theorem maximum_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=maximum (NetworkVertexCode.data r c b,(i.val,j.val)) ∧
      ∀ Y,HasMargins Y r c → (∀ u v,Y u v≤b u v) → Y i j≤X i j := by
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.CellMaximumProgram.maximum, OAI.ContingencyTables.NetworkVertexCode.data