OAI/MathematicalPhysics/Heisenberg/FiniteHistories.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Exposure.trajectory line 20
  2. lemma OAI.Heisenberg.Exposure.trajectory_zero line 24
  3. lemma OAI.Heisenberg.Exposure.trajectory_succ line 27
  4. def OAI.Heisenberg.Exposure.SameHistory line 31
  5. def OAI.Heisenberg.Exposure.Revealed line 34
  6. theorem OAI.Heisenberg.Exposure.sameHistory_iff line 37
  7. theorem OAI.Heisenberg.Exposure.not_revealed_swap line 70
  8. def OAI.Heisenberg.Exposure.productWeight line 93
  9. lemma OAI.Heisenberg.Exposure.productWeight_sum line 95
  10. lemma OAI.Heisenberg.Exposure.productWeight_nonneg line 101
  11. def OAI.Heisenberg.Exposure.merge line 104
  12. lemma OAI.Heisenberg.Exposure.merge_left line 108
  13. lemma OAI.Heisenberg.Exposure.merge_right line 113
  14. lemma OAI.Heisenberg.Exposure.productWeight_merge line 118
  15. theorem OAI.Heisenberg.Exposure.cylinder_disintegration line 126
  16. theorem OAI.Heisenberg.Exposure.cylinder_mass line 152
  17. lemma OAI.Heisenberg.LayeredExchange.wiring_update_swap line 168
  18. def OAI.Heisenberg.LayeredExchange.transport line 190
  19. lemma OAI.Heisenberg.LayeredExchange.wiring_pow line 194
  20. lemma OAI.Heisenberg.LayeredExchange.invariant_propagates line 202
  21. lemma OAI.Heisenberg.LayeredExchange.invariant_cut line 210
  22. lemma OAI.Heisenberg.Exposure.filtered_cylinder_disintegration line 222