OAI/Computability/FourierTransform/MeasuredFit.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.Slant.far line 9
2. def OAI.PowerSaving.Slant.trestle line 11
3. def OAI.PowerSaving.Slant.barrier line 12
4. def OAI.PowerSaving.Slant.lockBay line 13
5. structure OAI.PowerSaving.Slant.Wharf line 15
6. lemma OAI.PowerSaving.Slant.wharf line 31
7. def OAI.PowerSaving.Slant.cliff line 64
8. structure OAI.PowerSaving.Slant.Slips line 68
9. lemma OAI.PowerSaving.Slant.slips line 75
10. lemma OAI.PowerSaving.Slant.sound_cliff line 88
11. lemma OAI.PowerSaving.Slant.spill_cliff line 96
12. def OAI.PowerSaving.Slant.gravel line 115
13. def OAI.PowerSaving.Slant.reef line 121
14. lemma OAI.PowerSaving.Slant.beats_gravel line 124
15. lemma OAI.PowerSaving.Slant.beats_reef line 129
16. lemma OAI.PowerSaving.Slant.sound_gravel line 133
17. lemma OAI.PowerSaving.Slant.sound_reef line 136
18. lemma OAI.PowerSaving.Slant.spill_gravel line 140
19. lemma OAI.PowerSaving.Slant.spill_reef line 146
20. def OAI.PowerSaving.Slant.speck line 153

    Source comment

    b=1 small cross

    def speck (p w : ℕ) (h g : Line) (s c j : ℕ) : Reel :=
    …

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

21. def OAI.PowerSaving.Slant.sand line 157
22. lemma OAI.PowerSaving.Slant.beats_speck line 159
23. lemma OAI.PowerSaving.Slant.beats_sand line 161
24. lemma OAI.PowerSaving.Slant.quay_jet line 164
25. lemma OAI.PowerSaving.Slant.sound_speck line 167
26. lemma OAI.PowerSaving.Slant.sound_sand line 175
27. lemma OAI.PowerSaving.Slant.spill_speck line 178
28. lemma OAI.PowerSaving.Slant.spill_sand line 196