OAI/Computability/FourierTransform/LoopBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PowerSaving.RAM.During line 11

   Source documentation

   Parameters on which a loop body must be uniform.

   structure During {ι : Type U} (n : ι → ℕ) where
   …

2. theorem OAI.PowerSaving.RAM.Able.sum_time line 22
3. theorem OAI.PowerSaving.RAM.Able.loop line 29
4. theorem OAI.PowerSaving.RAM.Able.tab line 64
5. theorem OAI.PowerSaving.RAM.Able.sow line 94
6. theorem OAI.PowerSaving.RAM.Able.ifz line 136

   Source documentation

   Only require the guarantee on the active branch. Budget/charge functions of i can also depend on the branch.

   theorem ifz
       (hx : Able m b s w x n W' Z')
       (hz : Able m (b.comap (fun i : {i // n i = 0} => i.val)) s t
         (fun i => x i.val) (fun i => y i.val) (fun i => W i.val) (fun i => Z i.val))
       (hn : Able m (b.comap (fun i : {i // n i ≠ 0} => i.val)) s t
         (fun i => x i.val) (fun i => y i.val) (fun i => W i.val) (fun i => Z i.val)) :
       Able m b s t x y (fun i => W' i+W i) (fun i => Z' i+Z i) := by
   …

   Mentions: OAI.PowerSaving.RAM.Able