INFINITE SUM

-type represents an infinite sum, the limit of partial sums over a sequence or an indexed family of real numbers. It is essential for series, integrals, and measure theory in analysis, generalizing finite addition.

In this system, operates over or indexed sets, leveraging and to define convergence, with Z3 verifying summation properties in Schwartz’s framework.

Formation

(-Formation). An infinite sum is formed over a sequence or an indexed family , yielding a real number if convergent.

type exp =
  | Sum of exp * exp  (* ∑_i a_i, where i : index type *)

Introduction

(-Introduction). The infinite sum is introduced as , the limit of the sequence of partial sums , or over a general index .

let series (a : exp) : exp =
  Sum (Nat, a)

Elimination

(-Elimination). The value of is the real number if the series converges, usable in further computations or inequalities.

Computation

(-Computation). The infinite sum reduces to its limit when convergent, characterized by partial sums and verifiable by Z3 for specific sequences (e.g., geometric series).

Uniqueness

(-Uniqueness). The infinite sum is unique in if it converges, as the limit of partial sums is well-defined.

let equal env ctx (Sum (i1, a1)) (Sum (i2, a2)) =
  equal env ctx i1 i2 && equal env ctx a1 a2

Theorems

(Absolute Convergence). If converges, then converges absolutely, ensuring a real limit.

(Countable Additivity). For a measure and a countable disjoint family , .

let measure_series (mu : exp) (s : exp) =
  SetEq (App (mu, Union (Seq s)),
    Sum (Nat, Seq (Lam ("n", Nat,
      App (mu, App (s, Var "n"))))))