OAI/Computability/FourierTransform/WorkBounds.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.RAM.Bench.Moves line 16
  2. structure OAI.PowerSaving.RAM.Bench.Nick line 19
  3. structure OAI.PowerSaving.RAM.Bench.Instant line 24

    Source documentation

    Constant work setup of another environment.

    structure Instant (b : Bench m ι) (q : Bench m κ) (f : ι→κ) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  4. lemma OAI.PowerSaving.RAM.Bench.Moves.congr line 33
  5. lemma OAI.PowerSaving.RAM.Bench.Moves.weaken line 36
  6. lemma OAI.PowerSaving.RAM.Bench.Moves.ease line 39
  7. lemma OAI.PowerSaving.RAM.Bench.Moves.wc line 42
  8. lemma OAI.PowerSaving.RAM.Bench.Moves.pair line 44
  9. lemma OAI.PowerSaving.RAM.Bench.Moves.fst line 46
  10. lemma OAI.PowerSaving.RAM.Bench.Moves.snd line 48
  11. lemma OAI.PowerSaving.RAM.Bench.Moves.len line 51
  12. lemma OAI.PowerSaving.RAM.Bench.Moves.pick line 54
  13. lemma OAI.PowerSaving.RAM.Bench.Moves.transfer line 60
  14. lemma OAI.PowerSaving.RAM.Bench.Moves.zero line 65
  15. lemma OAI.PowerSaving.RAM.Bench.Moves.one line 66
  16. lemma OAI.PowerSaving.RAM.Bench.Moves.add line 68
  17. lemma OAI.PowerSaving.RAM.Bench.Moves.sub line 70
  18. lemma OAI.PowerSaving.RAM.Bench.Moves.mul line 72
  19. lemma OAI.PowerSaving.RAM.Bench.Moves.inv line 74
  20. lemma OAI.PowerSaving.RAM.Bench.Nick.wc line 81
  21. lemma OAI.PowerSaving.RAM.Bench.Nick.mov line 83
  22. lemma OAI.PowerSaving.RAM.Bench.Nick.congr line 85
  23. lemma OAI.PowerSaving.RAM.Bench.Nick.transfer line 88
  24. lemma OAI.PowerSaving.RAM.Bench.Nick.add line 92
  25. lemma OAI.PowerSaving.RAM.Bench.Nick.sub line 94
  26. lemma OAI.PowerSaving.RAM.Bench.Nick.mul line 96
  27. lemma OAI.PowerSaving.RAM.Bench.Nick.div line 98
  28. lemma OAI.PowerSaving.RAM.Bench.Nick.residue line 100
  29. lemma OAI.PowerSaving.RAM.Bench.Nick.digit line 102
  30. lemma OAI.PowerSaving.RAM.Bench.envNow line 106
  31. lemma OAI.PowerSaving.RAM.Bench.cherry line 107
  32. lemma OAI.PowerSaving.RAM.Bench.pie line 108
  33. lemma OAI.PowerSaving.RAM.Bench.caseM line 110
  34. lemma OAI.PowerSaving.RAM.Bench.Instant.next line 116
  35. lemma OAI.PowerSaving.RAM.Bench.Instant.extend line 119
  36. lemma OAI.PowerSaving.RAM.Bench.Instant.along line 121
  37. lemma OAI.PowerSaving.RAM.Bench.Instant.identity line 123
  38. lemma OAI.PowerSaving.RAM.Bench.Instant.scan line 125
  39. lemma OAI.PowerSaving.RAM.Bench.Instant.climbs line 127
  40. lemma OAI.PowerSaving.RAM.Bench.Instant.supply line 130
  41. lemma OAI.PowerSaving.RAM.Bench.Instant.select line 133
  42. lemma OAI.PowerSaving.RAM.Bench.chop line 138
  43. lemma OAI.PowerSaving.RAM.Bench.stride line 143
  44. lemma OAI.PowerSaving.RAM.Bench.tokenNow line 147
  45. theorem OAI.PowerSaving.RAM.Bench.arrayM line 153
  46. theorem OAI.PowerSaving.RAM.Bench.arrayNow line 160
  47. theorem OAI.PowerSaving.RAM.Bench.scatterNow line 165
  48. theorem OAI.PowerSaving.RAM.Bench.repeatM line 172
  49. theorem OAI.PowerSaving.RAM.Bench.inspectz line 179