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
|
Require Import Reals.
Axiom y : R -> R.
Axiom d_y : derivable y.
Axiom n_y : forall x : R, y x <> 0%R.
Axiom dy_0 : derive_pt y 0 (d_y 0%R) = 1%R.
Lemma essai0 : continuity_pt (fun x : R => ((x + 2) / y x + x / y x)%R) 0.
assert (H := d_y).
assert (H0 := n_y).
reg.
Qed.
Lemma essai1 : derivable_pt (fun x : R => (/ 2 * sin x)%R) 1.
reg.
Qed.
Lemma essai2 : continuity (fun x : R => (Rsqr x * cos (x * x) + x)%R).
reg.
Qed.
Lemma essai3 : derivable_pt (fun x : R => (x * (Rsqr x + 3))%R) 0.
reg.
Qed.
Lemma essai4 : derivable (fun x : R => ((x + x) * sin x)%R).
reg.
Qed.
Lemma essai5 : derivable (fun x : R => (1 + sin (2 * x + 3) * cos (cos x))%R).
reg.
Qed.
Lemma essai6 : derivable (fun x : R => cos (x + 3)).
reg.
Qed.
Lemma essai7 :
derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1.
reg.
apply Rlt_0_1.
red; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
assumption.
Qed.
Lemma essai8 : derivable_pt (fun x : R => sqrt (Rsqr x + sin x + 1)) 0.
reg.
rewrite sin_0.
rewrite Rsqr_0.
replace (0 + 0 + 1)%R with 1%R; [ apply Rlt_0_1 | ring ].
Qed.
Lemma essai9 : derivable_pt (id + sin) 1.
reg.
Qed.
Lemma essai10 : derivable_pt (fun x : R => (x + 2)%R) 0.
reg.
Qed.
Lemma essai11 : derive_pt (fun x : R => (x + 2)%R) 0 essai10 = 1%R.
reg.
Qed.
Lemma essai12 : derivable (fun x : R => (x + Rsqr (x + 2))%R).
reg.
Qed.
Lemma essai13 :
derive_pt (fun x : R => (x + Rsqr (x + 2))%R) 0 (essai12 0%R) = 5%R.
reg.
Qed.
Lemma essai14 : derivable_pt (fun x : R => (2 * x + x)%R) 2.
reg.
Qed.
Lemma essai15 : derive_pt (fun x : R => (2 * x + x)%R) 2 essai14 = 3%R.
reg.
Qed.
Lemma essai16 : derivable_pt (fun x : R => (x + sin x)%R) 0.
reg.
Qed.
Lemma essai17 : derive_pt (fun x : R => (x + sin x)%R) 0 essai16 = 2%R.
reg.
rewrite cos_0.
reflexivity.
Qed.
Lemma essai18 : derivable_pt (fun x : R => (x + y x)%R) 0.
assert (H := d_y).
reg.
Qed.
Lemma essai19 : derive_pt (fun x : R => (x + y x)%R) 0 essai18 = 2%R.
assert (H := dy_0).
assert (H0 := d_y).
reg.
Qed.
Axiom z : R -> R.
Axiom d_z : derivable z.
Lemma essai20 : derivable_pt (fun x : R => z (y x)) 0.
reg.
apply d_y.
apply d_z.
Qed.
Lemma essai21 : derive_pt (fun x : R => z (y x)) 0 essai20 = 1%R.
assert (H := dy_0).
reg.
Abort.
Lemma essai22 : derivable (fun x : R => (sin (z x) + Rsqr (z x) / y x)%R).
assert (H := d_y).
reg.
apply n_y.
apply d_z.
Qed.
(* Pour tester la continuite de sqrt en 0 *)
Lemma essai23 :
continuity_pt
(fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1.
reg.
left; apply Rlt_0_1.
right; unfold Rminus; rewrite Rplus_opp_r; reflexivity.
Qed.
Lemma essai24 :
derivable (fun x : R => (sqrt (x * x + 2 * x + 2) + Rabs (x * x + 1))%R).
reg.
replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R.
apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ].
unfold Rsqr; ring.
red; intro; cut (0 < x * x + 1)%R.
intro; rewrite H in H0; elim (Rlt_irrefl _ H0).
apply Rplus_le_lt_0_compat;
[ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ]
| apply Rlt_0_1 ].
Qed.
|
