OAI/Probability/Contingency/ConditionalTransport.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Conditional Transport.

  1. def OAI.Contingency.PaddedGraph.repairedChild line 17
  2. abbrev OAI.Contingency.PaddedGraph.FeasibleBranches line 20
  3. instance OAI.Contingency.PaddedGraph.feasibleBranchesFintype line 23
  4. def OAI.Contingency.PaddedGraph.repairedBranch line 29
  5. theorem OAI.Contingency.PaddedGraph.repairedBranch_state line 36
  6. theorem OAI.Contingency.PaddedGraph.repairedBranch_injective line 52
  7. theorem OAI.Contingency.PaddedGraph.mixedBalance_repair line 65
  8. theorem OAI.Contingency.PaddedGraph.mixedBalance_repair_max line 105
  9. theorem OAI.Contingency.PaddedGraph.context_auxiliary_bound line 116
  10. theorem OAI.Contingency.PaddedGraph.concrete_conditional_transport line 128
  11. theorem OAI.Contingency.PaddedGraph.concrete_node_variance line 145
  12. def OAI.Contingency.profileEquiv line 170
  13. theorem OAI.Contingency.profileEquiv_succ line 178
  14. def OAI.Contingency.PaddedGraph.tupleState line 184
  15. theorem OAI.Contingency.PaddedGraph.tupleState_x line 188
  16. theorem OAI.Contingency.PaddedGraph.tupleState_q line 192
  17. def OAI.Contingency.PaddedGraph.appendAssignment line 196
  18. theorem OAI.Contingency.PaddedGraph.appendAssignment_prefix line 201
  19. theorem OAI.Contingency.PaddedGraph.appendAssignment_suffix line 209
  20. theorem OAI.Contingency.PaddedGraph.appendAssignment_cons line 217
  21. def OAI.Contingency.PaddedGraph.profileState line 228
  22. theorem OAI.Contingency.PaddedGraph.profileState_succ line 233
  23. theorem OAI.Contingency.PaddedGraph.contextState_profile line 242
  24. theorem OAI.Contingency.PaddedGraph.nodeMass_profile line 278
  25. theorem OAI.Contingency.PaddedGraph.nodeMean_profile line 292
  26. def OAI.Contingency.PaddedGraph.contextEnergy line 322
  27. theorem OAI.Contingency.PaddedGraph.contextEnergy_nonneg line 328
  28. def OAI.Contingency.PaddedGraph.contextTree line 333
  29. theorem OAI.Contingency.PaddedGraph.local_constant_le line 340
  30. theorem OAI.Contingency.PaddedGraph.contextTree_childBounds line 352
  31. theorem OAI.Contingency.PaddedGraph.concrete_exposure_variance line 382
  32. def OAI.Contingency.PaddedGraph.fullOccupancy line 404
  33. def OAI.Contingency.PaddedGraph.fullPattern line 407
  34. def OAI.Contingency.PaddedGraph.fullVertices line 413
  35. theorem OAI.Contingency.PaddedGraph.mem_fullVertices line 418
  36. def OAI.Contingency.PaddedGraph.fullUnitEdges line 425
  37. def OAI.Contingency.PaddedGraph.contextDisplay line 431
  38. theorem OAI.Contingency.PaddedGraph.contextDisplay_prefix line 436
  39. theorem OAI.Contingency.PaddedGraph.contextDisplay_suffix line 442
  40. theorem OAI.Contingency.PaddedGraph.contextDisplay_joint_inj line 448
  41. theorem OAI.Contingency.PaddedGraph.contextDisplay_box line 462
  42. theorem OAI.Contingency.PaddedGraph.contextDisplay_pattern line 472
  43. theorem OAI.Contingency.PaddedGraph.contextDisplay_vertex line 499
  44. theorem OAI.Contingency.PaddedGraph.contextDisplay_removeOne line 507
  45. def OAI.Contingency.PaddedGraph.contextEdge line 518
  46. theorem OAI.Contingency.PaddedGraph.contextEdge_injective line 523
  47. theorem OAI.Contingency.PaddedGraph.contextEdge_mem line 539
  48. theorem OAI.Contingency.PaddedGraph.contextEdge_energy line 561
  49. def OAI.Contingency.PaddedGraph.fullUnitEnergy line 571
  50. theorem OAI.Contingency.PaddedGraph.fullUnitEnergy_nonneg line 575
  51. theorem OAI.Contingency.PaddedGraph.contextEnergy_sum_le line 581
  52. theorem OAI.Contingency.PaddedGraph.sum_snoc line 609
  53. theorem OAI.Contingency.PaddedGraph.contextTree_level_sum_le line 618
  54. theorem OAI.Contingency.PaddedGraph.root_level_le line 639
  55. theorem OAI.Contingency.PaddedGraph.concrete_transversal_variance line 651