OAI/Probability/Contingency/Transport.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Transport.

  1. theorem OAI.Contingency.pair_mixed_telescope line 25
  2. theorem OAI.Contingency.future_square_sequence line 35
  3. theorem OAI.Contingency.future_square_nonneg line 73
  4. theorem OAI.Contingency.PositiveSlice.nonneg line 91
  5. theorem OAI.Contingency.actual_future_square line 99
  6. theorem OAI.Contingency.actual_future_monotone line 122
  7. def OAI.Contingency.raisedMarginal line 136
  8. theorem OAI.Contingency.raisedMarginal_positive line 141
  9. def OAI.Contingency.holeFunctional line 175
  10. def OAI.Contingency.holePotential line 178
  11. theorem OAI.Contingency.removeOne_pair_old line 182
  12. theorem OAI.Contingency.removeOne_pair_first line 190
  13. theorem OAI.Contingency.removeOne_pair_second line 198
  14. theorem OAI.Contingency.holeFunctional_pair line 205
  15. theorem OAI.Contingency.holePotential_pair line 214
  16. theorem OAI.Contingency.holeFunctional_branch line 225
  17. theorem OAI.Contingency.parent_balance_sum line 239
  18. theorem OAI.Contingency.balanced_child line 248
  19. theorem OAI.Contingency.holePotential_branch line 265
  20. theorem OAI.Contingency.child_potential_increment line 276
  21. theorem OAI.Contingency.balanced_potential_bound line 301
  22. theorem OAI.Contingency.branch_demand_conservation_endpoints line 322
  23. theorem OAI.Contingency.branch_demand_conservation line 341
  24. theorem OAI.Contingency.weighted_star_bound line 374
  25. def OAI.Contingency.raisedFull line 395
  26. theorem OAI.Contingency.raisedFull_eq line 400
  27. theorem OAI.Contingency.raisedFull_positive line 414
  28. theorem OAI.Contingency.matrixForm_raisedFull line 421
  29. theorem OAI.Contingency.matrixForm_twoRemoval_add line 438
  30. theorem OAI.Contingency.matrixForm_zero line 443
  31. theorem OAI.Contingency.PositiveSlice.add line 448