Operations on Sequences

These are common operations on sequences that we will be using.

everyOther


everyOther drops ever other term.
CoFixpoint everyOther (A:Type) (s:Stream A) : Stream A :=
Cons (hd s) (everyOther (tl (tl s))).

It preserves DecreasingNonNegative.
Lemma everyOther_dnn : forall (a : Stream Q),
 (DecreasingNonNegative a) ->
 (DecreasingNonNegative (everyOther a)).

It preserves limits.
Lemma everyOther_nbz : forall (a : Stream Q) x, (NearBy 0 x a) ->
 NearBy 0 x (everyOther a).

Lemma everyOther_zl : forall (a : Stream Q), (Limit a 0) ->
 Limit (everyOther a) 0.

Its characterization.
Lemma Str_nth_tl_everyOther : forall n A (a:Stream A), Str_nth_tl n (everyOther a) = everyOther (Str_nth_tl (2*n) a).

Lemma Str_nth_everyOther : forall n A (a:Stream A), Str_nth n (everyOther a) = (Str_nth (2*n) a).

mult_Streams

The point wise product of two streams.
Definition mult_Streams := zipWith (Qmult).

It preserves convergeing to 0.
Lemma mult_Streams_nbz : forall (a b : Stream Q) x, (NearBy 0 x a) -> forall y, NearBy 0 y b ->
 NearBy 0 (x*y) (mult_Streams a b).

Lemma ForAll_True : forall X (S:Stream X), ForAll (fun x => True) S.

Lemma mult_Streams_zl : forall (a b : Stream Q), (Limit a 0) -> forall (x:Qpos), NearBy 0 x b ->
 Limit (mult_Streams a b) 0.

It preserves DecreasingNonNegative.
Lemma mult_Streams_dnn : forall (a b : Stream Q),
 (DecreasingNonNegative a) ->
 (DecreasingNonNegative b) ->
 (DecreasingNonNegative (mult_Streams a b)).



StreamBounds

StreamBounds says that one stream pointwise bounds the absolute value of the other.
Definition StreamBounds (a b : Stream Q) := ForAll (fun (x:Stream (Q*Q)) => let (a,b):=(hd x) in AbsSmall a b) (zipWith (@pair _ _) a b).

If the bounding stream goes to 0, so does the bounded stream.
Lemma Stream_Bound_nbz : forall a b e, (StreamBounds a b) -> NearBy 0 e a -> NearBy 0 e b.

Lemma Stream_Bound_zl : forall a b, (StreamBounds a b) -> Limit a 0 -> Limit b 0.

If one stream is DecreasingNonNegative and the other is a GeometricSeries, then the result is a GeometricSeries.
Lemma mult_Streams_Gs : forall a (x y : Stream Q),
 (DecreasingNonNegative x) ->
 (GeometricSeries a y) ->
 (GeometricSeries a (mult_Streams x y)).

Section Powers.

Variable a : Q.

powers

The stream of powers of a.
CoFixpoint powers_help (c:Q) : Stream Q :=
Cons c (powers_help (c*a)).

Definition powers := powers_help 1.

Lemma Str_nth_powers_help : forall n x, Str_nth n (powers_help x) == x*a^n.

Lemma Str_nth_powers : forall n, Str_nth n powers == a^n.

powers is a GeometricSeries.
Lemma powers_help_Gs : (0 <= a) -> forall c,
 (GeometricSeries a (powers_help c)).

Lemma powers_Gs : (0 <= a) -> (GeometricSeries a powers).

Hypothesis Ha : 0 <= a <= 1.

It is decreasing an nonnegative when a is between 0 and 1.
Lemma powers_help_dnn : forall x, (0 <= x) -> DecreasingNonNegative (powers_help x).

Lemma powers_dnn : DecreasingNonNegative powers.

Lemma powers_help_nbz : forall x, 0 <= x <= 1 -> NearBy 0 (1#1)%Qpos (powers_help x).

Lemma powers_nbz : NearBy 0 (1#1)%Qpos powers.

End Powers.

positives

The stream of postive numbers.
CoFixpoint positives_help (n:positive) : Stream positive :=
Cons n (positives_help (Psucc n)).

Definition positives := positives_help 1.

Lemma Str_nth_positives : forall n, Str_nth n positives = P_of_succ_nat n.

recip_positives

The stream of 1/n.
Definition recip_positives := map (fun x => 1#x) positives.

Lemma Str_nth_recip_positives : forall n, Str_nth n recip_positives = 1#(P_of_succ_nat n).

The limit of recip_positives is 0.
Lemma recip_positives_help_nbz : forall (n d q:positive), (d <= q)%Z -> NearBy 0 (n#d)%Qpos (map (fun x => 1#x) (positives_help q)).

Lemma recip_positives_help_Exists : forall P n p, LazyExists P (map (fun x => (1#x)) (positives_help (Pplus_LazyNat p n))) -> LazyExists P (map (fun x => (1#x)) (positives_help p)).

Lemma recip_positives_zl : Limit recip_positives 0.

recip_positives is DecreasingNonNegative.
Lemma recip_positives_dnn : DecreasingNonNegative recip_positives.

factorials

The stream of factorials.
CoFixpoint factorials_help (n c:positive) : Stream positive :=
Cons c (factorials_help (Psucc n) (n*c)).

Definition factorials := factorials_help 1 1.

Lemma Str_nth_factorials : forall n, nat_of_P (Str_nth n factorials) = fac n.

recip_factorials

The stream of 1/n!.
Definition recip_factorials := map (fun x => 1#x) factorials.

Lemma Str_nth_recip_factorials : forall n, (Str_nth n recip_factorials) = 1#(P_of_succ_nat (pred (fac n))).

recip_factorials is DecreasingNonNegative.
Lemma recip_factorials_dnn : DecreasingNonNegative recip_factorials.

The limit of recip_factorial is 0.
Lemma recip_factorial_bounded : StreamBounds recip_positives (tl recip_factorials).

Lemma recip_factorials_zl : Limit recip_factorials 0.