OAI/Dynamics/ConditionalShuffle/HybridCycles.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Thorp.Conditional.Hybrid.raw_append line 10
  2. lemma OAI.Thorp.Conditional.Hybrid.raw_public line 23
  3. lemma OAI.Thorp.Conditional.Hybrid.raw_private line 32
  4. def OAI.Thorp.Conditional.Hybrid.periodLength line 40
  5. lemma OAI.Thorp.Conditional.Hybrid.periodLength_eq line 42
  6. def OAI.Thorp.Conditional.Hybrid.cycleSchedule line 44
  7. def OAI.Thorp.Conditional.Hybrid.tripleHistory line 48
  8. lemma OAI.Thorp.Conditional.Hybrid.tripleHistory_apply line 52
  9. def OAI.Thorp.Conditional.Hybrid.cycleHistory line 55
  10. lemma OAI.Thorp.Conditional.Hybrid.cycleHistory_apply line 58
  11. lemma OAI.Thorp.Conditional.Hybrid.raw_cycle line 62
  12. def OAI.Thorp.Conditional.Hybrid.repeatedSchedule line 69
  13. def OAI.Thorp.Conditional.Hybrid.repeatedHistory line 72
  14. lemma OAI.Thorp.Conditional.Hybrid.repeatedHistory_apply line 75
  15. lemma OAI.Thorp.Conditional.Hybrid.raw_cycles line 79
  16. lemma OAI.Thorp.Conditional.Hybrid.repeated_energy line 102
  17. lemma OAI.Thorp.Conditional.Hybrid.repeated_point_energy line 118