OAI/Computability/FourierTransform/RecursiveBatches.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.RAM.Sim line 9

   Source documentation

   An instance of the simultaneous kernel program.

   abbrev Sim (ρ : Type*) (k : ℕ) := ρ × Bits k

2. def OAI.PowerSaving.RAM.sim line 10
3. abbrev OAI.PowerSaving.RAM.bundle line 12
4. abbrev OAI.PowerSaving.RAM.simIn line 13
5. abbrev OAI.PowerSaving.RAM.hatch line 14
6. def OAI.PowerSaving.RAM.whole line 16
7. def OAI.PowerSaving.RAM.loaded line 19
8. def OAI.PowerSaving.RAM.cut line 24

   Source comment

   cut t groups of R.n fibers from the peeled coordinates

   def cut {β ρ} (r f t : ℕ) (X : Layout β) (R : Layout ρ)
       (h : t*R.n = (book X r f).n) :
       (Fin t × ρ) ≃ Grid β r f :=
   …

   Mentions: OAI.PowerSaving.Layout

9. lemma OAI.PowerSaving.RAM.cut_eq line 30
10. lemma OAI.PowerSaving.RAM.uncut_eq line 35
11. def OAI.PowerSaving.RAM.fill line 47

    Source documentation

    Source data for one recursive call (one batch).

    def fill (l : ρ) (j : α) (z : Space α) {r f t : ℕ} (X : Layout (Minus j))
        (R : Layout ρ) (h : t*R.n=(book X r f).n)
        (v : Grain α ρ r f) (b : Fin t) : Sim ρ f → ℂ :=
    …

    Mentions: OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Grain, OAI.PowerSaving.RAM.Sim

12. def OAI.PowerSaving.RAM.yieldTape line 54

    Source documentation

    Collection of returned answers.

    def yieldTape (l : ρ) (j : α) (z : Space α) {r f t} (X : Layout (Minus j))
        (R : Layout ρ) (h : t*R.n=(book X r f).n) (v : Grain α ρ r f) : Tape (Tape ℂ) :=
    …

    Mentions: OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Grain, OAI.PowerSaving.Tape

13. lemma OAI.PowerSaving.RAM.fill_result line 60

    Source comment

    proof calculation for one direction

    lemma fill_result [Fintype ρ] [DecidableEq ρ] (l : ρ) (j : α) (z : Space α)
        (hz : z j=1) (hn : z≠0) {r f t} (X : Layout (Minus j)) (R : Layout ρ) h
        (v : Grain α ρ r f) (a : Grid α r f) :
        let q := peelBook j z r f a
    …

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

14. lemma OAI.PowerSaving.RAM.Rig.simSmall line 88
15. lemma OAI.PowerSaving.RAM.Rig.simSize line 92
16. lemma OAI.PowerSaving.RAM.Rig.batchSmall line 100
17. lemma OAI.PowerSaving.RAM.Rig.batchSize line 107
18. lemma OAI.PowerSaving.RAM.Rig.fill_read line 113
19. lemma OAI.PowerSaving.RAM.Rig.fill_ready line 134
20. lemma OAI.PowerSaving.RAM.Rig.direction_get line 155

    Source comment

    compute a directional outcome from the packed answers (and from unchanged roles)

    lemma direction_get (hn : z≠0) (hz : z j=1)
        (H : Has m B s (Ty.a (bundle cl)) x fun i => yieldTape l j z X' R (hg i) (v i))
        (a : ∀ i, Beach α ρ r (f i)) (ha : Knows m B s x fun i => (fleet X R r (f i)).loc (a i)) :
        Has m B s (c cl) x fun i => ferry r (f i) (.dir l z hn) (v i) (a i) := by
    …

    Mentions: OAI.PowerSaving.RAM.Has, OAI.PowerSaving.RAM.bundle, OAI.PowerSaving.RAM.yieldTape, OAI.PowerSaving.RAM.Beach, OAI.PowerSaving.RAM.Knows, OAI.PowerSaving.RAM.fleet, OAI.PowerSaving.RAM.ferry