OAI/Computability/SpaceSimulation/OneTape/Sizes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Fifths.Cost.lg line 7
2. theorem OAI.Fifths.Cost.lg_pos line 8
3. theorem OAI.Fifths.Cost.lg_mono line 9
4. def OAI.Fifths.Cost.power line 10
5. def OAI.Fifths.Cost.K line 11
6. theorem OAI.Fifths.Cost.K_pos line 12
7. theorem OAI.Fifths.Cost.bigK line 13
8. theorem OAI.Fifths.Cost.K_mono line 17
9. def OAI.Fifths.Cost.bound line 23

   Source documentation

   room for any fixed power of the allowed accessor logarithm and for start-up costs.

   def bound (d T : ℕ) := K T*K T*lg T^(d+2)

   Mentions: OAI.Fifths.Cost.K, OAI.Fifths.Cost.lg

10. theorem OAI.Fifths.Cost.lg_pow_le line 24
11. theorem OAI.Fifths.Cost.lg_le line 28
12. theorem OAI.Fifths.Cost.bound_pos line 33
13. theorem OAI.Fifths.Cost.bound_mono line 34
14. theorem OAI.Fifths.Cost.ofT line 41
15. theorem OAI.Fifths.Scaled.looser line 56
16. theorem OAI.Fifths.Scaled.prodPos line 59
17. theorem OAI.Fifths.Single.estimate line 77

    Source documentation

    Simultaneous verification of register and stack bounds after balancing. Uses arbitrary indices to avoid unnecessary restrictions on profiles of inputs that can be rescanned.

    theorem estimate (d : ℕ) (p : ∀ i, (W i).k = K (W i).T) :
        (Fits (fun i => bound d (W i).T) fun i =>
           let C := (M.tour (x i) (W i)).circuit; C.P.n ^ (C.width+1)) ∧
    …

    Mentions: OAI.Fifths.Fits