OAI/Combinatorics/ContingencyTables/Transport/GraphIntegralCompletion.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Integral completion of actual graph incidence equations

Integral root-path flows give an explicit solution of every nonroot incidence equation. This works directly on the finite row/column graph, including disconnected components and singleton components.

  1. def OAI.ContingencyTables.GraphIntegralCompletion.edgeFlow line 21
  2. lemma OAI.ContingencyTables.GraphIntegralCompletion.edgeFlow_skew line 25
  3. lemma OAI.ContingencyTables.GraphIntegralCompletion.edgeFlow_nonadj line 30
  4. lemma OAI.ContingencyTables.GraphIntegralCompletion.edgeFlow_sum line 36
  5. def OAI.ContingencyTables.GraphIntegralCompletion.walkFlow line 41
  6. lemma OAI.ContingencyTables.GraphIntegralCompletion.walkFlow_nil line 45
  7. lemma OAI.ContingencyTables.GraphIntegralCompletion.walkFlow_cons line 49
  8. lemma OAI.ContingencyTables.GraphIntegralCompletion.walkFlow_skew line 55
  9. lemma OAI.ContingencyTables.GraphIntegralCompletion.walkFlow_supported line 62
  10. lemma OAI.ContingencyTables.GraphIntegralCompletion.walkFlow_sum line 68
  11. def OAI.ContingencyTables.GraphIntegralCompletion.componentRoot line 78
  12. lemma OAI.ContingencyTables.GraphIntegralCompletion.componentRoot_component line 82
  13. lemma OAI.ContingencyTables.GraphIntegralCompletion.componentRoot_reachable line 87
  14. lemma OAI.ContingencyTables.GraphIntegralCompletion.componentRoot_constant line 92
  15. lemma OAI.ContingencyTables.GraphIntegralCompletion.componentRoot_idempotent line 98
  16. def OAI.ContingencyTables.GraphIntegralCompletion.rootPath line 103
  17. def OAI.ContingencyTables.GraphIntegralCompletion.completionFlow line 106
  18. lemma OAI.ContingencyTables.GraphIntegralCompletion.completionFlow_skew line 109
  19. lemma OAI.ContingencyTables.GraphIntegralCompletion.completionFlow_supported line 117
  20. theorem OAI.ContingencyTables.GraphIntegralCompletion.completionFlow_divergence line 126

    Source documentation

    Every prescribed integral nonroot divergence is satisfied exactly. The chosen roots are the only vertices where a discrepancy can remain.

    theorem completionFlow_divergence (G : SimpleGraph V) (r : V → ℤ)
    (a : V) (ha : a≠componentRoot G a) : (∑ b, completionFlow G r a b)=r a := by
…

    Mentions: OAI.ContingencyTables.GraphIntegralCompletion.componentRoot, OAI.ContingencyTables.GraphIntegralCompletion.completionFlow

  21. def OAI.ContingencyTables.GraphIntegralCompletion.tableFlow line 141
  22. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableFlow_skew line 147
  23. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableFlow_row line 152
  24. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableFlow_column line 157
  25. def OAI.ContingencyTables.GraphIntegralCompletion.tableCompletion line 162
  26. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableCompletion_supported line 167
  27. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableCompletion_row line 172
  28. lemma OAI.ContingencyTables.GraphIntegralCompletion.tableCompletion_column line 186