OAI/Computability/FourierTransform/SynchronizedAlgorithm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Algorithm for the synchronized forest.

  1. lemma OAI.PowerSaving.RAM.Bench.tapeCongr line 15
  2. theorem OAI.PowerSaving.RAM.Bench.Bough.water line 23
  3. theorem OAI.PowerSaving.RAM.Bench.Bough.swell line 43
  4. structure OAI.PowerSaving.RAM.Bench.Thicket line 62

    Source documentation

    Given number of beats and axes, tape of trees (exact-width layer schedules + metadata).

    structure Thicket (b : Bench m ι) (l d : ι→ℕ) (r : ι→Axes) (u : ι → ℕ → Reel) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  5. lemma OAI.PowerSaving.RAM.Bench.Thicket.transfer line 73
  6. lemma OAI.PowerSaving.RAM.Bench.Thicket.digitize line 79
  7. theorem OAI.PowerSaving.RAM.Bench.Thicket.conduct line 91

    Source documentation

    Run synchronized transform. Input tape in mixed-radix order, output likewise.

    theorem conduct (h : b.Thicket l d r pV) (hI : b.Moves (fun _ => 0) sc fun _ => Complex.I)
    (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (extent (r i) (l i)) (x i)) :
    b.Moves (fun i => d i* (extent (r i) (l i)*hills (l i)))
      (a (c cl)) fun i => Tape.tab (extent (r i) (l i))
        (forest (r i) (l i) (pV i) (x i) (d i)) := by
…

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

  8. theorem OAI.PowerSaving.RAM.Bench.Thicket.stream line 111