OAI/Combinatorics/TreeEdit/CircleFourier.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TreeEdit.TorusFourier.frequency line 10
2. lemma OAI.TreeEdit.TorusFourier.character_apply line 13
3. lemma OAI.TreeEdit.TorusFourier.frequency_eq_zero line 21
4. lemma OAI.TreeEdit.TorusFourier.frequency_add line 26
5. def OAI.TreeEdit.TorusFourier.centered line 29
6. lemma OAI.TreeEdit.TorusFourier.centered_cast line 32
7. lemma OAI.TreeEdit.TorusFourier.centered_bound line 35
8. lemma OAI.TreeEdit.TorusFourier.centered_eq_zero line 43
9. lemma OAI.TreeEdit.TorusFourier.chord_lower line 47
10. lemma OAI.TreeEdit.TorusFourier.sum_chord_detect line 72
11. lemma OAI.TreeEdit.TorusFourier.char_sum line 115
12. lemma OAI.TreeEdit.TorusFourier.natAbs_real line 121
13. lemma OAI.TreeEdit.TorusFourier.character_one line 125
14. def OAI.TreeEdit.TorusFourier.summary line 136
15. lemma OAI.TreeEdit.TorusFourier.summary_add line 139
16. lemma OAI.TreeEdit.TorusFourier.centered_summary_add line 151
17. lemma OAI.TreeEdit.TorusFourier.outside_coefficient_dvd line 180
18. lemma OAI.TreeEdit.TorusFourier.branch_integer line 193
19. lemma OAI.TreeEdit.TorusFourier.character_state line 238
20. lemma OAI.TreeEdit.TorusFourier.cycle_congruence line 245
21. lemma OAI.TreeEdit.TorusFourier.branch_summaries line 278