OAI/Probability/Contingency/RecursiveTransport.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Recursive Transport.

  1. def OAI.Contingency.PairCoords line 21
  2. instance OAI.Contingency.pairCoordsFintype line 25
  3. instance OAI.Contingency.pairCoordsDecidableEq line 29
  4. def OAI.Contingency.pairBox line 34
  5. def OAI.Contingency.allBalance line 39
  6. def OAI.Contingency.allRaise line 46
  7. theorem OAI.Contingency.allBalance_closure line 55
  8. theorem OAI.Contingency.allRaise_positive line 70
  9. def OAI.Contingency.Branches line 96
  10. instance OAI.Contingency.branchesFintype line 100
  11. def OAI.Contingency.leafDisplay line 104
  12. def OAI.Contingency.leafCoefficient line 109
  13. def OAI.Contingency.BoxSupported line 122
  14. theorem OAI.Contingency.PositiveSlice.boxSupported line 126
  15. theorem OAI.Contingency.allBalance_boxSupported line 131
  16. theorem OAI.Contingency.leaf_demand_conservation line 149
  17. theorem OAI.Contingency.allRaise_future_monotone line 196
  18. theorem OAI.Contingency.leaf_potential_bound line 216
  19. theorem OAI.Contingency.leaf_balanced line 268
  20. def OAI.Contingency.leafStarEnergy line 295
  21. theorem OAI.Contingency.recursive_star_transport line 303
  22. theorem OAI.Contingency.removeOne_injective line 361
  23. theorem OAI.Contingency.removeOne_sup line 367
  24. theorem OAI.Contingency.holeEdge_display line 380
  25. theorem OAI.Contingency.leafDisplay_inj line 389
  26. def OAI.Contingency.edgeEnergy line 406
  27. theorem OAI.Contingency.edgeEnergy_mk line 413
  28. theorem OAI.Contingency.edgeEnergy_nonneg line 416
  29. def OAI.Contingency.starEdge line 424
  30. def OAI.Contingency.starIndices line 429
  31. def OAI.Contingency.leafStarEdges line 434
  32. theorem OAI.Contingency.starEdge_injOn line 441
  33. theorem OAI.Contingency.leafStarEnergy_eq_edges line 461
  34. theorem OAI.Contingency.leafStarEnergy_le_graph line 481