OAI/Computability/FourierTransform/SectorPrograms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compile synchronized gather slot, and synchronized sector packing metadata.

  1. structure OAI.PowerSaving.RAM.Bench.Kit line 18

    Source comment

    all chip fields within budget
    structure Kit (b : Bench m ι) (Y : ι→Shard) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  2. lemma OAI.PowerSaving.RAM.Bench.Kit.lend line 26
  3. lemma OAI.PowerSaving.RAM.Bench.Kit.addr line 29
  4. lemma OAI.PowerSaving.RAM.Bench.Kit.grab line 31
  5. lemma OAI.PowerSaving.RAM.Bench.Kit.transfer line 42
  6. lemma OAI.PowerSaving.RAM.Bench.Kit.roll line 46
  7. lemma OAI.PowerSaving.RAM.Bench.Kit.seedKit line 51
  8. theorem OAI.PowerSaving.RAM.Bench.Bough.prospect line 58
  9. theorem OAI.PowerSaving.RAM.Bench.Bough.bedding line 80
  10. theorem OAI.PowerSaving.RAM.Bench.Bough.glean line 102

    Source documentation

    Apply synchronized scaled-lookup slot to a vector.

    theorem glean (h : b.Bough l r u) (cl : Paint) (x : ι → Line)
    (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (extent (r i) (l i)) (x i)) :
    b.Moves (fun i => extent (r i) (l i)) (a (c cl)) fun i =>
      Tape.tab (extent (r i) (l i)) (graft (extent (r i) (l i))
        (canopy (r i) (fun j => leafM (u i j)) (l i)) (x i)) := by
…

    Mentions: OAI.PowerSaving.RAM.Paint, OAI.PowerSaving.Line, OAI.PowerSaving.Tape.tab, OAI.PowerSaving.RAM.Bench.canopy