OAI/MathematicalPhysics/Heisenberg/CutContractions.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Hitting.hitting_zero_column line 14
  2. def OAI.Heisenberg.Exposure.cutFactors line 25
  3. lemma OAI.Heisenberg.Exposure.cutFactors_substochastic line 33
  4. theorem OAI.Heisenberg.Exposure.cut_return_energy line 44
  5. theorem OAI.Heisenberg.Flow.exposed_prefix_leakage line 118
  6. def OAI.Heisenberg.Schedule.run line 215
  7. lemma OAI.Heisenberg.Schedule.run_zero line 217
  8. lemma OAI.Heisenberg.Schedule.run_succ line 218
  9. lemma OAI.Heisenberg.Schedule.run_val line 220
  10. lemma OAI.Heisenberg.Schedule.run_inj line 222
  11. def OAI.Heisenberg.Schedule.warm line 229
  12. def OAI.Heisenberg.Schedule.cut line 230
  13. lemma OAI.Heisenberg.Schedule.warm_pos line 233
  14. lemma OAI.Heisenberg.Schedule.warm_le line 238
  15. lemma OAI.Heisenberg.Schedule.cut_step line 240
  16. lemma OAI.Heisenberg.Schedule.cut_mod line 242
  17. def OAI.Heisenberg.Schedule.round line 256
  18. lemma OAI.Heisenberg.Schedule.round_mono line 258
  19. lemma OAI.Heisenberg.Schedule.round_lt line 262
  20. def OAI.Heisenberg.Schedule.clock line 267
  21. lemma OAI.Heisenberg.Schedule.clock_mod line 269
  22. lemma OAI.Heisenberg.Schedule.clock_run line 273
  23. lemma OAI.Heisenberg.Schedule.clock_run_phase line 284