TensorRecursion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PowerSaving.RAM.ebb line 15
lemma OAI.PowerSaving.RAM.ebb_eq line 20
lemma OAI.PowerSaving.RAM.amplifies line 33

lemma OAI.PowerSaving.RAM.amplify line 54

Source documentation

Body proof with fixed r. B need only dominate 2^k polynomially.

lemma amplify (m : Bool) (b : Bank (hatch cl) ι) (v : ∀ i, Sim ρ (k i) → ℂ)
    (X : Layout α) (R : Layout ρ) (r : ℕ)
    (hr : 3 ≤ X.n) (hq : ∀ i, X.n*f i+r=k i) (hd : r < X.n)
    (hc : ∀ i, n i*(sim R (f i)).n=2^k i)
    (hk : Contract cl b f τ R)
    (hB : Small b.B (fun i => 2^k i))
    (p : PWord α ρ) (hp : ∀ f v, walk f p v = multiAct f (fun _ => kernel α) v) :
    Able m b (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 => 2^k i) (fun i => tally p*n i*τ i) := by
…

Mentions: OAI.PowerSaving.RAM.Bank, OAI.PowerSaving.RAM.hatch, OAI.PowerSaving.RAM.Sim, OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.sim, OAI.PowerSaving.RAM.Contract, OAI.PowerSaving.RAM.Small, OAI.PowerSaving.RAM.Able, OAI.PowerSaving.RAM.simIn, OAI.PowerSaving.RAM.bundle, OAI.PowerSaving.RAM.loaded, OAI.PowerSaving.RAM.whole