OAI/Combinatorics/ContingencyTables/Transport/FiniteGraphCutSemantics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact edge-deletion and cut-metadata computation

  1. lemma OAI.ContingencyTables.FiniteGraphCutProgram.keep_eq_true_iff line 11
  2. lemma OAI.ContingencyTables.FiniteGraphCutProgram.deleteRow_graph line 18
  3. theorem OAI.ContingencyTables.FiniteGraphCutProgram.deleteGraph_graph line 33
  4. lemma OAI.ContingencyTables.FiniteGraphCutProgram.reachableCode_graph line 44
  5. theorem OAI.ContingencyTables.FiniteGraphCutProgram.awayCode_graph line 49
  6. theorem OAI.ContingencyTables.FiniteGraphCutProgram.cutCode_graph line 59

    Source documentation

    The executed Boolean metadata is the selected root-away cut in the actual graph, rather than an arbitrary precomputed cut oracle.

    theorem cutCode_graph (u v root a : Fin n) :
    cutCode (((graphCode G,(u.val,v.val)),root.val),a.val)=
      RootedCut.cut G u v root a := by
…

    Mentions: OAI.ContingencyTables.FiniteGraphCutProgram.cutCode, OAI.ContingencyTables.RootedCut.cut

  7. theorem OAI.ContingencyTables.FiniteGraphCutProgram.canonicalCutCode_graph line 67