OAI/Computability/FourierTransform/RoleArrays.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.RAM.Beach line 10
2. abbrev OAI.PowerSaving.RAM.Grain line 11
3. def OAI.PowerSaving.RAM.fleet line 13
4. def OAI.PowerSaving.RAM.ferry line 19
5. def OAI.PowerSaving.RAM.coastline line 23

   Source documentation

   Total certificate action.

   def coastline (r f : ℕ) (p : PWord α ρ) (v : Grain α ρ r f) : Grain α ρ r f :=
   …

   Mentions: OAI.PowerSaving.RAM.Grain

6. theorem OAI.PowerSaving.RAM.coast_cons line 26
7. structure OAI.PowerSaving.RAM.Rig line 35

   Source documentation

   Gear and ready input full role tape.

   structure Rig {α ρ : Type*} (m : Bool) (B f : ι → ℕ) (s : Ty) (x : ι → T s)
       (cl : Paint) (X : Layout α) (R : Layout ρ) (r : ℕ) (v : ∀ i, Grain α ρ r (f i)) : Prop where
   …

   Mentions: OAI.PowerSaving.RAM.Ty, OAI.PowerSaving.RAM.Paint, OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Grain

8. lemma OAI.PowerSaving.RAM.Rig.gather line 49
9. lemma OAI.PowerSaving.RAM.Rig.large line 56
10. lemma OAI.PowerSaving.RAM.Rig.size line 60
11. lemma OAI.PowerSaving.RAM.Rig.addrs line 64
12. lemma OAI.PowerSaving.RAM.Rig.read line 74
13. lemma OAI.PowerSaving.RAM.Rig.chart line 83
14. lemma OAI.PowerSaving.RAM.Rig.ferry_point line 92
15. lemma OAI.PowerSaving.RAM.Rig.ferry_shift line 109
16. lemma OAI.PowerSaving.RAM.Rig.point_cost line 127
17. lemma OAI.PowerSaving.RAM.Rig.shift_cost line 137
18. lemma OAI.PowerSaving.RAM.Rig.little line 149

    Source documentation

    Fixed scalar matrices of C etc.

    lemma little (i j : F) :
        Has m B s sc x fun _ => littleC i j := by
    …

    Mentions: OAI.PowerSaving.RAM.Has, OAI.PowerSaving.RAM.sc

19. lemma OAI.PowerSaving.RAM.Rig.leftOvers line 160
20. lemma OAI.PowerSaving.RAM.Rig.dots_cost line 166

    Source documentation

    r remaining bits before main work.

    lemma dots_cost :
        Can m B s (a (c cl)) x
          (fun i => (fleet X R r (f i)).tape (fun d =>
            chords r (f i) (fun j => v i (d.1,j)) d.2))
          (fun i => (fleet X R r (f i)).n) := by
    …

    Mentions: OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.fleet