OAI/MathematicalPhysics/Heisenberg/HistoryMarginals.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Heisenberg.Exposure.product_marginal line 17
  2. theorem OAI.Heisenberg.Serial.mean_walkKernel line 62
  3. theorem OAI.Heisenberg.Serial.prefix_mean line 71
  4. theorem OAI.Heisenberg.Serial.prefix_endpoint_bound line 89
  5. lemma OAI.Heisenberg.Serial.follow_snoc line 123
  6. lemma OAI.Heisenberg.Serial.follow_trajectory line 131
  7. def OAI.Heisenberg.Clocks.WeakTimes line 148
  8. instance OAI.Heisenberg.Clocks.(instance at line 149) line 149
  9. def OAI.Heisenberg.Clocks.shifted line 151
  10. lemma OAI.Heisenberg.Clocks.shifted_strictMono line 154
  11. def OAI.Heisenberg.Clocks.timeSet line 162
  12. lemma OAI.Heisenberg.Clocks.timeSet_card line 165
  13. lemma OAI.Heisenberg.Clocks.timeSet_injective line 169
  14. theorem OAI.Heisenberg.Clocks.card_weakTimes_le line 182
  15. lemma OAI.Heisenberg.Clocks.weakTimes_weight_bound line 189
  16. theorem OAI.Heisenberg.Clocks.chronological_bound_limit line 199
  17. def OAI.Heisenberg.Clocks.edgeWords line 215
  18. lemma OAI.Heisenberg.Clocks.mem_edgeWords_zero line 219
  19. lemma OAI.Heisenberg.Clocks.mem_edgeWords_cons line 222
  20. lemma OAI.Heisenberg.Clocks.edgeWords_length line 228
  21. lemma OAI.Heisenberg.Clocks.card_edgeWords line 238
  22. def OAI.Heisenberg.Clocks.Follows line 252
  23. lemma OAI.Heisenberg.Clocks.follows_mem line 256