OAI/Combinatorics/ContingencyTables/Machines/TightenedInputProgram.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Executed endpoint translation and a feasible tightened baseline

The lower and upper matrices are computed by the endpoint scans. Binary subtraction updates the capacities and both margins, then the same proved flow program produces a baseline table in the translated instance.

  1. abbrev OAI.ContingencyTables.TightenedInputProgram.TranslationInput line 19
  2. abbrev OAI.ContingencyTables.TightenedInputProgram.MarginInput line 20
  3. abbrev OAI.ContingencyTables.TightenedInputProgram.CellInput line 21
  4. def OAI.ContingencyTables.TightenedInputProgram.rowValue line 23
  5. def OAI.ContingencyTables.TightenedInputProgram.rowValueRealizer line 25
  6. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_rowValue line 31
  7. def OAI.ContingencyTables.TightenedInputProgram.columnValue line 42
  8. def OAI.ContingencyTables.TightenedInputProgram.columnValueRealizer line 44
  9. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_columnValue line 51
  10. def OAI.ContingencyTables.TightenedInputProgram.position line 61
  11. def OAI.ContingencyTables.TightenedInputProgram.positionRealizer line 62
  12. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_position line 63
  13. def OAI.ContingencyTables.TightenedInputProgram.cellValue line 66
  14. def OAI.ContingencyTables.TightenedInputProgram.cellValueRealizer line 68
  15. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_cellValue line 74
  16. def OAI.ContingencyTables.TightenedInputProgram.rowIndices line 84
  17. def OAI.ContingencyTables.TightenedInputProgram.rowIndicesRealizer line 85
  18. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_rowIndices line 87
  19. def OAI.ContingencyTables.TightenedInputProgram.columnIndices line 90
  20. def OAI.ContingencyTables.TightenedInputProgram.columnIndicesRealizer line 91
  21. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_columnIndices line 93
  22. def OAI.ContingencyTables.TightenedInputProgram.capacityRow line 96
  23. def OAI.ContingencyTables.TightenedInputProgram.capacityRowRealizer line 98
  24. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_capacityRow line 100
  25. def OAI.ContingencyTables.TightenedInputProgram.translate line 105
  26. def OAI.ContingencyTables.TightenedInputProgram.translateRealizer line 109
  27. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_translate line 114
  28. lemma OAI.ContingencyTables.TightenedInputProgram.rowValue_code line 123
  29. lemma OAI.ContingencyTables.TightenedInputProgram.columnValue_code line 128
  30. lemma OAI.ContingencyTables.TightenedInputProgram.cellValue_code line 134
  31. lemma OAI.ContingencyTables.TightenedInputProgram.translate_code line 141
  32. def OAI.ContingencyTables.TightenedInputProgram.prepare line 168
  33. def OAI.ContingencyTables.TightenedInputProgram.prepareRealizer line 170
  34. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_prepare line 172
  35. def OAI.ContingencyTables.TightenedInputProgram.compute line 176
  36. def OAI.ContingencyTables.TightenedInputProgram.computeRealizer line 177
  37. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_compute line 179
  38. lemma OAI.ContingencyTables.TightenedInputProgram.compute_code line 182
  39. def OAI.ContingencyTables.TightenedInputProgram.baseline line 189
  40. def OAI.ContingencyTables.TightenedInputProgram.baselineRealizer line 190
  41. lemma OAI.ContingencyTables.TightenedInputProgram.polynomial_baseline line 192
  42. theorem OAI.ContingencyTables.TightenedInputProgram.translated_nonempty line 196

    Source documentation

    Endpoint translation preserves a concrete feasible witness.

    theorem translated_nonempty {m n : ℕ} (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) :
    ∃ Y,HasMargins Y (ComputedTableTightening.newRows r c b)
      (ComputedTableTightening.newColumns r c b) ∧
      ∀ i j,Y i j≤ComputedTableTightening.newBounds r c b i j := by
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.ComputedTableTightening.newRows, OAI.ContingencyTables.ComputedTableTightening.newColumns, OAI.ContingencyTables.ComputedTableTightening.newBounds

  43. theorem OAI.ContingencyTables.TightenedInputProgram.baseline_correct line 209

    Source documentation

    The stored baseline comes from the executed flow decoder, with all its margin and capacity obligations discharged by endpoint translation.

    theorem baseline_correct {m n : ℕ} (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) :
    ∃ Y,baseline (data r c b)=natCode Y ∧
      HasMargins Y (ComputedTableTightening.newRows r c b)
        (ComputedTableTightening.newColumns r c b) ∧
      ∀ i j,Y i j≤ComputedTableTightening.newBounds r c b i j := by
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.TightenedInputProgram.baseline, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.ComputedTableTightening.newRows, OAI.ContingencyTables.ComputedTableTightening.newColumns, OAI.ContingencyTables.ComputedTableTightening.newBounds