OAI/MathematicalPhysics/AlternatingFlow/Profiles.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AlternatingNS.Profiles.clock line 10
2. lemma OAI.AlternatingNS.Profiles.clock_smooth line 14
3. lemma OAI.AlternatingNS.Profiles.clock_mem line 18
4. lemma OAI.AlternatingNS.Profiles.clock_zero line 21
5. lemma OAI.AlternatingNS.Profiles.clock_one line 25
6. lemma OAI.AlternatingNS.Profiles.clock_monotone line 29
7. def OAI.AlternatingNS.Profiles.periodizer line 34
8. lemma OAI.AlternatingNS.Profiles.periodizer_periodic line 37
9. lemma OAI.AlternatingNS.Profiles.periodizer_int_add line 41
10. lemma OAI.AlternatingNS.Profiles.periodizer_self line 45
11. lemma OAI.AlternatingNS.Profiles.periodizer_near_zero line 52
12. lemma OAI.AlternatingNS.Profiles.periodizer_smooth line 63
13. def OAI.AlternatingNS.Profiles.decoder line 87
14. lemma OAI.AlternatingNS.Profiles.decoder_law line 92
15. lemma OAI.AlternatingNS.Profiles.decoder_smooth line 101
16. lemma OAI.AlternatingNS.Profiles.iteratedDeriv_periodic line 106
17. lemma OAI.AlternatingNS.Profiles.periodic_derivatives_bounded line 113
18. lemma OAI.AlternatingNS.Profiles.decoder_derivatives_bounded line 126
19. lemma OAI.AlternatingNS.Encoding.read_donor_configuration line 134