OAI/Computability/FourierTransform/BinaryFFT.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.Slant.initial line 9
2. def OAI.PowerSaving.Slant.ending line 10
3. lemma OAI.PowerSaving.Slant.half_fits line 12
4. lemma OAI.PowerSaving.Slant.half_sep line 14
5. def OAI.PowerSaving.Slant.deal line 17
6. def OAI.PowerSaving.Slant.foldPair line 19
7. def OAI.PowerSaving.Slant.duo line 23
8. def OAI.PowerSaving.Slant.pulse line 26
9. lemma OAI.PowerSaving.Slant.sound_foldPair line 30
10. lemma OAI.PowerSaving.Slant.sound_duo line 34
11. lemma OAI.PowerSaving.Slant.sound_pulse line 41
12. lemma OAI.PowerSaving.Slant.beats_duo line 48
13. lemma OAI.PowerSaving.Slant.beats_pulse line 52
14. def OAI.PowerSaving.Slant.Flows line 58
15. lemma OAI.PowerSaving.Slant.go_foldPair line 61
16. lemma OAI.PowerSaving.Slant.flows_duo line 70
17. lemma OAI.PowerSaving.Slant.flows_pulse line 98
18. def OAI.PowerSaving.Slant.backPulse line 110
19. lemma OAI.PowerSaving.Slant.sound_back line 113
20. lemma OAI.PowerSaving.Slant.beats_back line 116
21. lemma OAI.PowerSaving.Slant.flows_back line 120
22. structure OAI.PowerSaving.Slant.Retrace line 126

    Source documentation

    mount at offset and effect only on zone.

    structure Retrace (r : Reel) (u : Zone) (f : Line→Line) : Prop where
    …

    Mentions: OAI.PowerSaving.Slant.Reel, OAI.PowerSaving.Slant.Zone, OAI.PowerSaving.Line

23. lemma OAI.PowerSaving.Slant.atBase_retrace line 130
24. lemma OAI.PowerSaving.Slant.retrace_preserve line 141