OAI/Computability/FourierTransform/TraversalPrograms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PowerSaving.RAM.Bench.Fen line 13
  2. abbrev OAI.PowerSaving.RAM.Bench.routes line 19
  3. abbrev OAI.PowerSaving.RAM.Bench.Forks line 22
  4. def OAI.PowerSaving.RAM.Bench.Forks.tUp line 27
  5. def OAI.PowerSaving.RAM.Bench.Forks.tOff line 28
  6. lemma OAI.PowerSaving.RAM.Bench.Fen.transfer line 36
  7. lemma OAI.PowerSaving.RAM.Bench.Fen.shrunk line 46
  8. lemma OAI.PowerSaving.RAM.Bench.Fen.midst line 49
  9. lemma OAI.PowerSaving.RAM.Bench.Fen.further line 53
  10. lemma OAI.PowerSaving.RAM.Bench.Fen.smaller line 57
  11. lemma OAI.PowerSaving.RAM.Bench.Fen.lower line 59
  12. def OAI.PowerSaving.RAM.Bench.Fen.stalk line 64

    Source documentation

    Step bench. Indexed by the 'combined' new prefix; on tray are ambient-axis bench, then decoded old prefix, offset, and previous state.

    def stalk (b : Bench m ι) (l : ι→ℕ) (r : ι→Axes) (s : Ty) (S : ι → ℕ → ℕ → T s) :
    Bench m (Forks l r) :=
…

    Mentions: OAI.PowerSaving.RAM.Bench, OAI.PowerSaving.RAM.Ty, OAI.PowerSaving.RAM.Bench.Forks

  13. lemma OAI.PowerSaving.RAM.Bench.Fen.stalkFeeds line 69
  14. lemma OAI.PowerSaving.RAM.Bench.Fen.stalkReads line 76
  15. theorem OAI.PowerSaving.RAM.Bench.Fen.visit line 87

    Source documentation

    Linear array work traversal theorem (using table of active prefixes each level).

    theorem visit (h : b.Fen l r) (S : ι → ℕ → ℕ → T s)
    (hS : b.Moves (fun _ => 0) s fun i => S i 0 0)
    (hs : (stalk b l r s S).Moves (fun _ => 0) s fun d => S d.i.i (d.i.j+1) d.j) :
    b.Moves (fun i => extent (r i) (l i)) (a s) fun i =>
      Tape.tab (extent (r i) (l i)) (S i (l i)) := by
…

    Mentions: OAI.PowerSaving.RAM.Bench.Fen.stalk, OAI.PowerSaving.RAM.Bench.Moves, OAI.PowerSaving.Tape.tab