OAI/Probability/Contingency/RootTransport.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Root Transport.

  1. def OAI.Contingency.allSurplus line 20
  2. theorem OAI.Contingency.allBalance_nonneg line 29
  3. theorem OAI.Contingency.allSurplus_nonneg line 39
  4. theorem OAI.Contingency.raisedFull_le_surplus line 49
  5. theorem OAI.Contingency.allRaise_le_surplus line 67
  6. def OAI.Contingency.rootCoeff line 86
  7. def OAI.Contingency.minusMass line 91
  8. def OAI.Contingency.plusMass line 92
  9. def OAI.Contingency.auxiliaryMass line 93
  10. theorem OAI.Contingency.root_balance line 95
  11. theorem OAI.Contingency.root_potential line 105
  12. theorem OAI.Contingency.root_test_demand line 115
  13. theorem OAI.Contingency.root_quadratic_bound line 123
  14. instance OAI.Contingency.pairCoordsNonempty line 161
  15. theorem OAI.Contingency.softened_root_transport line 167
  16. def OAI.Contingency.joinPairHead line 235
  17. def OAI.Contingency.pairCoordsEquiv line 250
  18. theorem OAI.Contingency.pairCoordsEquiv_zero line 254
  19. def OAI.Contingency.branchValue line 257
  20. theorem OAI.Contingency.leafDisplay_base line 261
  21. theorem OAI.Contingency.leafDisplay_slot line 267
  22. def OAI.Contingency.smallCoordsTail line 282
  23. def OAI.Contingency.smallCoords line 290
  24. def OAI.Contingency.smallOccupancy line 293
  25. theorem OAI.Contingency.leaf_occupancy_special line 296
  26. theorem OAI.Contingency.leaf_occupancy_ordinary line 303
  27. def OAI.Contingency.smallPattern line 313
  28. theorem OAI.Contingency.removeOne_occupancy line 319
  29. theorem OAI.Contingency.leaf_hole_pattern line 338
  30. theorem OAI.Contingency.pairBox_const line 361
  31. def OAI.Contingency.smallVertexSet line 374
  32. theorem OAI.Contingency.mem_smallVertexSet line 378
  33. def OAI.Contingency.smallUnitEdges line 385
  34. theorem OAI.Contingency.leaf_edge_mem line 390
  35. theorem OAI.Contingency.small_soft_transport line 411
  36. theorem OAI.Contingency.allBalance_continuous line 450
  37. theorem OAI.Contingency.allSurplus_continuous line 460
  38. theorem OAI.Contingency.edgeEnergy_continuous line 473
  39. theorem OAI.Contingency.root_masses_positive line 482
  40. def OAI.Contingency.softSequence line 510
  41. theorem OAI.Contingency.softSequence_range line 512
  42. theorem OAI.Contingency.softSequence_tendsto line 518
  43. theorem OAI.Contingency.zero_root_transport line 525
  44. theorem OAI.Contingency.transport_repair_arithmetic line 572