Library Coq.Reals.SeqProp
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 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)
Un -> +oo
Un -> +oo => /Un -> O
|x|^n/n! -> 0