OAI/Dynamics/EntropyCounterexample/ClockPeriodization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.ClockPeriodization.periodize line 15
2. theorem OAI.Problem340.ClockPeriodization.contDiff_tsum_of_locallyFinite line 18
3. theorem OAI.Problem340.ClockPeriodization.locallyFinite_clockIntervals line 29
4. theorem OAI.Problem340.ClockPeriodization.locallyFinite_translates line 38
5. theorem OAI.Problem340.ClockPeriodization.contDiff_periodize line 48
6. theorem OAI.Problem340.ClockPeriodization.periodize_add_period line 59
7. theorem OAI.Problem340.ClockPeriodization.periodize_eq_on_fundamental line 75
8. theorem OAI.Problem340.ClockPeriodization.translate_index_unique line 95
9. theorem OAI.Problem340.ClockPeriodization.norm_periodize_le line 113
10. theorem OAI.Problem340.ClockPeriodization.periodize_mem_Icc line 134