TensorAlgorithm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PowerSaving.RAM.Able.branch line 16

Source documentation

With a closed-code test.

lemma branch (h : Can m b.B s w x n W) (P : ι → Prop) (hp : ∀ i, n i=0 ↔ P i)
    (g : Able m (b.comap (fun i : {i // P i} => i.1)) s t
      (fun i => x i.1) (fun i => y i.1) (fun i => W i.1) (fun i => Z i.1))
    (k : Able m (b.comap (fun i : {i // ¬P i} => i.1)) s t
      (fun i => x i.1) (fun i => y i.1) (fun i => W i.1) (fun i => Z i.1)) :
    Able m b s t x y W Z := by
…

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

def OAI.PowerSaving.RAM.Able.defaultProg line 34

lemma OAI.PowerSaving.RAM.Able.dispatch line 41

Source documentation

Dispatch according to a bounded integer.

lemma dispatch (d : ℕ) (h : Can m b.B s w x n W)
    (hd : ∀ i, n i<d)
    (g : ∀ k<d, Able m (b.comap (fun i : {i // n i=k} => i.1)) s t
      (fun i => x i.1) (fun i => y i.1) (fun i => W i.1) (fun i => Z i.1)) :
    Able m b s t x y W Z := by
…

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

lemma OAI.PowerSaving.RAM.fixed_order line 74
Source comment
Handles small tensor orders. all logical coordinates are fixed-size in this lemma.
```
lemma fixed_order (m : Bool) (B W : ι → ℕ) (cl : Paint) (k : ℕ) (R : Layout ρ)
    (v : ι→ Sim ρ k→ℂ) :
    Can m B (simIn cl) (bundle cl) (fun i => loaded cl R k (v i))
      (fun i => (sim R k).tape (whole k (v i))) W := by
…
```
Mentions: OAI.PowerSaving.RAM.Paint, OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Sim, OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.simIn, OAI.PowerSaving.RAM.bundle, OAI.PowerSaving.RAM.loaded, OAI.PowerSaving.RAM.sim, OAI.PowerSaving.RAM.whole
lemma OAI.PowerSaving.RAM.almost_fixed line 116