OAI/Computability/FourierTransform/SectorIdentities.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Shard effect = binary kernel applied in contiguous sectors.

  1. def OAI.PowerSaving.Grove.fleck line 13

    Source documentation

    natural address binary kernel

    def fleck (i j : ℕ) : ℂ := if i=j then ca else cb
  2. def OAI.PowerSaving.Grove.prism line 14
  3. def OAI.PowerSaving.Grove.gleam line 17
  4. lemma OAI.PowerSaving.Grove.bits_next line 19
  5. lemma OAI.PowerSaving.Grove.prism_loc line 24
  6. lemma OAI.PowerSaving.Grove.sum_bits_addr line 39
  7. lemma OAI.PowerSaving.Grove.gleam_loc line 44
  8. def OAI.PowerSaving.Grove.gleans line 51
  9. lemma OAI.PowerSaving.Grove.leaf_gleans line 54
  10. lemma OAI.PowerSaving.Grove.prism_fringe line 84

    Source documentation

    The prism multiplies under shard composition. Need low-word append of only two choices (0 or 1 low bits).

    lemma prism_fringe {n l m : ℕ} {u x v y : Shard}
    (_hl : u.Mark n l) (_hl' : v.Mark n l) (hn : x.Mark m 1) (hn' : y.Mark m 1)
    (hs : x.same y) :
    prism (fringe m u x).height (fringe m u x).seat (fringe m v y).seat =
    prism u.height u.seat v.seat * prism x.height x.seat y.seat := by
…

    Mentions: OAI.PowerSaving.Grove.Shard, OAI.PowerSaving.Grove.prism

  11. lemma OAI.PowerSaving.Grove.gleans_fringe line 109
  12. lemma OAI.PowerSaving.Grove.canopy_gleans line 139
  13. def OAI.PowerSaving.Grove.stow line 158

    Source comment

    operation in packed addresses
    def stow (n : ℕ) (f : ℕ → Shard) (x : Line) : Line :=
…

    Mentions: OAI.PowerSaving.Grove.Shard, OAI.PowerSaving.Line

  14. def OAI.PowerSaving.Grove.slit line 161
  15. def OAI.PowerSaving.Grove.glimpse line 165

    Source documentation

    local output from packed data at a sector address.

    def glimpse (n : ℕ) (f : ℕ → Shard) (x : Line) (j : ℕ) : Line :=
…

    Mentions: OAI.PowerSaving.Grove.Shard, OAI.PowerSaving.Line

  16. lemma OAI.PowerSaving.Grove.sum_zone line 168
  17. lemma OAI.PowerSaving.Grove.graft_glimpse line 183
  18. def OAI.PowerSaving.Grove.seatfare line 243

    Source comment

    sector start width sums (need cost bound on packed call).
    def seatfare (n : ℕ) (f : ℕ→Shard) (j : ℕ) :=
…

    Mentions: OAI.PowerSaving.Grove.Shard

  19. lemma OAI.PowerSaving.Grove.fare_sum line 246