~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

<code class="keyword">Definition</code> <a name="D_x"></a>D_x (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (y x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop := D x /\ y <> x.

<code class="keyword">Definition</code> <a name="continue_in"></a>continue_in (f:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop :=

<a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> f (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (f x0) x0.

<code class="keyword">Definition</code> <a name="D_in"></a>D_in (f d:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop :=

<a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) / (x - x0)) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (d x0) x0.

<code class="keyword">Lemma</code> <a name="cont_deriv"></a>cont_deriv :

forall (f d:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> f d D x0 -> <a href="Coq.Reals.Rderiv.html#continue_in">continue_in</a> f D x0.

unfold continue_in in |- *; unfold D_in in |- *; unfold limit1_in in |- *;

unfold limit_in in |- *; unfold Rdiv in |- *; simpl in |- *;

intros; elim (H eps H0); clear H; intros; elim H;

clear H; intros; elim (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> (d x0) 0); intro.

split with (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> 1 x); split.

elim (<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> 1 x 0); intros a b; apply (b (<a href="Coq.Init.Logic.html#conj">conj</a> <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a> H)).

intros; elim H3; clear H3; intros;

generalize (let (H1, H2) := <a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> 1 x (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0) in H1);

unfold Rgt in |- *; intro; elim (H5 H4); clear H5;

intros; generalize (H1 x1 (<a href="Coq.Init.Logic.html#conj">conj</a> H3 H6)); clear H1;

intro; unfold D_x in H3; elim H3; intros.

rewrite H2 in H1; unfold R_dist in |- *; unfold R_dist in H1;

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0) < eps * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0)).

intro; unfold R_dist in H5;

generalize (<a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a> eps (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0)) 1 H0 H5);

rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; intro; apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with (r2:= eps * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0));

assumption.

rewrite (<a href="Coq.Reals.RIneq.html#Rminus_0_r">Rminus_0_r</a> ((f x1 - f x0) * / (x1 - x0))) in H1;

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a> in H1; cut (x1 - x0 <> 0).

intro; rewrite (<a href="Coq.Reals.Rbasic_fun.html#Rabs_Rinv">Rabs_Rinv</a> (x1 - x0) H9) in H1;

generalize

(<a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0)) (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0) * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0))

eps (<a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a> (x1 - x0) H9) H1); intro; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> in H10;

rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> in H10; rewrite <a href="Coq.Reals.Raxioms.html#Rinv_l">Rinv_l</a> in H10.

rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a> in H10; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>; assumption.

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_no_R0">Rabs_no_R0</a>; auto.

apply <a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a>; auto.

split with (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (/ 2) x) (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (2 * d x0))); split.

cut (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (/ 2) x > 0).

cut (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (2 * d x0) > 0).

intros; elim (<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (/ 2) x) (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (2 * d x0)) 0);

intros a b; apply (b (<a href="Coq.Init.Logic.html#conj">conj</a> H4 H3)).

apply <a href="Coq.Reals.RIneq.html#Rmult_gt_0_compat">Rmult_gt_0_compat</a>; auto.

unfold Rgt in |- *; apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>;

apply <a href="Coq.Reals.RIneq.html#Rmult_integral_contrapositive">Rmult_integral_contrapositive</a>; split.

discrR.

assumption.

elim (<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> (/ 2) x 0); intros a b; cut (0 < 2).

intro; generalize (<a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a> 2 H3); intro; fold (/ 2 > 0) in H4;

apply (b (<a href="Coq.Init.Logic.html#conj">conj</a> H4 H)).

fourier.

intros; elim H3; clear H3; intros;

generalize

(let (H1, H2) :=

<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (/ 2) x) (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (2 * d x0)) (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0) in

H1); unfold Rgt in |- *; intro; elim (H5 H4); clear H5;

intros; generalize (let (H1, H2) := <a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> (/ 2) x (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0) in H1);

unfold Rgt in |- *; intro; elim (H7 H5); clear H7;

intros; clear H4 H5; generalize (H1 x1 (<a href="Coq.Init.Logic.html#conj">conj</a> H3 H8));

clear H1; intro; unfold D_x in H3; elim H3; intros;

generalize (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> H5); clear H5; intro H5;

generalize (<a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a> x1 x0 H5); intro; generalize H1;

pattern (d x0) at 1 in |- *;

rewrite <- (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (d x0) in H2);

rewrite <- (<a href="Coq.Reals.Raxioms.html#Rinv_l">Rinv_l</a> (x1 - x0) H9); unfold R_dist in |- *;

unfold Rminus at 1 in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (f x1 - f x0) (/ (x1 - x0)));

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ (x1 - x0) * (x1 - x0)) (d x0));

rewrite <- (<a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a> (d x0) (/ (x1 - x0) * (x1 - x0)));

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (- d x0) (/ (x1 - x0) * (x1 - x0)));

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (/ (x1 - x0)) (x1 - x0) (- d x0));

100

rewrite <-

101

(<a href="Coq.Reals.Raxioms.html#Rmult_plus_distr_l">Rmult_plus_distr_l</a> (/ (x1 - x0)) (f x1 - f x0) ((x1 - x0) * - d x0))

102

; rewrite (<a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a> (/ (x1 - x0)) (f x1 - f x0 + (x1 - x0) * - d x0));

103

clear H1; intro;

104

generalize

105

(<a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0))

106

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ (x1 - x0)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0 + (x1 - x0) * - d x0)) eps

107

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a> (x1 - x0) H9) H1);

108

rewrite <-

109

(<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0)) (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ (x1 - x0)))

110

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0 + (x1 - x0) * - d x0)));

111

rewrite (<a href="Coq.Reals.Rbasic_fun.html#Rabs_Rinv">Rabs_Rinv</a> (x1 - x0) H9);

112

rewrite (<a href="Coq.Reals.RIneq.html#Rinv_r">Rinv_r</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0)) (<a href="Coq.Reals.Rbasic_fun.html#Rabs_no_R0">Rabs_no_R0</a> (x1 - x0) H9));

113

rewrite

114

(let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0 + (x1 - x0) * - d x0)) in H2)

115

; generalize (<a href="Coq.Reals.Rbasic_fun.html#Rabs_triang_inv">Rabs_triang_inv</a> (f x1 - f x0) ((x1 - x0) * d x0));

116

intro; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (x1 - x0) (- d x0));

117

rewrite (<a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a> (d x0) (x1 - x0));

118

fold (f x1 - f x0 - d x0 * (x1 - x0)) in |- *;

119

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (x1 - x0) (d x0)) in H10; clear H1;

120

intro;

121

generalize

122

(<a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0) - <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0)))

123

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0 - d x0 * (x1 - x0))) (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0) * eps) H10 H1);

124

clear H1; intro;

125

generalize

126

(<a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0)))

127

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0) - <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0))) (

128

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0) * eps) H1); unfold Rminus at 2 in |- *;

129

rewrite (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0)) (- <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0))));

130

rewrite <-

131

(<a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0))) (- <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0)))

132

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0))); rewrite (<a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0))));

133

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rplus_ne">Rplus_ne</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0)) in H2);

134

clear H1; intro; cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0)) + <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0) * eps < eps).

135

intro;

136

apply

137

(<a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f x1 - f x0))

138

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0)) + <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0) * eps) eps H1 H11).

139

clear H1 H5 H3 H10; generalize (<a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a> (d x0) H2); intro;

140

unfold Rgt in H0;

141

generalize (<a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a> eps (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0) (/ 2) H0 H7);

142

clear H7; intro;

143

generalize

144

(<a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)) (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0) (

145

eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (2 * d x0)) H1 H6); clear H6; intro;

146

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> eps (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x1 x0)) in H3; unfold R_dist in H3, H5;

147

rewrite <- (<a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a> (d x0) (x1 - x0)) in H5;

148

rewrite (<a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a> 2 (d x0)) in H5; cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2 <> 0).

149

intro; fold (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0) > 0) in H1;

150

rewrite

151

(<a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2) (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)) H6

152

(<a href="Coq.Reals.RIneq.html#Rlt_dichotomy_converse">Rlt_dichotomy_converse</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)) 0 (<a href="Coq.Init.Logic.html#or_intror">or_intror</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0) < 0) H1)))

153

in H5;

154

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)) (eps * (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2 * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)))) in H5;

155

rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> eps (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2) (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0))) in H5;

156

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2) (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0)) (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0))) in H5;

157

rewrite

158

(<a href="Coq.Reals.Raxioms.html#Rinv_l">Rinv_l</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0))

159

160

in H5; rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (eps * / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2) in H1) in H5;

161

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> 2 = 2).

162

intro; rewrite H7 in H5;

163

generalize

164

(<a href="Coq.Reals.RIneq.html#Rplus_lt_compat">Rplus_lt_compat</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (d x0 * (x1 - x0))) (eps * / 2)

165

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x1 - x0) * eps) (eps * / 2) H5 H3); intro;

166

rewrite <a href="Coq.Reals.Rlimit.html#eps2">eps2</a> in H10; assumption.

167

unfold Rabs in |- *; case (<a href="Coq.Reals.Rbasic_fun.html#Rcase_abs">Rcase_abs</a> 2); auto.

168

intro; cut (0 < 2).

169

intro; generalize (<a href="Coq.Reals.Raxioms.html#Rlt_asym">Rlt_asym</a> 0 2 H7); intro; elimtype <a href="Coq.Init.Logic.html#False">False</a>; auto.

170

fourier.

171

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_no_R0">Rabs_no_R0</a>.

172

discrR.

173

<code class="keyword">Qed</code>.

174

175

176

<code class="keyword">Lemma</code> <a name="Dconst"></a>Dconst :

177

forall (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (y x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>), <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => y) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0) D x0.

178

unfold D_in in |- *; intros; unfold limit1_in in |- *;

179

unfold limit_in in |- *; unfold Rdiv in |- *; intros;

180

simpl in |- *; split with eps; split; auto.

181

intros; rewrite (<a href="Coq.Reals.RIneq.html#Rminus_diag_eq">Rminus_diag_eq</a> y y (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> y)); rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>;

182

unfold R_dist in |- *; rewrite (<a href="Coq.Reals.RIneq.html#Rminus_diag_eq">Rminus_diag_eq</a> 0 0 (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> 0));

183

unfold Rabs in |- *; case (<a href="Coq.Reals.Rbasic_fun.html#Rcase_abs">Rcase_abs</a> 0); intro.

184

absurd (0 < 0); auto.

185

red in |- *; intro; apply (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> 0 H1).

186

unfold Rgt in H0; assumption.

187

<code class="keyword">Qed</code>.

188

189

190

<code class="keyword">Lemma</code> <a name="Dx"></a>Dx :

191

forall (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>), <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 1) D x0.

192

unfold D_in in |- *; unfold Rdiv in |- *; intros; unfold limit1_in in |- *;

193

unfold limit_in in |- *; intros; simpl in |- *; split with eps;

194

split; auto.

195

intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros;

196

rewrite (<a href="Coq.Reals.RIneq.html#Rinv_r">Rinv_r</a> (x - x0) (<a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a> x x0 (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> H3)));

197

unfold R_dist in |- *; rewrite (<a href="Coq.Reals.RIneq.html#Rminus_diag_eq">Rminus_diag_eq</a> 1 1 (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> 1));

198

unfold Rabs in |- *; case (<a href="Coq.Reals.Rbasic_fun.html#Rcase_abs">Rcase_abs</a> 0); intro.

199

absurd (0 < 0); auto.

200

red in |- *; intro; apply (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> 0 r).

201

unfold Rgt in H; assumption.

202

<code class="keyword">Qed</code>.

203

204

205

<code class="keyword">Lemma</code> <a name="Dadd"></a>Dadd :

206

forall (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (df dg f g:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

207

208

209

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => f x + g x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => df x + dg x) D x0.

210

unfold D_in in |- *; intros;

211

generalize

212

(<a href="Coq.Reals.Rlimit.html#limit_plus">limit_plus</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0))

213

(fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (g x - g x0) * / (x - x0)) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (

214

df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in in |- *;

215

unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0);

216

clear H; intros; elim H; clear H; intros; split with x;

217

split; auto; intros; generalize (H1 x1 H2); clear H1;

218

intro; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (f x1 - f x0) (/ (x1 - x0))) in H1;

219

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (g x1 - g x0) (/ (x1 - x0))) in H1;

220

rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_plus_distr_l">Rmult_plus_distr_l</a> (/ (x1 - x0)) (f x1 - f x0) (g x1 - g x0))

221

in H1;

222

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ (x1 - x0)) (f x1 - f x0 + (g x1 - g x0))) in H1;

223

cut (f x1 - f x0 + (g x1 - g x0) = f x1 + g x1 - (f x0 + g x0)).

224

intro; rewrite H3 in H1; assumption.

225

ring.

226

<code class="keyword">Qed</code>.

227

228

229

<code class="keyword">Lemma</code> <a name="Dmult"></a>Dmult :

230

231

232

233

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => f x * g x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => df x * g x + f x * dg x) D x0.

234

intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0;

235

generalize (<a href="Coq.Reals.Rderiv.html#cont_deriv">cont_deriv</a> f df D x0 H1); unfold continue_in in |- *;

236

intro;

237

generalize

238

(<a href="Coq.Reals.Rlimit.html#limit_mul">limit_mul</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (g x - g x0) * / (x - x0)) (

239

fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => f x) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (dg x0) (f x0) x0 H0 H3);

240

intro; cut (<a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => g x0) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (g x0) x0).

241

intro;

242

generalize

243

(<a href="Coq.Reals.Rlimit.html#limit_mul">limit_mul</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0)) (

244

fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => g x0) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (df x0) (g x0) x0 H H5);

245

clear H H0 H1 H2 H3 H5; intro;

246

generalize

247

(<a href="Coq.Reals.Rlimit.html#limit_plus">limit_plus</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0) * g x0)

248

(fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (g x - g x0) * / (x - x0) * f x) (

249

<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4);

250

clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H;

251

simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *;

252

simpl in |- *; intros; elim (H eps H0); clear H; intros;

253

elim H; clear H; intros; split with x; split; auto;

254

intros; generalize (H1 x1 H2); clear H1; intro;

255

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (f x1 - f x0) (/ (x1 - x0))) in H1;

256

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (g x1 - g x0) (/ (x1 - x0))) in H1;

257

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (/ (x1 - x0)) (f x1 - f x0) (g x0)) in H1;

258

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (/ (x1 - x0)) (g x1 - g x0) (f x1)) in H1;

259

rewrite <-

260

(<a href="Coq.Reals.Raxioms.html#Rmult_plus_distr_l">Rmult_plus_distr_l</a> (/ (x1 - x0)) ((f x1 - f x0) * g x0)

261

((g x1 - g x0) * f x1)) in H1;

262

rewrite

263

(<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ (x1 - x0)) ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1))

264

in H1; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (dg x0) (f x0)) in H1;

265

cut

266

((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0).

267

intro; rewrite H3 in H1; assumption.

268

ring.

269

unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;

270

split with eps; split; auto; intros; elim (<a href="Coq.Reals.Rfunctions.html#R_dist_refl">R_dist_refl</a> (g x0) (g x0));

271

intros a b; rewrite (b (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> (g x0))); unfold Rgt in H;

272

assumption.

273

<code class="keyword">Qed</code>.

274

275

276

<code class="keyword">Lemma</code> <a name="Dmult_const"></a>Dmult_const :

277

forall (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (f df:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x0 a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

278

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> f df D x0 -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => a * f x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => a * df x) D x0.

279

intros;

280

generalize (<a href="Coq.Reals.Rderiv.html#Dmult">Dmult</a> D (fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0) df (fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => a) f x0 (<a href="Coq.Reals.Rderiv.html#Dconst">Dconst</a> D a x0) H);

281

unfold D_in in |- *; intros; rewrite (<a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a> (f x0)) in H0;

282

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rplus_ne">Rplus_ne</a> (a * df x0) in H2) in H0;

283

assumption.

284

<code class="keyword">Qed</code>.

285

286

287

<code class="keyword">Lemma</code> <a name="Dopp"></a>Dopp :

288

forall (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (f df:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

289

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> f df D x0 -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => - f x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => - df x) D x0.

290

intros; generalize (<a href="Coq.Reals.Rderiv.html#Dmult_const">Dmult_const</a> D f df x0 (-1) H); unfold D_in in |- *;

291

unfold limit1_in in |- *; unfold limit_in in |- *;

292

intros; generalize (H0 eps H1); clear H0; intro; elim H0;

293

clear H0; intros; elim H0; clear H0; simpl in |- *;

294

intros; split with x; split; auto.

295

intros; generalize (H2 x1 H3); clear H2; intro;

296

rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a> in H2;

297

rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a> in H2;

298

rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a> in H2;

299

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (f x1) in H2) in H2;

300

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (f x0) in H2) in H2;

301

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (df x0) in H2) in H2;

302

assumption.

303

<code class="keyword">Qed</code>.

304

305

306

<code class="keyword">Lemma</code> <a name="Dminus"></a>Dminus :

307

308

309

310

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => f x - g x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => df x - dg x) D x0.

311

unfold Rminus in |- *; intros; generalize (<a href="Coq.Reals.Rderiv.html#Dopp">Dopp</a> D g dg x0 H0); intro;

312

apply (<a href="Coq.Reals.Rderiv.html#Dadd">Dadd</a> D df (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => - dg x) f (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => - g x) x0);

313

assumption.

314

<code class="keyword">Qed</code>.

315

316

317

<code class="keyword">Lemma</code> <a name="Dx_pow_n"></a>Dx_pow_n :

318

forall (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

319

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x ^ n) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Raxioms.html#INR">INR</a> n * x ^ (n - 1)) D x0.

320

simple induction n; intros.

321

simpl in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>; apply <a href="Coq.Reals.Rderiv.html#Dconst">Dconst</a>.

322

intros; cut (n0 = (<a href="Coq.Init.Datatypes.html#S">S</a> n0 - 1)%nat);

323

[ intro a; rewrite <- a; clear a | simpl in |- *; apply minus_n_O ].

324

generalize

325

(<a href="Coq.Reals.Rderiv.html#Dmult">Dmult</a> D (fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 1) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Raxioms.html#INR">INR</a> n0 * x ^ (n0 - 1)) (

326

fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x ^ n0) x0 (<a href="Coq.Reals.Rderiv.html#Dx">Dx</a> D x0) (

327

H D x0)); unfold D_in in |- *; unfold limit1_in in |- *;

328

unfold limit_in in |- *; simpl in |- *; intros; elim (H0 eps H1);

329

clear H0; intros; elim H0; clear H0; intros; split with x;

330

split; auto.

331

intros; generalize (H2 x1 H3); clear H2 H3; intro;

332

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (x0 ^ n0) in H2) in H2;

333

rewrite (<a href="Coq.Reals.Rfunctions.html#tech_pow_Rmult">tech_pow_Rmult</a> x1 n0) in H2; rewrite (<a href="Coq.Reals.Rfunctions.html#tech_pow_Rmult">tech_pow_Rmult</a> x0 n0) in H2;

334

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (<a href="Coq.Reals.Raxioms.html#INR">INR</a> n0) (x0 ^ (n0 - 1))) in H2;

335

rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> x0 (x0 ^ (n0 - 1)) (<a href="Coq.Reals.Raxioms.html#INR">INR</a> n0)) in H2;

336

rewrite (<a href="Coq.Reals.Rfunctions.html#tech_pow_Rmult">tech_pow_Rmult</a> x0 (n0 - 1)) in H2; elim (<a href="Coq.Logic.Classical_Prop.html#classic">classic</a> (n0 = 0%nat));

337

intro cond.

338

rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *;

339

cut (1 + x0 * 1 * 0 = 1 * 1);

340

[ intro A; rewrite A in H2; assumption | ring ].

341

cut (n0 <> 0%nat -> <a href="Coq.Init.Datatypes.html#S">S</a> (n0 - 1) = n0); [ intro | omega ];

342

rewrite (H3 cond) in H2; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (x0 ^ n0) (<a href="Coq.Reals.Raxioms.html#INR">INR</a> n0)) in H2;

343

rewrite (<a href="Coq.Reals.Rfunctions.html#tech_pow_Rplus">tech_pow_Rplus</a> x0 n0 n0) in H2; assumption.

344

<code class="keyword">Qed</code>.

345

346

347

<code class="keyword">Lemma</code> <a name="Dcomp"></a>Dcomp :

348

forall (Df Dg:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (df dg f g:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

349

350

351

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => g (f x)) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => df x * dg (f x)) (<a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> Df Dg f) x0.

352

intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in in |- *;

353

unfold Rdiv in |- *; intros;

354

generalize

355

(<a href="Coq.Reals.Rlimit.html#limit_comp">limit_comp</a> f (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (g x - g (f x0)) * / (x - f x0)) (

356

<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Df x0) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Dg (f x0)) (f x0) (dg (f x0)) x0);

357

intro; generalize (<a href="Coq.Reals.Rderiv.html#cont_deriv">cont_deriv</a> f df Df x0 H); intro;

358

unfold continue_in in H4; generalize (H3 H4 H2); clear H3;

359

intro;

360

generalize

361

(<a href="Coq.Reals.Rlimit.html#limit_mul">limit_mul</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (g (f x) - g (f x0)) * / (f x - f x0))

362

(fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0))

363

(<a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Df x0) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Dg (f x0)) f) (dg (f x0)) (

364

df x0) x0 H3); intro;

365

cut

366

(<a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0))

367

(<a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Df x0) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Dg (f x0)) f) (df x0) x0).

368

intro; generalize (H5 H6); clear H5; intro;

369

generalize

370

(<a href="Coq.Reals.Rlimit.html#limit_mul">limit_mul</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (f x - f x0) * / (x - x0)) (

371

fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => dg (f x0)) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Df x0) (df x0) (dg (f x0)) x0 H1

372

(<a href="Coq.Reals.Rlimit.html#limit_free">limit_free</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => dg (f x0)) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> Df x0) x0 x0));

373

intro; unfold limit1_in in |- *; unfold limit_in in |- *;

374

simpl in |- *; unfold limit1_in in H5, H7; unfold limit_in in H5, H7;

375

simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8);

376

clear H5 H7; intros; elim H5; elim H7; clear H5 H7;

377

intros; split with (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> x x1); split.

378

elim (<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> x x1 0); intros a b; apply (b (<a href="Coq.Init.Logic.html#conj">conj</a> H9 H5)); clear a b.

379

intros; elim H11; clear H11; intros; elim (<a href="Coq.Reals.Rbasic_fun.html#Rmin_Rgt">Rmin_Rgt</a> x x1 (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x2 x0));

380

intros a b; clear b; unfold Rgt in a; elim (a H12);

381

clear H5 a; intros; unfold D_x, Dgf in H11, H7, H10;

382

clear H12; elim (<a href="Coq.Logic.Classical_Prop.html#classic">classic</a> (f x2 = f x0)); intro.

383

elim H11; clear H11; intros; elim H11; clear H11; intros;

384

generalize (H10 x2 (<a href="Coq.Init.Logic.html#conj">conj</a> (<a href="Coq.Init.Logic.html#conj">conj</a> H11 H14) H5)); intro;

385

rewrite (<a href="Coq.Reals.RIneq.html#Rminus_diag_eq">Rminus_diag_eq</a> (f x2) (f x0) H12) in H16;

386

rewrite (<a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a> (/ (x2 - x0))) in H16;

387

rewrite (<a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a> (dg (f x0))) in H16; rewrite H12;

388

rewrite (<a href="Coq.Reals.RIneq.html#Rminus_diag_eq">Rminus_diag_eq</a> (g (f x0)) (g (f x0)) (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> (g (f x0))));

389

rewrite (<a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a> (/ (x2 - x0))); assumption.

390

clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros;

391

cut

392

(((Df x2 /\ x0 <> x2) /\ Dg (f x2) /\ f x0 <> f x2) /\ <a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> x2 x0 < x1);

393

auto; intro; generalize (H7 x2 H14); intro;

394

generalize (<a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a> (f x2) (f x0) H12); intro;

395

rewrite

396

(<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (g (f x2) - g (f x0)) (/ (f x2 - f x0))

397

((f x2 - f x0) * / (x2 - x0))) in H15;

398

rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a> (/ (f x2 - f x0)) (f x2 - f x0) (/ (x2 - x0)))

399

in H15; rewrite (<a href="Coq.Reals.Raxioms.html#Rinv_l">Rinv_l</a> (f x2 - f x0) H16) in H15;

400

rewrite (let (H1, H2) := <a href="Coq.Reals.RIneq.html#Rmult_ne">Rmult_ne</a> (/ (x2 - x0)) in H2) in H15;

401

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (df x0) (dg (f x0))); assumption.

402

clear H5 H3 H4 H2; unfold limit1_in in |- *; unfold limit_in in |- *;

403

simpl in |- *; unfold limit1_in in H1; unfold limit_in in H1;

404

simpl in H1; intros; elim (H1 eps H2); clear H1; intros;

405

elim H1; clear H1; intros; split with x; split; auto;

406

intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4;

407

intros; elim H4; clear H4; intros; exact (H3 x1 (<a href="Coq.Init.Logic.html#conj">conj</a> H4 H5)).

408

<code class="keyword">Qed</code>.

409

410

411

<code class="keyword">Lemma</code> <a name="D_pow_n"></a>D_pow_n :

412

forall (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (D:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) (expr dexpr:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>),

413

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> expr dexpr D x0 ->

414

<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => expr x ^ n)

415

(fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Raxioms.html#INR">INR</a> n * expr x ^ (n - 1) * dexpr x) (

416

<a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> D D expr) x0.

417

intros n D x0 expr dexpr H;

418

generalize

419

(<a href="Coq.Reals.Rderiv.html#Dcomp">Dcomp</a> D D dexpr (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Raxioms.html#INR">INR</a> n * x ^ (n - 1)) expr (

420

fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x ^ n) x0 H (<a href="Coq.Reals.Rderiv.html#Dx_pow_n">Dx_pow_n</a> n D (expr x0)));

421

intro; unfold D_in in |- *; unfold limit1_in in |- *;

422

unfold limit_in in |- *; simpl in |- *; intros; unfold D_in in H0;

423

unfold limit1_in in H0; unfold limit_in in H0; simpl in H0;

424

elim (H0 eps H1); clear H0; intros; elim H0; clear H0;

425

intros; split with x; split; intros; auto.

426

cut

427

(dexpr x0 * (<a href="Coq.Reals.Raxioms.html#INR">INR</a> n * expr x0 ^ (n - 1)) =

428

<a href="Coq.Reals.Raxioms.html#INR">INR</a> n * expr x0 ^ (n - 1) * dexpr x0);

429

[ intro Rew; rewrite <- Rew; exact (H2 x1 H3) | ring ].

430

<code class="keyword">Qed</code>.

431

</code>

432

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

433

</body>

434

</html>

b'\\ No newline at end of file'

Older »