OAI/Computability/WLIdentification/FiniteEncoding.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.NumericFinite.elements line 9
  2. def OAI.WLIdentification.NumericFinite.count line 10
  3. theorem OAI.WLIdentification.NumericFinite.elements_zero line 12
  4. theorem OAI.WLIdentification.NumericFinite.elements_succ line 13
  5. theorem OAI.WLIdentification.NumericFinite.count_zero line 18
  6. theorem OAI.WLIdentification.NumericFinite.count_succ line 19
  7. theorem OAI.WLIdentification.NumericFinite.mem_elements line 24
  8. theorem OAI.WLIdentification.NumericFinite.count_mono line 27
  9. theorem OAI.WLIdentification.NumericFinite.count_strict line 32
  10. theorem OAI.WLIdentification.NumericFinite.rank line 39
  11. def OAI.WLIdentification.NumericFinite.select line 58
  12. theorem OAI.WLIdentification.NumericFinite.select_correct line 61
  13. theorem OAI.WLIdentification.WordExpressions.NatPoly.filterCount line 76
  14. theorem OAI.WLIdentification.WordExpressions.NatPoly.filterSelect line 92
  15. def OAI.WLIdentification.WordExpressions.Expr.decisionBound line 115
  16. theorem OAI.WLIdentification.WordExpressions.Expr.decisionBound_polynomial line 118
  17. theorem OAI.WLIdentification.WordExpressions.Expr.decides line 124

    Source documentation

    The output bit is tested by three actual finite-control instructions. Rejection is a literal rejecting state, including on malformed words.

    theorem decides (e : Expr 1) (B : ℕ → ℕ)
    (hw : ∀ n, n ≤ B n) (h : ∀ w, e.Bounded (fun _ => w) (B w.length)) :
    ∃ M : Machine, DecidesWithin M {w | (e.eval (fun _ => w)).getLast?.getD false = true}
      (fun n => e.decisionBound (B n)) := by
…

    Mentions: OAI.WLIdentification.WordExpressions.Expr, OAI.WLIdentification.Machine, OAI.WLIdentification.DecidesWithin

  18. def OAI.WLIdentification.ComputationBounds.Exponential line 170

    Source documentation

    A single exponential with a polynomial exponent (not an iterated exponential).

    def Exponential (f : ℕ → ℕ) : Prop := ∃ C d : ℕ, ∀ n, f n ≤ 2^(C*(n+1)^d)
  19. theorem OAI.WLIdentification.ComputationBounds.power line 172
  20. theorem OAI.WLIdentification.ComputationBounds.exp_dominates line 177
  21. theorem OAI.WLIdentification.ComputationBounds.two_pow line 181
  22. theorem OAI.WLIdentification.ComputationBounds.polynomial_exponential line 185
  23. theorem OAI.WLIdentification.ComputationBounds.exp_constant line 188
  24. theorem OAI.WLIdentification.ComputationBounds.exp_identity line 190
  25. theorem OAI.WLIdentification.ComputationBounds.exp_add line 192
  26. theorem OAI.WLIdentification.ComputationBounds.exp_mul line 208
  27. theorem OAI.WLIdentification.ComputationBounds.exp_power line 218
  28. theorem OAI.WLIdentification.ComputationBounds.polynomial_exp_comp line 223