OAI/Computability/FourierTransform/CompilerEnvironment.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Additional composition library for local compilation -- time and all integer words polynomial in the ambient width.

  1. structure OAI.PowerSaving.RAM.Bench line 13
  2. def OAI.PowerSaving.RAM.Bench.Makes line 21
  3. structure OAI.PowerSaving.RAM.Bench.Digit line 24
  4. def OAI.PowerSaving.RAM.Bench.along line 28
  5. def OAI.PowerSaving.RAM.Bench.extend line 31
  6. def OAI.PowerSaving.RAM.Bench.scrutin line 34
  7. def OAI.PowerSaving.RAM.Bench.scan line 37
  8. def OAI.PowerSaving.RAM.Bench.climbs line 40
  9. structure OAI.PowerSaving.RAM.Bench.Feeds line 45

    Source comment

    Access another bench. b prepares q's inputs.
    structure Feeds (b : Bench m ι) (q : Bench m κ) (f : ι→κ) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  10. lemma OAI.PowerSaving.RAM.Bench.Makes.congr line 53
  11. lemma OAI.PowerSaving.RAM.Bench.Makes.along line 56
  12. lemma OAI.PowerSaving.RAM.Bench.Makes.pair line 59
  13. lemma OAI.PowerSaving.RAM.Bench.Makes.fst line 62
  14. lemma OAI.PowerSaving.RAM.Bench.Makes.snd line 64
  15. lemma OAI.PowerSaving.RAM.Bench.Makes.wc line 67
  16. lemma OAI.PowerSaving.RAM.Bench.Makes.zero line 69
  17. lemma OAI.PowerSaving.RAM.Bench.Makes.one line 70
  18. lemma OAI.PowerSaving.RAM.Bench.Makes.add line 71
  19. lemma OAI.PowerSaving.RAM.Bench.Makes.sub line 73
  20. lemma OAI.PowerSaving.RAM.Bench.Makes.neg line 75
  21. lemma OAI.PowerSaving.RAM.Bench.Makes.mul line 77
  22. lemma OAI.PowerSaving.RAM.Bench.Makes.inv line 79
  23. lemma OAI.PowerSaving.RAM.Bench.Makes.look line 81
  24. lemma OAI.PowerSaving.RAM.Bench.prepares line 86
  25. lemma OAI.PowerSaving.RAM.Bench.pull line 88
  26. lemma OAI.PowerSaving.RAM.Bench.draw line 92
  27. lemma OAI.PowerSaving.RAM.Bench.Feeds.along line 96
  28. lemma OAI.PowerSaving.RAM.Bench.toppings line 100
  29. lemma OAI.PowerSaving.RAM.Bench.trayLeft line 103
  30. lemma OAI.PowerSaving.RAM.Bench.Feeds.extend line 106
  31. lemma OAI.PowerSaving.RAM.Bench.Feeds.push line 109
  32. lemma OAI.PowerSaving.RAM.Bench.Feeds.next line 112
  33. lemma OAI.PowerSaving.RAM.Bench.enclose line 117
  34. lemma OAI.PowerSaving.RAM.Bench.Digit.wc line 125
  35. lemma OAI.PowerSaving.RAM.Bench.Digit.congr line 127
  36. lemma OAI.PowerSaving.RAM.Bench.Digit.add line 129
  37. lemma OAI.PowerSaving.RAM.Bench.Digit.sub line 132
  38. lemma OAI.PowerSaving.RAM.Bench.Digit.mul line 136
  39. lemma OAI.PowerSaving.RAM.Bench.Digit.div line 139
  40. lemma OAI.PowerSaving.RAM.Bench.Digit.mod line 143
  41. lemma OAI.PowerSaving.RAM.Bench.Digit.minimum line 147
  42. lemma OAI.PowerSaving.RAM.Bench.Digit.isLess line 152
  43. lemma OAI.PowerSaving.RAM.Bench.Feeds.scan line 162
  44. lemma OAI.PowerSaving.RAM.Bench.Feeds.climbs line 165
  45. lemma OAI.PowerSaving.RAM.Bench.slot line 171
  46. lemma OAI.PowerSaving.RAM.Bench.tab line 176
  47. lemma OAI.PowerSaving.RAM.Bench.stepi line 180
  48. lemma OAI.PowerSaving.RAM.Bench.stepsum line 185
  49. lemma OAI.PowerSaving.RAM.Bench.loop line 189
  50. lemma OAI.PowerSaving.RAM.Bench.Feeds.select line 195

    Source comment

    scan arbitrary stage by computed index
    lemma Feeds.select {n : κ→ℕ} {f : ι → During n}
    (h : b.Feeds q (fun i => (f i).i)) (g : b.Makes w (fun i => (f i).j)) :
    b.Feeds (q.scan n) f := ⟨h.inputs.pair g,h.size⟩
…

    Mentions: OAI.PowerSaving.RAM.During