1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Ranalysis2.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*)
Require Rbase.
Require Rfunctions.
Require Ranalysis1.
V7only [Import R_scope.]. Open Local Scope R_scope.
(**********)
Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``.
Intros; Unfold Rdiv Rminus Rsqr.
Repeat Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_Rplus_distr; Repeat Rewrite Rinv_Rmult; Try Assumption.
Replace ``l1*(f2 x)*(/(f2 x)*/(f2 x))`` with ``l1*/(f2 x)*((f2 x)*/(f2 x))``; [Idtac | Ring].
Replace ``l1*(/(f2 x)*/(f2 (x+h)))*(f2 x)`` with ``l1*/(f2 (x+h))*((f2 x)*/(f2 x))``; [Idtac | Ring].
Replace ``l1*(/(f2 x)*/(f2 (x+h)))* -(f2 (x+h))`` with ``-(l1*/(f2 x)*((f2 (x+h))*/(f2 (x+h))))``; [Idtac | Ring].
Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*((f2 (x+h))*/h)`` with ``(f1 x)*/(f2 x)*/h*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring].
Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*( -(f2 x)*/h)`` with ``-((f1 x)*/(f2 (x+h))*/h*((f2 x)*/(f2 x)))``; [Idtac | Ring].
Replace ``(l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))*(f2 (x+h)))`` with ``l2*(f1 x)*/(f2 x)*/(f2 x)*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring].
Replace ``l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))* -(f2 x)`` with ``-(l2*(f1 x)*/(f2 x)*/(f2 (x+h))*((f2 x)*/(f2 x)))``; [Idtac | Ring].
Repeat Rewrite <- Rinv_r_sym; Try Assumption Orelse Ring.
Apply prod_neq_R0; Assumption.
Qed.
Lemma Rmin_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0 < (Rmin x y)``.
Intros; Unfold Rmin.
Case (total_order_Rle x y); Intro; Assumption.
Qed.
Lemma maj_term1 : (x,h,eps,l1,alp_f2:R;eps_f2,alp_f1d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f1d``->``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < (Rabsolu ((eps*(f2 x))/8))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f1d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) < eps/4``.
Intros.
Assert H7 := (H3 h H6).
Assert H8 := (H2 h H4 H5).
Apply Rle_lt_trans with ``2/(Rabsolu (f2 x))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))``.
Rewrite Rabsolu_mult.
Apply Rle_monotony_r.
Apply Rabsolu_pos.
Rewrite Rabsolu_Rinv; [Left; Exact H7 | Assumption].
Apply Rlt_le_trans with ``2/(Rabsolu (f2 x))*(Rabsolu ((eps*(f2 x))/8))``.
Apply Rlt_monotony.
Unfold Rdiv; Apply Rmult_lt_pos; [Sup0 | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption].
Exact H8.
Right; Unfold Rdiv.
Repeat Rewrite Rabsolu_mult.
Rewrite Rabsolu_Rinv; DiscrR.
Replace ``(Rabsolu 8)`` with ``8``.
Replace ``8`` with ``2*4``; [Idtac | Ring].
Rewrite Rinv_Rmult; [Idtac | DiscrR | DiscrR].
Replace ``2*/(Rabsolu (f2 x))*((Rabsolu eps)*(Rabsolu (f2 x))*(/2*/4))`` with ``(Rabsolu eps)*/4*(2*/2)*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))``; [Idtac | Ring].
Replace (Rabsolu eps) with eps.
Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
Ring.
Symmetry; Apply Rabsolu_right; Left; Assumption.
Symmetry; Apply Rabsolu_right; Left; Sup.
Qed.
Lemma maj_term2 : (x,h,eps,l1,alp_f2,alp_f2t2:R;eps_f2:posreal;f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2t2``->``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``)-> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2t2`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``l1<>0`` -> ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) < eps/4``.
Intros.
Assert H8 := (H3 h H6).
Assert H9 := (H2 h H5).
Apply Rle_lt_trans with ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``.
Rewrite Rabsolu_mult; Apply Rle_monotony.
Apply Rabsolu_pos.
Rewrite <- (Rabsolu_Ropp ``(f2 x)-(f2 (x+h))``); Rewrite Ropp_distr2.
Left; Apply H9.
Apply Rlt_le_trans with ``(Rabsolu (2*l1/((f2 x)*(f2 x))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``.
Apply Rlt_monotony_r.
Apply Rabsolu_pos_lt.
Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption Orelse DiscrR.
Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H).
Apply Rinv_neq_R0; Apply prod_neq_R0; Try Assumption Orelse DiscrR.
Unfold Rdiv.
Repeat Rewrite Rinv_Rmult; Try Assumption.
Repeat Rewrite Rabsolu_mult.
Replace ``(Rabsolu 2)`` with ``2``.
Rewrite (Rmult_sym ``2``).
Replace ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring].
Repeat Apply Rlt_monotony.
Apply Rabsolu_pos_lt; Assumption.
Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption.
Repeat Rewrite Rabsolu_Rinv; Try Assumption.
Rewrite <- (Rmult_sym ``2``).
Unfold Rdiv in H8; Exact H8.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Right.
Unfold Rsqr Rdiv.
Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Repeat Rewrite Rabsolu_mult.
Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
Replace (Rabsolu eps) with eps.
Replace ``(Rabsolu (8))`` with ``8``.
Replace ``(Rabsolu 2)`` with ``2``.
Replace ``8`` with ``4*2``; [Idtac | Ring].
Rewrite Rinv_Rmult; DiscrR.
Replace ``2*((Rabsolu l1)*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*(eps*((Rabsolu (f2 x))*(Rabsolu (f2 x)))*(/4*/2*/(Rabsolu l1)))`` with ``eps*/4*((Rabsolu l1)*/(Rabsolu l1))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring].
Repeat Rewrite <- Rinv_r_sym; Try (Apply Rabsolu_no_R0; Assumption) Orelse DiscrR.
Ring.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Symmetry; Apply Rabsolu_right; Left; Sup.
Symmetry; Apply Rabsolu_right; Left; Assumption.
Qed.
Lemma maj_term3 : (x,h,eps,l2,alp_f2:R;eps_f2,alp_f2d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f2d``->``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < (Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) < eps/4``.
Intros.
Assert H8 := (H2 h H4 H5).
Assert H9 := (H3 h H6).
Apply Rle_lt_trans with ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``.
Rewrite Rabsolu_mult.
Apply Rle_monotony.
Apply Rabsolu_pos.
Left; Apply H8.
Apply Rlt_le_trans with ``(Rabsolu (2*(f1 x)/((f2 x)*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``.
Apply Rlt_monotony_r.
Apply Rabsolu_pos_lt.
Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption.
Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H).
Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption.
Unfold Rdiv.
Repeat Rewrite Rinv_Rmult; Try Assumption.
Repeat Rewrite Rabsolu_mult.
Replace ``(Rabsolu 2)`` with ``2``.
Rewrite (Rmult_sym ``2``).
Replace ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring].
Repeat Apply Rlt_monotony.
Apply Rabsolu_pos_lt; Assumption.
Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption.
Repeat Rewrite Rabsolu_Rinv; Assumption Orelse Idtac.
Rewrite <- (Rmult_sym ``2``).
Unfold Rdiv in H9; Exact H9.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Right.
Unfold Rsqr Rdiv.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Repeat Rewrite Rabsolu_mult.
Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
Replace (Rabsolu eps) with eps.
Replace ``(Rabsolu (8))`` with ``8``.
Replace ``(Rabsolu 2)`` with ``2``.
Replace ``8`` with ``4*2``; [Idtac | Ring].
Rewrite Rinv_Rmult; DiscrR.
Replace ``2*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))))`` with ``eps*/4*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*(2*/2)``; [Idtac | Ring].
Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
Ring.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Symmetry; Apply Rabsolu_right; Left; Sup.
Symmetry; Apply Rabsolu_right; Left; Assumption.
Qed.
Lemma maj_term4 : (x,h,eps,l2,alp_f2,alp_f2c:R;eps_f2:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2c`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``l2<>0`` -> ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x)))) < eps/4``.
Intros.
Assert H9 := (H2 h H5).
Assert H10 := (H3 h H6).
Apply Rle_lt_trans with ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``.
Rewrite Rabsolu_mult.
Apply Rle_monotony.
Apply Rabsolu_pos.
Left; Apply H9.
Apply Rlt_le_trans with ``(Rabsolu (2*l2*(f1 x)/((Rsqr (f2 x))*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``.
Apply Rlt_monotony_r.
Apply Rabsolu_pos_lt.
Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Assumption Orelse Idtac.
Red; Intro H11; Rewrite H11 in H; Elim (Rlt_antirefl ? H).
Apply Rinv_neq_R0; Apply prod_neq_R0.
Apply prod_neq_R0.
DiscrR.
Assumption.
Assumption.
Unfold Rdiv.
Repeat Rewrite Rinv_Rmult; Try Assumption Orelse (Unfold Rsqr; Apply prod_neq_R0; Assumption).
Repeat Rewrite Rabsolu_mult.
Replace ``(Rabsolu 2)`` with ``2``.
Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 x)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*((Rabsolu (/(f2 x)))*2)))``; [Idtac | Ring].
Replace ``(Rabsolu l2)*(Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*(((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))))``; [Idtac | Ring].
Repeat Apply Rlt_monotony.
Apply Rabsolu_pos_lt; Assumption.
Apply Rabsolu_pos_lt; Assumption.
Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Unfold Rsqr; Apply prod_neq_R0; Assumption.
Repeat Rewrite Rabsolu_Rinv; [Idtac | Assumption | Assumption].
Rewrite <- (Rmult_sym ``2``).
Unfold Rdiv in H10; Exact H10.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Right; Unfold Rsqr Rdiv.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR.
Repeat Rewrite Rabsolu_mult.
Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR.
Replace (Rabsolu eps) with eps.
Replace ``(Rabsolu (8))`` with ``8``.
Replace ``(Rabsolu 2)`` with ``2``.
Replace ``8`` with ``4*2``; [Idtac | Ring].
Rewrite Rinv_Rmult; DiscrR.
Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))*/(Rabsolu l2)))`` with ``eps*/4*((Rabsolu l2)*/(Rabsolu l2))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring].
Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption).
Ring.
Symmetry; Apply Rabsolu_right; Left; Sup0.
Symmetry; Apply Rabsolu_right; Left; Sup.
Symmetry; Apply Rabsolu_right; Left; Assumption.
Apply prod_neq_R0; Assumption Orelse DiscrR.
Apply prod_neq_R0; Assumption.
Qed.
Lemma D_x_no_cond : (x,a:R) ``a<>0`` -> (D_x no_cond x ``x+a``).
Intros.
Unfold D_x no_cond.
Split.
Trivial.
Apply Rminus_not_eq.
Unfold Rminus.
Rewrite Ropp_distr1.
Rewrite <- Rplus_assoc.
Rewrite Rplus_Ropp_r.
Rewrite Rplus_Ol.
Apply Ropp_neq; Assumption.
Qed.
Lemma Rabsolu_4 : (a,b,c,d:R) ``(Rabsolu (a+b+c+d)) <= (Rabsolu a) + (Rabsolu b) + (Rabsolu c) + (Rabsolu d)``.
Intros.
Apply Rle_trans with ``(Rabsolu (a+b)) + (Rabsolu (c+d))``.
Replace ``a+b+c+d`` with ``(a+b)+(c+d)``; [Apply Rabsolu_triang | Ring].
Apply Rle_trans with ``(Rabsolu a) + (Rabsolu b) + (Rabsolu (c+d))``.
Apply Rle_compatibility_r.
Apply Rabsolu_triang.
Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility.
Apply Rabsolu_triang.
Qed.
Lemma Rlt_4 : (a,b,c,d,e,f,g,h:R) ``a < b`` -> ``c < d`` -> ``e < f `` -> ``g < h`` -> ``a+c+e+g < b+d+f+h``.
Intros; Apply Rlt_trans with ``b+c+e+g``.
Repeat Apply Rlt_compatibility_r; Assumption.
Repeat Rewrite Rplus_assoc; Apply Rlt_compatibility.
Apply Rlt_trans with ``d+e+g``.
Rewrite Rplus_assoc; Apply Rlt_compatibility_r; Assumption.
Rewrite Rplus_assoc; Apply Rlt_compatibility; Apply Rlt_trans with ``f+g``.
Apply Rlt_compatibility_r; Assumption.
Apply Rlt_compatibility; Assumption.
Qed.
Lemma Rmin_2 : (a,b,c:R) ``a < b`` -> ``a < c`` -> ``a < (Rmin b c)``.
Intros; Unfold Rmin; Case (total_order_Rle b c); Intro; Assumption.
Qed.
Lemma quadruple : (x:R) ``4*x == x + x + x + x``.
Intro; Ring.
Qed.
Lemma quadruple_var : (x:R) `` x == x/4 + x/4 + x/4 + x/4``.
Intro; Rewrite <- quadruple.
Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m; DiscrR.
Reflexivity.
Qed.
(**********)
Lemma continuous_neq_0 : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (EXT eps : posreal | (h:R) ``(Rabsolu h) < eps`` -> ~``(f (x0+h))==0``).
Intros; Unfold continuity_pt in H; Unfold continue_in in H; Unfold limit1_in in H; Unfold limit_in in H; Elim (H ``(Rabsolu ((f x0)/2))``).
Intros; Elim H1; Intros.
Exists (mkposreal x H2).
Intros; Assert H5 := (H3 ``x0+h``).
Cut ``(dist R_met (x0+h) x0) < x`` -> ``(dist R_met (f (x0+h)) (f x0)) < (Rabsolu ((f x0)/2))``.
Unfold dist; Simpl; Unfold R_dist; Replace ``x0+h-x0`` with h.
Intros; Assert H7 := (H6 H4).
Red; Intro.
Rewrite H8 in H7; Unfold Rminus in H7; Rewrite Rplus_Ol in H7; Rewrite Rabsolu_Ropp in H7; Unfold Rdiv in H7; Rewrite Rabsolu_mult in H7; Pattern 1 ``(Rabsolu (f x0)) `` in H7; Rewrite <- Rmult_1r in H7.
Cut ``0<(Rabsolu (f x0))``.
Intro; Assert H10 := (Rlt_monotony_contra ? ? ? H9 H7).
Cut ``(Rabsolu (/2))==/2``.
Assert Hyp:``0<2``.
Sup0.
Intro; Rewrite H11 in H10; Assert H12 := (Rlt_monotony ``2`` ? ? Hyp H10); Rewrite Rmult_1r in H12; Rewrite <- Rinv_r_sym in H12; [Idtac | DiscrR].
Cut (Rlt (IZR `1`) (IZR `2`)).
Unfold IZR; Unfold INR convert; Simpl; Intro; Elim (Rlt_antirefl ``1`` (Rlt_trans ? ? ? H13 H12)).
Apply IZR_lt; Omega.
Unfold Rabsolu; Case (case_Rabsolu ``/2``); Intro.
Assert Hyp:``0<2``.
Sup0.
Assert H11 := (Rlt_monotony ``2`` ? ? Hyp r); Rewrite Rmult_Or in H11; Rewrite <- Rinv_r_sym in H11; [Idtac | DiscrR].
Elim (Rlt_antirefl ``0`` (Rlt_trans ? ? ? Rlt_R0_R1 H11)).
Reflexivity.
Apply (Rabsolu_pos_lt ? H0).
Ring.
Assert H6 := (Req_EM ``x0`` ``x0+h``); Elim H6; Intro.
Intro; Rewrite <- H7; Unfold dist R_met; Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt.
Unfold Rdiv; Apply prod_neq_R0; [Assumption | Apply Rinv_neq_R0; DiscrR].
Intro; Apply H5.
Split.
Unfold D_x no_cond.
Split; Trivial Orelse Assumption.
Assumption.
Change ``0 < (Rabsolu ((f x0)/2))``.
Apply Rabsolu_pos_lt; Unfold Rdiv; Apply prod_neq_R0.
Assumption.
Apply Rinv_neq_R0; DiscrR.
Qed.
|
