Library Coq.Reals.Rseries
Definition of sequence and properties
Section sequence.
Variable Un :
nat ->
R.
Boxed Fixpoint Rmax_N (
N:nat) :
R :=
match N with
|
O =>
Un 0
|
S n =>
Rmax (
Un (
S n)) (
Rmax_N n)
end.
Definition EUn r :
Prop :=
exists i :
nat,
r =
Un i.
Definition Un_cv (
l:R) :
Prop :=
forall eps:R,
eps > 0 ->
exists N :
nat, (
forall n:nat, (
n >=
N)%nat ->
R_dist (
Un n)
l <
eps).
Definition Cauchy_crit :
Prop :=
forall eps:R,
eps > 0 ->
exists N :
nat,
(
forall n m:nat,
(
n >=
N)%nat -> (
m >=
N)%nat ->
R_dist (
Un n) (
Un m) <
eps).
Definition Un_growing :
Prop :=
forall n:nat,
Un n <=
Un (
S n).
Lemma EUn_noempty :
exists r :
R,
EUn r.
Lemma Un_in_EUn :
forall n:nat,
EUn (
Un n).
Lemma Un_bound_imp :
forall x:R, (
forall n:nat,
Un n <=
x) ->
is_upper_bound EUn x.
Lemma growing_prop :
forall n m:nat,
Un_growing -> (
n >=
m)%nat ->
Un n >=
Un m.
classical is needed: not_all_not_ex
Definition of Power Series and properties