Section More_Cauchy_Props.

Miscellaneous

More properties of Cauchy sequences

We will now define some special Cauchy sequences and prove some more useful properties about them.

The sequence defined by x(n)=2/(n+1).

Lemma twice_inv_seq_Lim : SeqLimit (R:=IR) (fun n => 2[*]one_div_succ n) 0.

Definition twice_inv_seq : CauchySeq IR.
Defined.



Next, we prove that the sequence of absolute values of a Cauchy sequence is also Cauchy.

Lemma Cauchy_Lim_abs : forall seq y, Cauchy_Lim_prop2 seq y ->
 Cauchy_Lim_prop2 (fun n => AbsIR (seq n)) (AbsIR y).

Lemma Cauchy_abs : forall seq : CauchySeq IR, Cauchy_prop (fun n => AbsIR (seq n)).

Lemma Lim_abs : forall seq : CauchySeq IR,
 Lim (Build_CauchySeq _ _ (Cauchy_abs seq)) [=] AbsIR (Lim seq).

Lemma CS_seq_bounded' : forall seq : CauchySeqR,
 {K : IR | 0 [<] K | forall m : N, AbsSmall K (seq m)}.


End More_Cauchy_Props.

Section Subsequences.

Subsequences

We will now examine (although without formalizing it) the concept of subsequence and some of its properties.

Let seq1,seq2:nat->IR.

In order for seq1 to be a subsequence of seq2, there must be an increasing function f growing to infinity such that forall (n :nat), (seq1 n) = (seq2 (f n)). We assume f to be such a function.

Finally, for some of our results it is important to assume that seq2 is monotonous.

Variables seq1 seq2 : N -> IR.
Variable f : N -> N.

Hypothesis monF : forall m n : N, m <= n -> f m <= f n.
Hypothesis crescF : forall n : N, {m : N | n < m /\ f n < f m}.
Hypothesis subseq : forall n : N, seq1 n [=] seq2 (f n).

Hypothesis mon_seq2 :
 (forall m n, m <= n -> seq2 m [<=] seq2 n) \/ (forall m n, m <= n -> seq2 n [<=] seq2 m).

Lemma unbnd_f : forall m, {n : N | m < f n}.


Lemma conv_subseq_imp_conv_seq : Cauchy_prop seq1 -> Cauchy_prop seq2.

Lemma Cprop2_seq_imp_Cprop2_subseq : forall a,
 Cauchy_Lim_prop2 seq2 a -> Cauchy_Lim_prop2 seq1 a.

Lemma conv_seq_imp_conv_subseq : Cauchy_prop seq2 -> Cauchy_prop seq1.

Lemma Cprop2_subseq_imp_Cprop2_seq : forall a,
 Cauchy_Lim_prop2 seq1 a -> Cauchy_Lim_prop2 seq2 a.

End Subsequences.

Section Cauchy_Subsequences.

Variables seq1 seq2 : CauchySeq IR.
Variable f : N -> N.

Hypothesis monF : forall m n : N, m <= n -> f m <= f n.
Hypothesis crescF : forall n : N, {m : N | n < m /\ f n < f m}.
Hypothesis subseq : forall n : N, seq1 n [=] seq2 (f n).

Hypothesis mon_seq2 :
 (forall m n, m <= n -> seq2 m [<=] seq2 n) \/ (forall m n, m <= n -> seq2 n [<=] seq2 m).

Lemma Lim_seq_eq_Lim_subseq : Lim seq1 [=] Lim seq2.

Lemma Lim_subseq_eq_Lim_seq : Lim seq1 [=] Lim seq2.

End Cauchy_Subsequences.

Section Properties_of_Exponentiation.

More properties of Exponentiation



Finally, we prove that x^n grows to infinity if x > 1.

Lemma power_big' : forall (R : COrdField) (x : R) n,
 0 [<=] x -> 1[+]nring n[*]x [<=] (1[+]x) [^]n.




Lemma power_big : forall x y : IR, 0 [<=] x -> 1 [<] y -> {N : N | x [<=] y[^]N}.









Lemma qi_yields_zero : forall q : IR,
 0 [<=] q -> q [<] 1 -> forall e, 0 [<] e -> {N : N | q[^]N [<=] e}.
























Lemma qi_lim_zero : forall q : IR, 0 [<=] q -> q [<] 1 -> SeqLimit (fun i => q[^]i) 0.









End Properties_of_Exponentiation.

IR has characteristic zero


Lemma char0_IR : Char0 IR.

Lemma poly_apzero_IR : forall f : cpoly_cring IR, f [#] 0 -> {c : IR | f ! c [#] 0}.

Lemma poly_IR_extensional : forall p q : cpoly_cring IR, (forall x, p ! x [=] q ! x) -> p [=] q.