Geometric Series

A geometric series is simple to sum. However we do something slightly more general. We sum a series that satifies the ratio test.

Section GeometricSeries.
Variable a : Q.

Hypothesis Ha0 : 0 <= a.
Hypothesis Ha1 : a < 1.

The definition of what we are calling a GeometricSeries: a series that satifies the ratio test.
Definition GeometricSeries := ForAll (fun s => Qabs ((hd (tl s))) <= a*(Qabs(hd s))).

err_bound is a bound on how the series could be in terms of its head elemement.
Let err_bound (s:Stream Q) : Q := Qabs (hd s)/(1-a).

err_prop: is err an bound on the series s?
Let err_prop (err:Q) (s:Stream Q) : bool :=
match ((err_bound s) ?= err) with
 Gt => false
|_ => true
end.


Lemma err_prop_prop : forall e s, err_prop e s <-> err_bound s <= e.

The key lemma bout error bounds.
Lemma err_prop_key : forall (e:Q) (s: Stream Q) (x:Q),
 err_prop e s -> Qabs x <= a*e -> Qabs (Qplus' (hd s) x) <= e.

Lemma err_prop_key' : forall (e:Q) (s: Stream Q),
 GeometricSeries s -> err_prop e s -> err_prop (a*e) (tl s).

Lemma err_prop_monotone : forall (e0 e1:Q) (s: Stream Q), (e0 <= e1) -> err_prop e0 s -> err_prop e1 s.

Lemma err_prop_monotone' : forall (e:Q) (s: Stream Q), GeometricSeries s -> err_prop e s -> err_prop e (tl s).

InfiniteSum is sums the series s.

InfiniteSum_raw_F is the body of the fixpoint. It tests the error of the partial sum and bails out early if the error becomes small enough.
Definition InfiniteSum_raw_F rec (err_prop:Stream Q -> bool) (s:Stream Q) : Q :=
if (err_prop s) then 0 else (Qplus' (hd s) (rec err_prop (tl s))).

By carefully using continuations, we can efficently compute n iterations of InfiniteSum_raw_F with call-by-value.
Fixpoint InfiniteSum_raw_N (n:positive) (cont: (Stream Q -> bool) -> Stream Q -> Q) {struct n} : (Stream Q -> bool) -> Stream Q -> Q :=
match n with
| xH => InfiniteSum_raw_F cont
| xO n' => InfiniteSum_raw_N n' (fun err s => InfiniteSum_raw_N n' cont err s)
| xI n' => InfiniteSum_raw_F (fun err s =>
 (InfiniteSum_raw_N n' (fun err s => InfiniteSum_raw_N n' cont err s)) err s)
end.

Lemmas for reasoning about InfiniteSum_raw_N.
Lemma InfiniteSum_raw_N_F : forall p c,
 InfiniteSum_raw_N p (fun err s => InfiniteSum_raw_F c err s)=
 InfiniteSum_raw_F (fun err s => InfiniteSum_raw_N p c err s).

Lemma InfiniteSum_raw_N_Psucc : forall p c,
 InfiniteSum_raw_N (Psucc p) c =
 InfiniteSum_raw_F (fun err s => InfiniteSum_raw_N p c err s).

Lemma InfiniteSum_raw_N_extend' : forall (p q:positive) s (err : Stream Q -> bool),
 (err (Str_nth_tl (nat_of_P p) s)) -> (p <= q)%Z ->
 InfiniteSum_raw_N p (fun _ _ => 0) err s = InfiniteSum_raw_N q (fun _ _ => 0) err s.

Lemma InfiniteSum_raw_N_extend : forall (p:positive) s (err : Stream Q -> bool),
 (err (Str_nth_tl (nat_of_P p) s)) ->
 InfiniteSum_raw_N p (fun _ _ => 0) err s = InfiniteSum_raw_N (Psucc p) (fun _ _ => 0) err s.

Lemma InfiniteSum_raw_N_ind : forall (err:Stream Q -> bool) (P:Stream Q -> Q -> Prop),
 (forall s, (err s) -> P s 0) ->
 (forall s rec, ~(err s) -> P (tl s) rec -> P s (Qplus' (hd s) rec)) ->
 forall (p:positive) s, (err (Str_nth_tl (nat_of_P p) s)) -> P s (InfiniteSum_raw_N p (fun err s => 0) err s).

The infinite sum is indeed bounded by an error bound.
Lemma err_prop_correct : forall (e:Qpos) s, (GeometricSeries s) -> (err_prop e s) ->
 forall (p:positive) (e':Stream Q -> bool),
  (e' (Str_nth_tl (nat_of_P p) s)) -> Qabs (InfiniteSum_raw_N p (fun err s => 0) e' s) <= e.

This lemma tells us how to compute an upper bound on the number of terms we will need to compute. It is okay for this error to be loose because the partial sums will bail out early when it sees that its estimate of the error is small enough.
Lemma GeometricCovergenceLemma : forall (n:positive) (e:Qpos),
 /(e*(1 - a)) <= n -> a^n <= e.

Definition InfiniteGeometricSum_maxIter series (err:Qpos) : positive :=
let x := (1-a) in
let (n,d) := (Qabs (hd series))/(err*x*x) in
match Zsucc (Zdiv n d) with
| Zpos p => p
| _ => 1%positive
end.

Lemma InfiniteGeometricSum_maxIter_monotone : forall series (err:Qpos),
 GeometricSeries series ->
 (InfiniteGeometricSum_maxIter (tl series) err <= InfiniteGeometricSum_maxIter series err)%Z.

Lemma InfiniteGeometricSum_maxIter_correct : forall series (err:Qpos), GeometricSeries series ->
 err_prop err (Str_nth_tl (nat_of_P (InfiniteGeometricSum_maxIter series err)) series).

The implemenation of InfiniteGeometricSum.
Definition InfiniteGeometricSum_raw series (e:QposInf) : Q :=
match e with
| ∞ => 0
| Qpos2QposInf err => InfiniteSum_raw_N (InfiniteGeometricSum_maxIter series err)
  (fun err s => 0) (err_prop err) series
end.

Lemma InfiniteGeometricSum_raw_prf : forall series, GeometricSeries series ->
is_RegularFunction (InfiniteGeometricSum_raw series).

Definition InfiniteGeometricSum series (Gs:GeometricSeries series) : CR :=
Build_RegularFunction (InfiniteGeometricSum_raw_prf Gs).

The InfiniteGeometricSum is correct.
Lemma InfiniteGeometricSum_step : forall series (Gs:GeometricSeries series),
 (InfiniteGeometricSum Gs ==
  ('(hd series))+(InfiniteGeometricSum (ForAll_Str_nth_tl 1%nat Gs)))%CR.

Lemma InfiniteGeometricSum_bound : forall series
 (Gs:GeometricSeries series),
 AbsSmall (R:=CRasCOrdField) ('(err_bound series))%CR (InfiniteGeometricSum Gs).

Lemma InfiniteGeometricSum_small_tail : forall series (e : Q+),
GeometricSeries series ->
{n : N & forall Gs : GeometricSeries (Str_nth_tl n series),
AbsSmall (R:=CRasCOrdField) (' e)%CR (InfiniteGeometricSum Gs)}.

Lemma GeometricSeries_convergent : forall (series:Stream Q),
 GeometricSeries series ->
 convergent (fun n => inj_Q IR (Str_nth n series)).

Lemma InfiniteGeometricSum_correct : forall (series:Stream Q) (x:nat -> IR),
 (forall n:nat, inj_Q IR (Str_nth n series)%Q[=]x n) ->
 forall (Gs:GeometricSeries series) H,
 (InfiniteGeometricSum Gs==IRasCR (∑0∞ x H))%CR.

Lemma InfiniteGeometricSum_correct' : forall (series:Stream Q),
 forall (Gs:GeometricSeries series),
 (InfiniteGeometricSum Gs == IRasCR (∑0∞ _ (GeometricSeries_convergent Gs)))%CR.

End GeometricSeries.