OAI/Combinatorics/KServer/CausalRounding.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Pushing the actual finite rounded law onto one fixed finite state space.

  1. def OAI.KServer.TreeRounding.Law.mass line 15
  2. lemma OAI.KServer.TreeRounding.Law.mass_nonneg line 17
  3. lemma OAI.KServer.TreeRounding.Law.mass_sum line 20
  4. lemma OAI.KServer.TreeRounding.Law.mass_average line 24
  5. lemma OAI.KServer.TreeRounding.Law.mass_support line 33
  6. def OAI.KServer.TreeRounding.Law.distribution line 40
  7. lemma OAI.KServer.TreeRounding.Law.mass_left line 44
  8. lemma OAI.KServer.TreeRounding.Law.mass_right line 56
  9. structure OAI.KServer.CausalCouplings.Family line 81
  10. def OAI.KServer.CausalCouplings.kernel line 91
  11. lemma OAI.KServer.CausalCouplings.kernel_nonneg line 94
  12. lemma OAI.KServer.CausalCouplings.kernel_sum line 100
  13. lemma OAI.KServer.CausalCouplings.disintegration line 106
  14. lemma OAI.KServer.CausalCouplings.push line 117
  15. def OAI.KServer.CausalCouplings.machine line 121
  16. lemma OAI.KServer.CausalCouplings.machine_transition line 131
  17. def OAI.KServer.CausalCouplings.cost line 137
  18. def OAI.KServer.CausalCouplings.transport line 141
  19. def OAI.KServer.CausalCouplings.pathCost line 143
  20. lemma OAI.KServer.CausalCouplings.virtual_eq line 147
  21. lemma OAI.KServer.CausalCouplings.mean_path line 159
  22. lemma OAI.KServer.CausalCouplings.exists_policy line 171
  23. structure OAI.KServer.TreeRounding.CountState line 199
  24. lemma OAI.KServer.TreeRounding.count_initial line 206
  25. def OAI.KServer.TreeRounding.initialCount line 211
  26. lemma OAI.KServer.TreeRounding.count_step_exists line 214
  27. def OAI.KServer.TreeRounding.countStepLaw line 226
  28. theorem OAI.KServer.TreeRounding.countStep_spec line 229
  29. def OAI.KServer.TreeRounding.nextCount line 240
  30. def OAI.KServer.TreeRounding.countState line 246
  31. lemma OAI.KServer.TreeRounding.countState_nil line 250
  32. lemma OAI.KServer.TreeRounding.countState_snoc line 252
  33. def OAI.KServer.TreeRounding.pairLaw line 257
  34. def OAI.KServer.TreeRounding.countFamily line 260
  35. lemma OAI.KServer.TreeRounding.marginal_valid line 294
  36. lemma OAI.KServer.TreeRounding.pair_old_valid line 300
  37. lemma OAI.KServer.TreeRounding.pair_new_valid line 303
  38. lemma OAI.KServer.TreeRounding.joint_average line 307
  39. lemma OAI.KServer.TreeRounding.expected_bound line 313
  40. def OAI.KServer.CausalCouplings.mixture line 370
  41. lemma OAI.KServer.CausalCouplings.mixture_transport line 391
  42. lemma OAI.KServer.CausalCouplings.mixture_path line 407
  43. def OAI.KServer.CausalCouplings.safeConfig line 416
  44. lemma OAI.KServer.CausalCouplings.safeConfig_serves line 420
  45. lemma OAI.KServer.CausalCouplings.safeConfig_eq_nil line 431
  46. lemma OAI.KServer.CausalCouplings.safeConfig_eq line 435
  47. lemma OAI.KServer.CausalCouplings.path_ofFn line 452
  48. abbrev OAI.KServer.JointRounded.T line 483
  49. abbrev OAI.KServer.JointRounded.State line 484
  50. def OAI.KServer.JointRounded.family line 486
  51. def OAI.KServer.JointRounded.rawConfig line 491
  52. def OAI.KServer.JointRounded.config line 494
  53. lemma OAI.KServer.JointRounded.config_serves line 497
  54. lemma OAI.KServer.JointRounded.q_take line 500
  55. lemma OAI.KServer.JointRounded.a_take line 504
  56. lemma OAI.KServer.JointRounded.take_succ line 510
  57. lemma OAI.KServer.JointRounded.raw_take line 516
  58. lemma OAI.KServer.JointRounded.config_take line 522
  59. lemma OAI.KServer.JointRounded.step_bound line 541
  60. lemma OAI.KServer.JointPolicy.tape_nonempty line 592
  61. abbrev OAI.KServer.JointPolicy.MixState line 598
  62. def OAI.KServer.JointPolicy.mixed line 600
  63. def OAI.KServer.JointPolicy.rendered line 603
  64. lemma OAI.KServer.JointPolicy.rendered_serves line 606
  65. lemma OAI.KServer.JointPolicy.mean_path line 610
  66. lemma OAI.KServer.JointPolicy.path_bound line 632
  67. lemma OAI.KServer.JointPolicy.exists_policy line 647