Computing Alternating Series.

Alternating series are particularly nice to sum because each term is also a bound on the error of the partial sum.

Decreasing and Nonnegative


We characterize a decreasing nonnegative stream of rational numbers by saying at every point in the stream s, then every further point in the stream is in [0,s].
Definition DecreasingNonNegative := ForAll (fun (s:Stream Q) => ForAll (fun (t:Stream Q) => 0 <= (hd t) <= (hd s)) s).

An alternative charactherization is that at every point in the stream the second element is in between 0 and the head element.
Definition DecreasingNonNegative_alt := ForAll (fun (s:Stream Q) => 0 <= (hd (tl s)) <= (hd s)).

These two characterizations are equivalent.
Lemma dnn_alt_dnn : forall s, DecreasingNonNegative_alt s -> DecreasingNonNegative s.

Lemma dnn_dnn_alt : forall s, DecreasingNonNegative s -> DecreasingNonNegative_alt s.

Lemma dnn_alt_iff_dnn : forall s, DecreasingNonNegative_alt s <-> DecreasingNonNegative s.

Every tail of a decreasing nonnegative stream is also decreasing and nonnegative.
Lemma dnn_tl : forall s, DecreasingNonNegative s -> DecreasingNonNegative (tl s).
Lemma dnn_Str_nth_tl : forall n s, DecreasingNonNegative s -> DecreasingNonNegative (Str_nth_tl n s).

Section InfiniteAlternatingSum.
Given a stream, we can compute its alternating partial sum up to an point satifying a predicate, so long as that predicate eventually exists.
Definition PartialAlternatingSumUntil (P:Stream Q -> bool)(seq:Stream Q)(ex:LazyExists P seq) : Q :=
(takeUntil P ex Qminus' 0).

The value of the partial sum is between 0 and the head of the sequence if the sequence is decreasing and nonnegative.
Lemma PartialAlternatingSumUntil_small : forall (P:Stream Q -> bool)(seq:Stream Q)(dnn:DecreasingNonNegative seq)(ex:LazyExists P seq), 0 <= (PartialAlternatingSumUntil P ex) <= (hd seq).

A boolean version of Qball.
Definition Qball_ex_bool e a b : bool :=
 if ball_ex_dec _ Qmetric_dec e a b then true else false.

Lemma sumbool_eq_true : forall P (dec:{P}+{~P}), (if dec then true else false) = true <-> P.

If a sequence has a limit of l, then there is a point that gets arbitrarily close to l.
Lemma Limit_near : forall (seq:Stream Q) (l:Q), Limit seq l -> forall e, LazyExists (fun s => Qball_ex_bool e (hd s) l) seq.

The infinte sum of an alternating series is the limit of the partial sums.
Definition InfiniteAlternatingSum_raw (seq:Stream Q)(zl:Limit seq 0)(e:QposInf) :=
PartialAlternatingSumUntil _ (Limit_near zl e).

Lemma InfiniteAlternatingSum_prf : forall seq (dnn:DecreasingNonNegative seq) (zl:Limit seq 0), is_RegularFunction (InfiniteAlternatingSum_raw zl).

Definition InfiniteAlternatingSum (seq:Stream Q)(dnn:DecreasingNonNegative seq)(zl:Limit seq 0) : CR :=
Build_RegularFunction (InfiniteAlternatingSum_prf dnn zl).

Lemma InfiniteAlternatingSum_step : forall seq (dnn:DecreasingNonNegative seq) (zl:Limit seq 0),
 (InfiniteAlternatingSum dnn zl ==
  ('(hd seq))-(InfiniteAlternatingSum (dnn_tl dnn) (Limit_tl zl)))%CR.

The infinite alternating series is always nonnegative.
Lemma InfiniteAlternatingSum_nonneg : forall seq (dnn:DecreasingNonNegative seq) (zl:Limit seq 0),
 (inject_Q 0%Q <= InfiniteAlternatingSum dnn zl)%CR.

The infinite alternating series is always bounded by the first term in the series.
Lemma InfiniteAlternatingSum_bound : forall seq (dnn:DecreasingNonNegative seq) (zl:Limit seq 0),
 (InfiniteAlternatingSum dnn zl <= inject_Q (hd seq))%CR.

InfiniteAlternatingSum is correct.
Lemma dnn_zl_convergent : forall (seq:Stream Q),
 forall (dnn:DecreasingNonNegative seq) (zl:Limit seq 0),
 convergent (fun n => inj_Q IR ((-(1))^n*Str_nth n seq)).

Lemma InfiniteAlternatingSum_correct : forall (seq:Stream Q) (x:nat -> IR),
 (forall n:nat, inj_Q IR (((-(1))^n)*Str_nth n seq)%Q[=]x n) ->
 forall (dnn:DecreasingNonNegative seq) zl H,
 (InfiniteAlternatingSum dnn zl==IRasCR (∑0∞ x H))%CR.

Lemma InfiniteAlternatingSum_correct' : forall (seq:Stream Q),
 forall (dnn:DecreasingNonNegative seq) zl,
 (InfiniteAlternatingSum dnn zl==IRasCR (∑0∞ _ (dnn_zl_convergent dnn zl)))%CR.
End InfiniteAlternatingSum.