OAI/Computability/FourierTransform/ColumnAddresses.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Constant (i.e. independent of f) work for transposed-column addresses. The number of bits per COLUMN is fixed. Groups of f bits have prepared powers and XOR table.

  1. abbrev OAI.PowerSaving.RAM.Has line 15

    Source documentation

    "Ready", i.e. can be computed in constant work, not free.

    abbrev Has (m : Bool) (B : ι → ℕ) (s t : Ty) (x : ι → T s) (y : ι → T t) : Prop :=
…

    Mentions: OAI.PowerSaving.RAM.Ty

  2. abbrev OAI.PowerSaving.RAM.Knows line 17
  3. structure OAI.PowerSaving.RAM.Gear line 22

    Source documentation

    Particular indexing programs are proved uniformly over all f through this finite syntax interface.

    structure Gear (m : Bool) (B f : ι → ℕ) (s : Ty) (x : ι → T s) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Ty

  4. lemma OAI.PowerSaving.RAM.Gear.descend line 33
  5. lemma OAI.PowerSaving.RAM.Gear.body_size line 43
  6. lemma OAI.PowerSaving.RAM.Gear.body_small line 47
  7. lemma OAI.PowerSaving.RAM.Gear.grid_size line 52
  8. lemma OAI.PowerSaving.RAM.Gear.grid_small line 57
  9. lemma OAI.PowerSaving.RAM.Gear.body_get line 62
  10. lemma OAI.PowerSaving.RAM.Gear.body_set line 74
  11. lemma OAI.PowerSaving.RAM.Gear.grid_fetch line 89
  12. lemma OAI.PowerSaving.RAM.Gear.grid_combine line 99
  13. lemma OAI.PowerSaving.RAM.Gear.addr_xor line 106
  14. lemma OAI.PowerSaving.RAM.Gear.shifted line 114

    Source documentation

    Address translated by z (across f columns).

    lemma shifted (z : Space α) (v : ∀ i, Grid α r (f i))
    (h : Knows m B s x (fun i => (book X r (f i)).loc (v i))) :
    Knows m B s x (fun i => (book X r (f i)).loc ((v i).1,
      fun j => (v i).2 j + z)) := by
…

    Mentions: OAI.PowerSaving.RAM.Knows

  15. lemma OAI.PowerSaving.RAM.Gear.from_grid line 137

    Source documentation

    Program can go back and forth between grid and (fiber,within-fiber).

    lemma from_grid (j : α) (X' : Layout (Minus j)) (z : Space α)
    (v : ∀ i, Grid α r (f i))
    (h : Knows m B s x (fun i => (book X r (f i)).loc (v i))) :
    let u i := peelBook j z r (f i) (v i)
…

    Mentions: OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Knows

  16. lemma OAI.PowerSaving.RAM.Gear.to_grid line 159