OAI/MathematicalPhysics/AlternatingFlow/TimeGlue.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AlternatingNS.Profiles.pulse line 10
2. lemma OAI.AlternatingNS.Profiles.pulse_smooth line 12
3. lemma OAI.AlternatingNS.Profiles.clock_hasDeriv line 15
4. lemma OAI.AlternatingNS.Profiles.pulse_zero_left line 18
5. lemma OAI.AlternatingNS.Profiles.pulse_zero_right line 24
6. def OAI.AlternatingNS.TimeGlue.glue line 34
7. lemma OAI.AlternatingNS.TimeGlue.eq_sum line 38
8. lemma OAI.AlternatingNS.TimeGlue.locally_eq_sum line 48
9. lemma OAI.AlternatingNS.TimeGlue.smooth line 60
10. lemma OAI.AlternatingNS.TimeGlue.hasDerivAt line 75
11. lemma OAI.AlternatingNS.TimeGlue.pulse_slot line 91
12. lemma OAI.AlternatingNS.TimeGlue.clock_slot line 102