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 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)
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
|x|^n/n! -> 0