OAI/Computability/FourierTransform/PackingPrograms.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Local packing tables, printed in local polynomial time.

  1. abbrev OAI.PowerSaving.RAM.chipTy line 13
  2. abbrev OAI.PowerSaving.RAM.sapTy line 14
  3. abbrev OAI.PowerSaving.RAM.blossomTy line 15
  4. abbrev OAI.PowerSaving.RAM.leafTy line 16
  5. abbrev OAI.PowerSaving.RAM.treeTy line 17
  6. def OAI.PowerSaving.RAM.chip line 19
  7. def OAI.PowerSaving.RAM.blossom line 21
  8. def OAI.PowerSaving.RAM.leavesT line 24
  9. def OAI.PowerSaving.RAM.treeT line 25
  10. lemma OAI.PowerSaving.RAM.Bench.Band.partD line 34
  11. lemma OAI.PowerSaving.RAM.Bench.Band.crownD line 38
  12. lemma OAI.PowerSaving.RAM.Bench.Band.trial line 43

    Source comment

    if exact operations
    lemma trial (hx : b.Digit n) (hy : b.Digit x) {y z : ι→ℕ} (h : b.Digit y) (g : b.Digit z) :
    b.Digit (fun i => if n i=x i then y i else z i) := by
…
  13. lemma OAI.PowerSaving.RAM.Bench.Band.thickD line 49
  14. lemma OAI.PowerSaving.RAM.Bench.Band.trimD line 53
  15. lemma OAI.PowerSaving.RAM.Bench.Band.sumsD line 57
  16. lemma OAI.PowerSaving.RAM.Bench.Band.blossomD line 72
  17. lemma OAI.PowerSaving.RAM.Bench.Band.leavesD line 83
  18. lemma OAI.PowerSaving.RAM.Bench.Engrave.tree line 89
  19. structure OAI.PowerSaving.RAM.Bench.Spring line 95

    Source comment

    use in array work
    structure Spring (b : Bench m ι) (n : ι→ℕ) (s : ι→Stroke) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  20. lemma OAI.PowerSaving.RAM.Bench.Spring.transfer line 101
  21. lemma OAI.PowerSaving.RAM.Bench.Spring.read line 105
  22. structure OAI.PowerSaving.RAM.Bench.Bough line 110
  23. lemma OAI.PowerSaving.RAM.Bench.Bough.good line 117
  24. lemma OAI.PowerSaving.RAM.Bench.Bough.transfer line 121