CoRN.reals.PosSeq

Require Export Series.

Section SeqProperties.

Definition seq_pos (x : nat → IR) := ∀ n : nat, [0] [<] x n.
Definition seq_inf_sum (x : nat → IR) :=
∀ M : IR, {N : nat | ∀ m : nat, N ≤ m → M [<] seq_part_sum x m}.

Lemma One_part_sum : ∀ (m : nat), seq_part_sum (fun n : nat ⇒ [1]) m [=] nring m.
Proof.
 intros.
 induction m; simpl; algebra.
Qed.

Lemma One_seq_is_pos : seq_pos (fun n : nat ⇒ [1]).
Proof.
 unfold seq_pos.
 intros. apply pos_one.
Qed.

Lemma One_seq_is_inf_sum : seq_inf_sum (fun n : nat ⇒ [1]).
Proof.
 unfold seq_inf_sum.
 intros.
 assert ({N : nat | M [<] nring N}).
  apply Archimedes'.
 destruct X as [N H].
 ∃ N. intros.
 apply less_leEq_trans with (nring (R:=IR) N); auto.
 assert (seq_part_sum (fun n : nat ⇒ [1]) m [=] nring m).
  apply One_part_sum.
 astepr (nring (R:=IR) m).
 apply nring_leEq.
 auto.
Qed.

Lemma seq_pos_imp_sum_pos : ∀ (x : nat → IR), seq_pos x → ∀ n, [0] [<] seq_part_sum x (S n).
Proof.
 intros.
 induction n.
  simpl.
  astepl ([0][+][0]:IR).
  apply plus_resp_less_lft. apply X.
  simpl.
 simpl in |- ×.
 apply plus_resp_pos.
  apply IHn.
 apply X.
Qed.

Lemma seq_pos_imp_sum_pos' :
    ∀ (x : nat → IR) (H1 : seq_pos x) (n m : nat) (H2 : m < n),
    [0] [<] Sum m n x.
Proof.
 unfold seq_pos.
 intros.
 induction n.
  assert (¬ m < 0). auto with arith. contradiction.
   elim (le_lt_eq_dec _ _ H2); intros H3.
  astepr (Sum m n x [+] x (S n)).
  apply plus_resp_pos.
   apply IHn; auto with arith.
  apply H1.
 replace n with m; auto.
 astepr (Sum m m x [+]x (S m)).
 apply plus_resp_pos.
  astepr (x m).
  apply H1.
 apply H1.
Qed.

Lemma seq_pos_imp_ap_zero : ∀ (x : nat → IR), seq_pos x → ∀ n, seq_part_sum x (S n) [#] [0].
Proof.
 unfold seq_pos.
 intros.
 apply ap_symmetric_unfolded.
 apply less_imp_ap.
 apply seq_pos_imp_sum_pos; auto.
Qed.

Lemma seq_inf_sum_imp_div_small :
∀ (x : nat → IR) (H1 : seq_inf_sum x) (H2: seq_pos x) (C e : IR)
(H4 : [0] [<] e), { N : nat |
  ∀ m : nat, N ≤ m → AbsSmall e (C [/](seq_part_sum x (S m)) [//] (seq_pos_imp_ap_zero x H2 m))}.
Proof.
 unfold seq_inf_sum. unfold seq_pos.
 intros.
 assert ({N : nat | ∀ m : nat,
   N ≤ m → ((AbsIR C)[/]e[//]pos_ap_zero IR e H4)[<]seq_part_sum x m}).
  apply (H1 ((AbsIR C) [/] e [//] (pos_ap_zero IR e H4))).
 destruct X as [N H].
 ∃ N.
 intros.
 assert (H3 : ((AbsIR C)[/]e[//]pos_ap_zero IR e H4)[<]seq_part_sum x (S m)).
  apply H; auto.
 astepr ((C [/] seq_part_sum x (S m)[//] (seq_pos_imp_ap_zero x H2 m))).
 assert (AbsSmall ((seq_part_sum x (S m))[*]e) C).
  apply AbsIR_imp_AbsSmall.
  apply less_leEq.
  apply (shift_less_mult IR (AbsIR C) (seq_part_sum x (S m)) e (pos_ap_zero IR e H4)); auto.
 rstepl ((seq_part_sum x (S m))[*]e [/] (seq_part_sum x (S m))[//]
   pos_ap_zero IR (seq_part_sum x (S m)) (seq_pos_imp_sum_pos x H2 m)).
 rstepr (C [/] (seq_part_sum x (S m))[//]
   pos_ap_zero IR (seq_part_sum x (S m)) (seq_pos_imp_sum_pos x H2 m)).
 apply div_resp_AbsSmall.
 auto.
Qed.

Lemma seq_inf_sum_ratio_bound :
∀ (y : nat→IR) (H2 : seq_pos y) (m N1: nat) (H3: S N1 < m),
AbsSmall [1] (Sum (G:=IR) (S N1) m (fun k : nat ⇒ y k)[/]
                  seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m).
Proof.
 intros.
 apply leEq_imp_AbsSmall.
  apply shift_leEq_div.
   apply seq_pos_imp_sum_pos; auto.
  astepl ([0]:IR).
  apply less_leEq.
  apply seq_pos_imp_sum_pos'; auto.
 apply shift_div_leEq.
  apply seq_pos_imp_sum_pos; auto.
 astepl (Sum (G:=IR) (S N1) m y).
 astepr (seq_part_sum y (S m)).
 unfold Sum. unfold Sum1. unfold seq_part_sum.
 apply shift_zero_leEq_minus'.
 rstepr (Sum0 (G:=IR) (S N1) y).
 apply less_leEq.
 astepr (seq_part_sum y (S N1)).
 apply seq_pos_imp_sum_pos; auto.
Qed.

End SeqProperties.