OAI/Dynamics/ConditionalShuffle/SweepPoint.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Thorp.Conditional.SweepHistory line 9
  2. lemma OAI.Thorp.Conditional.mean_function_snoc line 11
  3. def OAI.Thorp.Conditional.Untouched line 19
  4. lemma OAI.Thorp.Conditional.untouched_zero line 22
  5. lemma OAI.Thorp.Conditional.untouched_drop line 25
  6. lemma OAI.Thorp.Conditional.untouched_step line 38
  7. lemma OAI.Thorp.Conditional.untouched_run line 45
  8. def OAI.Thorp.Conditional.rawPoint line 53
  9. lemma OAI.Thorp.Conditional.rawPoint_support line 56
  10. def OAI.Thorp.Conditional.mate line 75
  11. lemma OAI.Thorp.Conditional.mate_zero line 78
  12. lemma OAI.Thorp.Conditional.mate_succ line 79
  13. lemma OAI.Thorp.Conditional.rawPoint_mate_zero line 82
  14. def OAI.Thorp.Conditional.partnerIndex line 95
  15. lemma OAI.Thorp.Conditional.partnerIndex_bit line 98
  16. lemma OAI.Thorp.Conditional.partnerIndex_later line 109
  17. lemma OAI.Thorp.Conditional.partnerIndex_ne line 121
  18. lemma OAI.Thorp.Conditional.partnerIndex_distinct line 128
  19. lemma OAI.Thorp.Conditional.physicalFlow_at_tag line 136
  20. lemma OAI.Thorp.Conditional.rawNext_masked line 150
  21. lemma OAI.Thorp.Conditional.rawNext_joint line 169
  22. lemma OAI.Thorp.Conditional.rawIterate_joint line 198
  23. lemma OAI.Thorp.Conditional.rawPoint_energy_identity line 248
  24. def OAI.Thorp.Conditional.encounterList line 256
  25. lemma OAI.Thorp.Conditional.encounterList_snoc_castSucc line 260
  26. lemma OAI.Thorp.Conditional.encounterList_snoc_last line 269
  27. lemma OAI.Thorp.Conditional.encounterList_injective line 278
  28. lemma OAI.Thorp.Conditional.encounterList_ne line 286
  29. lemma OAI.Thorp.Conditional.rawPoint_tag_product line 290