OAI/Computability/FourierTransform/RecursionBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.RAM.threshold line 9
2. def OAI.PowerSaving.RAM.batches line 10
3. def OAI.PowerSaving.RAM.allot line 12
4. lemma OAI.PowerSaving.RAM.down_lt line 18
5. lemma OAI.PowerSaving.RAM.rounds_eq line 26
6. structure OAI.PowerSaving.RAM.Desc line 40

   Source documentation

   Parameters included in the open-code guarantee.

   structure Desc (cl : Paint) (u a : ℕ) (R : Layout ρ) where
   …

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

7. def OAI.PowerSaving.RAM.funds line 50
8. def OAI.PowerSaving.RAM.charging line 53
9. lemma OAI.PowerSaving.RAM.rec_body line 56
10. theorem OAI.PowerSaving.RAM.recurse_run line 112

    Source documentation

    Recursion closed.

    theorem recurse_run (cl : Paint) (m : Bool) (X : Layout α) (R : Layout ρ) (u a : ℕ)
        (hX : X.n=u) (hu : 3≤u) (hR : R.n=2^a) (p : PWord α ρ)
        (hp : ∀ f v, walk f p v = multiAct f (fun _ => kernel α) v) {ι : Type*}
        (k : ι→ℕ) (v : ∀ i,Sim ρ (k i)→ℂ) :
        Can m (fun i => 2^k i) (simIn cl) (bundle cl) (fun i => loaded cl R (k i) (v i))
          (fun i => (sim R (k i)).tape (whole (k i) (v i)))
          (fun i => allot u a (tally p) (k i)) := 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, OAI.PowerSaving.RAM.allot