SEQ LIMIT

-type formalizes the limit of a sequence, capturing the value to which a sequence converges in or . It is a cornerstone of analysis, enabling precise definitions of continuity and integration.

In this system, operates on sequences, leveraging and Z3 to verify convergence properties, aligning with classical and constructive analysis.

Formation

(-Formation). A limit is a proposition asserting that a sequence converges to a value as the index approaches infinity or another point.

type exp =
  | Limit of exp * exp * exp * exp  (* Limit (a, p, l, Prop) *)

Introduction

(-Introduction). A limit is introduced by proving that for all , there exists an such that for all , , forming a propositional term.

let limit_a : exp =
  Limit (Seq sequence_a, Infinity, Zero,
    Lam ("ε", Real,
      Lam ("p", RealIneq (Gt, Var "ε", Zero),
        Pair (RealOps (Div, One, Var "ε"),
          Lam ("n", Nat,
            Lam ("q", RealIneq (Gt, Var "n", Var "N"),
              RealIneq (Lt,
                RealOps (Abs,
                RealOps (Minus, App (sequence_a, Var "n"),
                  Zero), Zero), Var "ε")))))))

Elimination

(-Elimination). If , then can be used as the limiting value in further propositions or computations.

let infer env ctx (Limit (a, p, l, prop)) =
  check env ctx a (Seq Real); check env ctx l Real; Prop

Computation

(-Computation). The limit proposition is verified by Z3, reducing to if the - condition holds, otherwise .

let reduce env ctx (Limit (a, Infinity, l, prop)) =
  smt_verify_iff ctx_z3 prop True

Uniqueness

(-Uniqueness). The limit of a sequence is unique in (e.g., ), as any two limits must be equal.

let equal env ctx (Limit (a1, p1, l1, _)) (Limit (a2, p2, l2, _)) =
  equal env ctx a1 a2 && equal env ctx p1 p2 && equal env ctx l1 l2

Theorems

(Cauchy Criterion). A sequence converges if and only if it is Cauchy, i.e., .

(Limit of Bounded Monotone). Every bounded, monotone sequence in has a limit, by completeness.

let monotone_limit (a : exp) (l : exp) =
  And (Forall ("n", Nat,
    RealIneq (Lte,
      App (a, Var "n"),
      App (a, NatOps (Plus, Var "n", One)))),
    Limit (a, Infinity, l, True))