OAI/Computability/FourierTransform/UniformBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PowerSaving.RAM.Bench.fairwind_small line 15
2. abbrev OAI.PowerSaving.RAM.Bench.Sizes line 36

   Source comment

   package extracted charges

   abbrev Sizes := {n : ℕ // 0<n}

3. abbrev OAI.PowerSaving.RAM.Bench.entry line 37
4. structure OAI.PowerSaving.RAM.Bench.Ration line 39
5. def OAI.PowerSaving.RAM.Bench.calorie line 43
6. lemma OAI.PowerSaving.RAM.Bench.Breezy.ration line 45
7. def OAI.PowerSaving.RAM.Bench.lunch line 52
8. lemma OAI.PowerSaving.RAM.Bench.storehouse line 55
9. def OAI.PowerSaving.RAM.Bench.onlyLength line 81

   Source comment

   order environments

   def onlyLength : Bench false Sizes := ⟨entry,w,entry⟩

   Mentions: OAI.PowerSaving.RAM.Bench, OAI.PowerSaving.RAM.Bench.Sizes, OAI.PowerSaving.RAM.Bench.entry

10. lemma OAI.PowerSaving.RAM.Bench.onlyLength_num line 82
11. lemma OAI.PowerSaving.RAM.Bench.orders1 line 84
12. lemma OAI.PowerSaving.RAM.Bench.orders2 line 88
13. def OAI.PowerSaving.RAM.Bench.towerOne line 95
14. lemma OAI.PowerSaving.RAM.Bench.executeOne line 99
15. def OAI.PowerSaving.RAM.Bench.towerBoth line 117
16. lemma OAI.PowerSaving.RAM.Bench.executeBoth line 122
17. theorem OAI.PowerSaving.RAM.Bench.flagshipOne line 142
18. theorem OAI.PowerSaving.RAM.Bench.flagshipBoth line 160