OAI/Combinatorics/ContingencyTables/Machines/FlowPathProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Binary path bottlenecks and one integral flow-entry update

  1. def OAI.ContingencyTables.FlowPathProgram.arcPairs line 15

    Source documentation

    Adjacent path entries, using only indices below the stored path length.

    def arcPairs (xs : List ℕ) : List (ℕ×ℕ) :=
…
  2. def OAI.ContingencyTables.FlowPathProgram.pairAt line 18
  3. def OAI.ContingencyTables.FlowPathProgram.pairAtRealizer line 20
  4. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_pairAt line 24
  5. def OAI.ContingencyTables.FlowPathProgram.arcIndices line 29
  6. def OAI.ContingencyTables.FlowPathProgram.arcIndicesRealizer line 31
  7. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_arcIndices line 34
  8. def OAI.ContingencyTables.FlowPathProgram.arcPairsRealizer line 41
  9. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_arcPairs line 44
  10. lemma OAI.ContingencyTables.FlowPathProgram.arcPairs_nil line 48
  11. lemma OAI.ContingencyTables.FlowPathProgram.arcPairs_singleton line 49
  12. lemma OAI.ContingencyTables.FlowPathProgram.arcPairs_cons_cons line 51
  13. lemma OAI.ContingencyTables.FlowPathProgram.arcPairs_map line 55
  14. def OAI.ContingencyTables.FlowPathProgram.minimumScan line 67
  15. def OAI.ContingencyTables.FlowPathProgram.minimumScanRealizer line 72
  16. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_minimumScan line 77
  17. lemma OAI.ContingencyTables.FlowPathProgram.minimumScan_eq line 82
  18. lemma OAI.ContingencyTables.FlowPathProgram.minimumFold_cast line 92
  19. lemma OAI.ContingencyTables.FlowPathProgram.minimumScan_cast line 101
  20. def OAI.ContingencyTables.FlowPathProgram.residuals line 109
  21. def OAI.ContingencyTables.FlowPathProgram.residualsRealizer line 112
  22. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_residuals line 116
  23. def OAI.ContingencyTables.FlowPathProgram.bottleneck line 121
  24. def OAI.ContingencyTables.FlowPathProgram.bottleneckRealizer line 122
  25. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_bottleneck line 123
  26. lemma OAI.ContingencyTables.FlowPathProgram.bottleneck_code line 126
  27. def OAI.ContingencyTables.FlowPathProgram.pairEqual line 143
  28. def OAI.ContingencyTables.FlowPathProgram.pairEqualRealizer line 146
  29. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_pairEqual line 151
  30. def OAI.ContingencyTables.FlowPathProgram.arcCount line 161
  31. def OAI.ContingencyTables.FlowPathProgram.arcCountRealizer line 164
  32. lemma OAI.ContingencyTables.FlowPathProgram.polynomial_arcCount line 167
  33. lemma OAI.ContingencyTables.FlowPathProgram.arcCount_cast line 170