OAI/Computability/FourierTransform/TransformProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PowerSaving.RAM.Bench.Dry.linearPow line 14
2. lemma OAI.PowerSaving.RAM.Bench.Dry.dire line 22

   Source comment

   polynomial direct branch, N^d

   lemma Dry.dire (h : b.Nick N)
       {x : ι→Line} {cl} (hx : b.Dry N (a (c cl)) fun i => Tape.tab (N i) (x i))
       {z : ι→ℂ} (hz : b.Dry N sc z) :
       b.Dry N (a (c cl)) fun i => Tape.tab (N i) (freq (N i) (z i) (x i)) := by
   …

   Mentions: OAI.PowerSaving.Line, OAI.PowerSaving.Tape.tab, OAI.PowerSaving.RAM.sc

3. def OAI.PowerSaving.RAM.Bench.fairwind line 49
4. lemma OAI.PowerSaving.RAM.Bench.fairwind_deg line 52
5. lemma OAI.PowerSaving.RAM.Bench.fairwind_left line 58
6. lemma OAI.PowerSaving.RAM.Bench.fairwind_n line 59
7. def OAI.PowerSaving.RAM.Bench.Breezy line 61
8. lemma OAI.PowerSaving.RAM.Bench.Breezy.of_moves line 66
9. lemma OAI.PowerSaving.RAM.Bench.Breezy.congr line 68
10. lemma OAI.PowerSaving.RAM.Bench.Breezy.pair line 71
11. lemma OAI.PowerSaving.RAM.Bench.Breezy.bind line 77
12. lemma OAI.PowerSaving.RAM.Bench.Breezy.flagtest line 83
13. lemma OAI.PowerSaving.RAM.Bench.Neaps.course line 97
14. lemma OAI.PowerSaving.RAM.Bench.Nick.landOrder line 122
15. lemma OAI.PowerSaving.RAM.Bench.Nick.land line 126
16. lemma OAI.PowerSaving.RAM.Bench.Nick.land' line 134