OAI/Dynamics/EntropyCounterexample/ClockProfiles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.periodicGain line 10
2. lemma OAI.Problem340.gainProfile_nonzero_mem line 13
3. lemma OAI.Problem340.periodicGain_contDiff line 18
4. lemma OAI.Problem340.periodicGain_periodic line 26
5. lemma OAI.Problem340.periodicGain_mem_Icc line 31
6. lemma OAI.Problem340.periodicGain_eq line 40
7. lemma OAI.Problem340.periodicGain_eq_gain line 47
8. lemma OAI.Problem340.periodicGain_eq_zero line 52
9. theorem OAI.Problem340.exists_periodic_gain line 57
10. lemma OAI.Problem340.gainProfile_liftIco_coe_eq_periodicGain line 70
11. lemma OAI.Problem340.gainProfile_liftIco_coe_contDiff line 87