SEQUENCES

-type represents sequences, functions from natural numbers to a codomain type, foundational for convergence, limits, and series in analysis. It captures the discrete indexing central to Riemann sums and beyond.

In this system, sequences bridge type theory with classical analysis, supporting definitions of suprema, infima, and integrals via ordered terms.

Formation

(-Formation). A sequence is a function from to a type , typically or .

type exp =
  | Seq of exp  (* Seq (Lam ("n", Nat, a_n)) *)

Introduction

(-Introduction). A sequence is introduced by a lambda abstraction , where for each .

let sequence_a : exp =
  Seq (Lam ("n", Nat, RealOps (Div, One, NatToReal (Var "n"))))

Elimination

(-Elimination). Evaluating a sequence at yields the term .

let eval_seq (s : exp) (n : exp) : exp =
  App (s, n)  (* a n *)

Computation

(-Computation). Applying a sequence reduces to substituting the index into the sequence body.

let reduce env ctx = function
  | App (Seq (Lam (n, _, body)), arg) -> subst n arg body
  | _ -> ...

Uniqueness

(-Uniqueness). Two sequences are equal if they agree on all indices, i.e., .

let equal env ctx (Seq a) (Seq b) =
  equal env ctx a b

Theorems

(Pointwise Convergence). A sequence converges to if , formalized via .

(Boundedness). A sequence is bounded if .

let bounded_seq (s : exp) (m : exp) =
  Forall ("n", Nat, RealIneq (Lte, RealOps (Abs, App (s, Var "n"), Zero), m))