# Library Coq.Reals.SeqProp

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import Classical.
Require Import Max.
Open Local Scope R_scope.
Convergence properties of sequences
Definition Un_decreasing (Un:nat -> R) : Prop :=
forall n:nat, Un (S n) <= Un n.
Definition opp_seq (Un:nat -> R) (n:nat) : R := - Un n.
Definition has_ub (Un:nat -> R) : Prop := bound (EUn Un).
Definition has_lb (Un:nat -> R) : Prop := bound (EUn (opp_seq Un)).
Lemma growing_cv :
forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l : R | Un_cv Un l }.
Lemma decreasing_growing :
forall Un:nat -> R, Un_decreasing Un -> Un_growing (opp_seq Un).
Lemma decreasing_cv :
forall Un:nat -> R, Un_decreasing Un -> has_lb Un -> { l : R | Un_cv Un l }.
Lemma ub_to_lub :
forall Un:nat -> R, has_ub Un -> { l : R | is_lub (EUn Un) l }.
Lemma lb_to_glb :
forall Un:nat -> R, has_lb Un -> { l : R | is_lub (EUn (opp_seq Un)) l }.
Definition lub (Un:nat -> R) (pr:has_ub Un) : R :=
let (a,_) := ub_to_lub Un pr in a.
Definition glb (Un:nat -> R) (pr:has_lb Un) : R :=
let (a,_) := lb_to_glb Un pr in - a.
Notation maj_sup := ub_to_lub (only parsing).
Notation min_inf := lb_to_glb (only parsing).
Notation majorant := lub (only parsing).
Notation minorant := glb (only parsing).
Lemma maj_ss :
forall (Un:nat -> R) (k:nat),
has_ub Un -> has_ub (fun i:nat => Un (k + i)%nat).
Lemma min_ss :
forall (Un:nat -> R) (k:nat),
has_lb Un -> has_lb (fun i:nat => Un (k + i)%nat).
Definition sequence_ub (Un:nat -> R) (pr:has_ub Un)
(i:nat) : R := lub (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr).
Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
(i:nat) : R := glb (fun k:nat => Un (i + k)%nat) (min_ss Un i pr).
Notation sequence_majorant := sequence_ub (only parsing).
Notation sequence_minorant := sequence_lb (only parsing).
Lemma Wn_decreasing :
forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
Lemma Vn_growing :
forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_lb Un pr).
Lemma Vn_Un_Wn_order :
forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un)
(n:nat), sequence_lb Un pr2 n <= Un n <= sequence_ub Un pr1 n.
Lemma min_maj :
forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un),
has_ub (sequence_lb Un pr2).
Lemma maj_min :
forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un),
has_lb (sequence_ub Un pr1).
Lemma cauchy_maj : forall Un:nat -> R, Cauchy_crit Un -> has_ub Un.
Lemma cauchy_opp :
forall Un:nat -> R, Cauchy_crit Un -> Cauchy_crit (opp_seq Un).
Lemma cauchy_min : forall Un:nat -> R, Cauchy_crit Un -> has_lb Un.
Lemma maj_cv :
forall (Un:nat -> R) (pr:Cauchy_crit Un),
{ l : R | Un_cv (sequence_ub Un (cauchy_maj Un pr)) l }.
Lemma min_cv :
forall (Un:nat -> R) (pr:Cauchy_crit Un),
{ l : R | Un_cv (sequence_lb Un (cauchy_min Un pr)) l }.
Lemma cond_eq :
forall x y:R, (forall eps:R, 0 < eps -> Rabs (x - y) < eps) -> x = y.
Lemma not_Rlt : forall r1 r2:R, ~ r1 < r2 -> r1 >= r2.
Lemma approx_maj :
forall (Un:nat -> R) (pr:has_ub Un) (eps:R),
0 < eps -> exists k : nat , Rabs (lub Un pr - Un k) < eps.
Lemma approx_min :
forall (Un:nat -> R) (pr:has_lb Un) (eps:R),
0 < eps -> exists k : nat , Rabs (glb Un pr - Un k) < eps.
Unicity of limit for convergent sequences
Lemma UL_sequence :
forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2.
Lemma CV_plus :
forall (An Bn:nat -> R) (l1 l2:R),
Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2).
Lemma cv_cvabs :
forall (Un:nat -> R) (l:R),
Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l).
Lemma CV_Cauchy :
forall Un:nat -> R, { l : R | Un_cv Un l } -> Cauchy_crit Un.
Lemma maj_by_pos :
forall Un:nat -> R,
{ l : R | Un_cv Un l } ->
exists l : R , 0 < l /\ ( forall n:nat, Rabs (Un n) <= l ).
Lemma CV_mult :
forall (An Bn:nat -> R) (l1 l2:R),
Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2).
Lemma tech9 :
forall Un:nat -> R,
Un_growing Un -> forall m n:nat, (m <= n)%nat -> Un m <= Un n.
Lemma tech10 :
forall (Un:nat -> R) (x:R), Un_growing Un -> is_lub (EUn Un) x -> Un_cv Un x.
Lemma tech13 :
forall (An:nat -> R) (k:R),
0 <= k < 1 ->
Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
exists k0 : R ,
k < k0 < 1 /\
( exists N : nat ,
( forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0 ) ).
Lemma growing_ineq :
forall (Un:nat -> R) (l:R),
Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l.
Un->l => (-Un) -> (-l)
Lemma CV_opp :
forall (An:nat -> R) (l:R), Un_cv An l -> Un_cv (opp_seq An) (- l).
Lemma decreasing_ineq :
forall (Un:nat -> R) (l:R),
Un_decreasing Un -> Un_cv Un l -> forall n:nat, l <= Un n.
Lemma CV_minus :
forall (An Bn:nat -> R) (l1 l2:R),
Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2).
Un -> +oo
Definition cv_infty (Un:nat -> R) : Prop :=
forall M:R, exists N : nat , ( forall n:nat, (N <= n)%nat -> M < Un n ).
Un -> +oo => /Un -> O
Lemma cv_infty_cv_R0 :
forall Un:nat -> R,
(forall n:nat, Un n <> 0) -> cv_infty Un -> Un_cv (fun n:nat => / Un n) 0.
Lemma decreasing_prop :
forall (Un:nat -> R) (m n:nat),
Un_decreasing Un -> (m <= n)%nat -> Un n <= Un m.
|x|^n/n! -> 0
Lemma cv_speed_pow_fact :
forall x:R, Un_cv (fun n:nat => x ^ n / INR (fact n)) 0.