1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/reals/".
17 include "ordered_fields_ch0.ma".
19 record is_real (F:ordered_field_ch0) : Type
21 { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? n);
22 r_complete: is_complete F
25 record real: Type \def
26 { r_ordered_field_ch0:> ordered_field_ch0;
27 r_real_properties: is_real r_ordered_field_ch0
30 definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R.
32 elim (r_complete ? (r_real_properties R) ? H);
36 definition max_seq: ∀R:real.∀x,y:R. nat → R.
38 elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
40 | apply not_eq_sum_field_zero ;
44 | apply lt_zero_to_le_inv_zero
50 theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
54 exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
57 elim (to_cotransitive R (of_le R) R 0
58 (inv R (sum_field R (S N))
59 (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
60 (lt_zero_to_le_inv_zero R (S N)
61 (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
63 elim (to_cotransitive R (of_le R) R 0
64 (inv R (1+sum R (plus R) 0 1 m)
65 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
66 (lt_zero_to_le_inv_zero R (S m)
67 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
69 rewrite > (plus_comm ? x (-x));
70 rewrite > opp_inverse;
72 [ apply (le_zero_x_to_le_opp_x_zero R ?);
73 apply lt_zero_to_le_inv_zero
74 | apply lt_zero_to_le_inv_zero
78 [ apply (to_transitive ? ?
79 (of_total_order_relation ? ? R) ? 0 ?);
80 [ apply (le_zero_x_to_le_opp_x_zero R ?)
87 elim (to_cotransitive R (of_le R) R 0
88 (inv R (1+sum R (plus R) 0 1 m)
89 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
90 (lt_zero_to_le_inv_zero R (S m)
91 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
95 | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
98 rewrite > eq_opp_plus_plus_opp_opp in H1;
99 rewrite > eq_opp_opp_x_x in H1;
100 rewrite > plus_comm in H1;
101 apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?);
103 | apply lt_zero_to_le_inv_zero
107 rewrite > (plus_comm ? y (-y));
108 rewrite > opp_inverse;
111 | apply lt_zero_to_le_inv_zero
118 definition max: ∀R:real.R → R → R.
120 apply (lim R (max_seq R x y));
121 apply cauchy_max_seq.
124 definition abs \def λR:real.λx:R. max R x (-x).
127 ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g →
128 (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?.
138 -(inv R (sum_field R (S n))
139 (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))).
141 axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R).
143 lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
149 lemma abs_x_ge_O: \forall R: real. \forall x:R. 0 ≤ abs R x.
153 rewrite < technical1;
159 (to_cotransitive R (of_le R) R 0
160 (inv R (sum_field R (S n))
161 (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))) (x--x)
162 (lt_zero_to_le_inv_zero R (S n)
163 (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))));