OAI/Computability/SpaceSimulation/OneTape/Growth.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Fifths.Cost.Log line 7

   Also declared: ComparatorChallenges/OneTapeSpace.lean:239 (same declaration text).

2. def OAI.Fifths.Cost.exponent line 8

   Also declared: ComparatorChallenges/OneTapeSpace.lean:240 (same declaration text).

3. theorem OAI.Fifths.Cost.logpos line 10
4. theorem OAI.Fifths.Cost.one_le line 11
5. theorem OAI.Fifths.Cost.smallPow line 19
6. theorem OAI.Fifths.Cost.lg_real line 24
7. theorem OAI.Fifths.Cost.log_integer line 37
8. theorem OAI.Fifths.Cost.log_shift line 46
9. theorem OAI.Fifths.Cost.k_fifth line 57
10. theorem OAI.Fifths.Cost.k_real line 67
11. def OAI.Fifths.Cost.factor line 81
12. theorem OAI.Fifths.Cost.fpos line 82
13. theorem OAI.Fifths.Cost.realBound line 83
14. theorem OAI.Fifths.Cost.scaledReal line 97

    Source comment

    The `+1` in a scaled natural bound. State concrete constants. These formulas will be used pointwise.

    theorem scaledReal (d u : ℕ) {T : ℕ} (h : T≥2) :
        ((u*(bound d T+1):ℕ) : ℝ) ≤
          (((u:ℝ)+1)*2*factor d) * (T:ℝ)^exponent * (Log T)^(d+2) := by
    …

    Mentions: OAI.Fifths.Cost.bound, OAI.Fifths.Cost.factor, OAI.Fifths.Cost.exponent, OAI.Fifths.Cost.Log

15. theorem OAI.Fifths.Cost.scaledShift line 110
16. theorem OAI.Fifths.Cost.absorbs line 126

    Source documentation

    Absorb a prescribed polylog with real leading constant and real exponent.

    theorem absorbs (p q : ℝ) (_h : 1 ≤ p) :
        ∃ d c : ℕ, ∀ T : ℕ,
          p * Log T ^ q ≤ ((c*(bound d T + 1):ℕ):ℝ) := by
    …

    Mentions: OAI.Fifths.Cost.Log, OAI.Fifths.Cost.bound