1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Reals.Rpower</title>
8
<h1>Library Coq.Reals.Rpower</h1>
12
<code class="keyword">Require</code> <code class="keyword">Import</code> Rbase.<br/>
13
<code class="keyword">Require</code> <code class="keyword">Import</code> Rfunctions.<br/>
14
<code class="keyword">Require</code> <code class="keyword">Import</code> SeqSeries.<br/>
15
<code class="keyword">Require</code> <code class="keyword">Import</code> Rtrigo.<br/>
16
<code class="keyword">Require</code> <code class="keyword">Import</code> Ranalysis1.<br/>
17
<code class="keyword">Require</code> <code class="keyword">Import</code> Exp_prop.<br/>
18
<code class="keyword">Require</code> <code class="keyword">Import</code> Rsqrt_def.<br/>
19
<code class="keyword">Require</code> <code class="keyword">Import</code> R_sqrt.<br/>
20
<code class="keyword">Require</code> <code class="keyword">Import</code> MVT.<br/>
21
<code class="keyword">Require</code> <code class="keyword">Import</code> Ranalysis4. Open <code class="keyword">Local</code> Scope R_scope.<br/>
24
<code class="keyword">Lemma</code> <a name="P_Rmin"></a>P_Rmin : forall (P:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>), P x -> P y -> P (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> x y).<br/>
25
intros P x y H1 H2; unfold Rmin in |- *; case (<a href="Coq.Reals.RIneq.html#Rle_dec">Rle_dec</a> x y); intro;<br/>
26
assumption.<br/>
27
<code class="keyword">Qed</code>.<br/>
30
<code class="keyword">Lemma</code> <a name="exp_le_3"></a>exp_le_3 : <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 1 <= 3.<br/>
31
assert (exp_1 : <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 1 <> 0).<br/>
32
assert (H0:= <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a> 1); red in |- *; intro; rewrite H in H0;<br/>
33
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H0).<br/>
34
apply <a href="Coq.Reals.RIneq.html#Rmult_le_reg_l">Rmult_le_reg_l</a> with (/ <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 1).<br/>
35
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; apply <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a>.<br/>
36
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.<br/>
37
apply <a href="Coq.Reals.RIneq.html#Rmult_le_reg_l">Rmult_le_reg_l</a> with (/ 3).<br/>
38
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup0.<br/>
39
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 3); rewrite <- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
40
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.<br/>
41
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; replace (/ <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 1) with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (-1)).<br/>
42
unfold exp in |- *; case (<a href="Coq.Reals.Rtrigo_def.html#exist_exp">exist_exp</a> (-1)); intros; simpl in |- *;<br/>
43
unfold exp_in in e;<br/>
44
assert (H:= <a href="Coq.Reals.AltSeries.html#alternated_series_ineq">alternated_series_ineq</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> i)) x 1).<br/>
46
(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (<a href="Coq.Reals.AltSeries.html#tg_alt">tg_alt</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> i))) (<a href="Coq.Init.Datatypes.html#S">S</a> (2 * 1)) <= x <=<br/>
47
<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (<a href="Coq.Reals.AltSeries.html#tg_alt">tg_alt</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> i))) (2 * 1)).<br/>
48
intro; elim H0; clear H0; intros H0 _; simpl in H0; unfold tg_alt in H0;<br/>
49
simpl in H0.<br/>
50
replace (/ 3) with<br/>
51
(1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +<br/>
52
-1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).<br/>
54
repeat rewrite <a href="Coq.Reals.RIneq.html#Rinv_1">Rinv_1</a>; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>;<br/>
55
rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>;<br/>
56
rewrite <a href="Coq.Reals.RIneq.html#Ropp_involutive">Ropp_involutive</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>;<br/>
57
rewrite <a href="Coq.Reals.Raxioms.html#Rplus_0_l">Rplus_0_l</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with 6.<br/>
58
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_plus_distr_l">Rmult_plus_distr_l</a>; replace (2 + 1 + 1 + 1 + 1) with 6.<br/>
59
rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 6)); rewrite <- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
60
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; replace 6 with 6.<br/>
61
do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
62
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 3); rewrite <- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
63
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
72
unfold Un_decreasing in |- *; intros;<br/>
73
apply <a href="Coq.Reals.RIneq.html#Rmult_le_reg_l">Rmult_le_reg_l</a> with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> n)).<br/>
74
apply <a href="Coq.Reals.Rprod.html#INR_fact_lt_0">INR_fact_lt_0</a>.<br/>
75
apply <a href="Coq.Reals.RIneq.html#Rmult_le_reg_l">Rmult_le_reg_l</a> with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> (<a href="Coq.Init.Datatypes.html#S">S</a> n))).<br/>
76
apply <a href="Coq.Reals.Rprod.html#INR_fact_lt_0">INR_fact_lt_0</a>.<br/>
77
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
78
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
79
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.<br/>
80
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; apply <a href="Coq.Reals.RIneq.html#le_INR">le_INR</a>; apply <a href="Coq.Arith.Factorial.html#fact_le">fact_le</a>; apply <a href="Coq.Arith.Le.html#le_n_Sn">le_n_Sn</a>.<br/>
81
apply <a href="Coq.Reals.Rfunctions.html#INR_fact_neq_0">INR_fact_neq_0</a>.<br/>
82
apply <a href="Coq.Reals.Rfunctions.html#INR_fact_neq_0">INR_fact_neq_0</a>.<br/>
83
assert (H0:= <a href="Coq.Reals.SeqProp.html#cv_speed_pow_fact">cv_speed_pow_fact</a> 1); unfold Un_cv in |- *; unfold Un_cv in H0;<br/>
84
intros; elim (H0 _ H1); intros; exists x0; intros; <br/>
85
unfold R_dist in H2; unfold R_dist in |- *;<br/>
86
replace (/ <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> n)) with (1 ^ n / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> n)).<br/>
88
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Rfunctions.html#pow1">pow1</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; reflexivity.<br/>
89
unfold infinit_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);<br/>
90
intros; exists x0; intros;<br/>
91
replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => (-1) ^ i * / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> i)) n) with<br/>
92
(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => / <a href="Coq.Reals.Raxioms.html#INR">INR</a> (<a href="Coq.Arith.Factorial.html#fact">fact</a> i) * (-1) ^ i) n).<br/>
94
apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros; apply <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>.<br/>
95
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 1).<br/>
96
rewrite <- <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>;<br/>
97
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
103
<code class="keyword">Qed</code>.<br/>
106
<code class="keyword">Theorem</code> <a name="exp_increasing"></a>exp_increasing : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, x < y -> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x < <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> y.<br/>
108
assert (H0 : <a href="Coq.Reals.Ranalysis1.html#derivable">derivable</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a>).<br/>
109
apply <a href="Coq.Reals.Ranalysis4.html#derivable_exp">derivable_exp</a>.<br/>
110
assert (H1:= <a href="Coq.Reals.MVT.html#positive_derivative">positive_derivative</a> _ H0).<br/>
111
unfold strict_increasing in H1.<br/>
114
replace (<a href="Coq.Reals.Ranalysis1.html#derive_pt">derive_pt</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x0 (H0 x0)) with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x0).<br/>
115
apply <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a>.<br/>
116
symmetry in |- *; apply <a href="Coq.Reals.Ranalysis1.html#derive_pt_eq_0">derive_pt_eq_0</a>.<br/>
117
apply (<a href="Coq.Reals.Exp_prop.html#derivable_pt_lim_exp">derivable_pt_lim_exp</a> x0).<br/>
119
<code class="keyword">Qed</code>.<br/>
121
<code class="keyword">Theorem</code> <a name="exp_lt_inv"></a>exp_lt_inv : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x < <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> y -> x < y.<br/>
122
intros x y H; case (<a href="Coq.Reals.RIneq.html#Rtotal_order">Rtotal_order</a> x y); [ intros H1 | intros [H1| H1] ].<br/>
124
rewrite H1 in H; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
125
assert (H2:= <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a> _ _ H1).<br/>
126
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ (<a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> _ _ _ H H2)).<br/>
127
<code class="keyword">Qed</code>.<br/>
129
<code class="keyword">Lemma</code> <a name="exp_ineq1"></a>exp_ineq1 : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> 1 + x < <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x.<br/>
130
intros; apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (- <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 0); rewrite <- (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x));<br/>
131
assert (H0:= <a href="Coq.Reals.MVT.html#MVT_cor1">MVT_cor1</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> 0 x <a href="Coq.Reals.Ranalysis4.html#derivable_exp">derivable_exp</a> H); elim H0; <br/>
132
intros; elim H1; intros; unfold Rminus in H2; rewrite H2; <br/>
133
rewrite <a href="Coq.Reals.RIneq.html#Ropp_0">Ropp_0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>;<br/>
134
replace (<a href="Coq.Reals.Ranalysis1.html#derive_pt">derive_pt</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x0 (<a href="Coq.Reals.Ranalysis4.html#derivable_exp">derivable_exp</a> x0)) with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x0).<br/>
135
rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>; rewrite <- <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>; rewrite <a href="Coq.Reals.RIneq.html#Rplus_opp_l">Rplus_opp_l</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_0_l">Rplus_0_l</a>;<br/>
136
pattern x at 1 in |- *; rewrite <- <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x0));<br/>
137
apply <a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a>.<br/>
139
rewrite <- <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>; apply <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a>; elim H3; intros; assumption.<br/>
140
symmetry in |- *; apply <a href="Coq.Reals.Ranalysis1.html#derive_pt_eq_0">derive_pt_eq_0</a>; apply <a href="Coq.Reals.Exp_prop.html#derivable_pt_lim_exp">derivable_pt_lim_exp</a>.<br/>
141
<code class="keyword">Qed</code>.<br/>
144
<code class="keyword">Lemma</code> <a name="ln_exists1"></a>ln_exists1 : forall y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < y -> 1 <= y -> <a href="Coq.Init.Specif.html#sigT">sigT</a> (fun z:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => y = <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> z).<br/>
145
intros; set (f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x - y); cut (f 0 <= 0).<br/>
146
intro; cut (<a href="Coq.Reals.Ranalysis1.html#continuity">continuity</a> f).<br/>
147
intro; cut (0 <= f y).<br/>
148
intro; cut (f 0 * f y <= 0).<br/>
149
intro; assert (X:= <a href="Coq.Reals.Rsqrt_def.html#IVT_cor">IVT_cor</a> f 0 y H2 (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> _ _ H) H4); elim X; intros t H5;<br/>
150
apply <a href="Coq.Init.Specif.html#existT">existT</a> with t; elim H5; intros; unfold f in H7;<br/>
151
apply <a href="Coq.Reals.RIneq.html#Rminus_diag_uniq_sym">Rminus_diag_uniq_sym</a>; exact H7.<br/>
152
pattern 0 at 2 in |- *; rewrite <- (<a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> (f y));<br/>
153
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (f 0)); apply <a href="Coq.Reals.RIneq.html#Rmult_le_compat_l">Rmult_le_compat_l</a>; <br/>
154
assumption.<br/>
155
unfold f in |- *; apply <a href="Coq.Reals.RIneq.html#Rplus_le_reg_l">Rplus_le_reg_l</a> with y; left;<br/>
156
apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with (1 + y).<br/>
157
rewrite <- (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> y); apply <a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a>; apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a>.<br/>
158
replace (y + (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> y - y)) with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> y); [ apply (exp_ineq1 y H) | ring ].<br/>
159
unfold f in |- *; change (<a href="Coq.Reals.Ranalysis1.html#continuity">continuity</a> (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> - <a href="Coq.Reals.Ranalysis1.html#fct_cte">fct_cte</a> y)) in |- *;<br/>
160
apply <a href="Coq.Reals.Ranalysis1.html#continuity_minus">continuity_minus</a>;<br/>
161
[ apply derivable_continuous; apply derivable_exp
162
| apply derivable_continuous; apply derivable_const ].<br/>
163
unfold f in |- *; rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>; apply <a href="Coq.Reals.RIneq.html#Rplus_le_reg_l">Rplus_le_reg_l</a> with y;<br/>
164
rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; replace (y + (1 - y)) with 1; [ apply H0 | ring ].<br/>
165
<code class="keyword">Qed</code>.<br/>
168
<code class="keyword">Lemma</code> <a name="ln_exists"></a>ln_exists : forall y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < y -> <a href="Coq.Init.Specif.html#sigT">sigT</a> (fun z:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => y = <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> z).<br/>
169
intros; case (<a href="Coq.Reals.RIneq.html#Rle_dec">Rle_dec</a> 1 y); intro.<br/>
170
apply (<a href="Coq.Reals.Rpower.html#ln_exists1">ln_exists1</a> _ H r).<br/>
171
assert (H0 : 1 <= / y).<br/>
172
apply <a href="Coq.Reals.RIneq.html#Rmult_le_reg_l">Rmult_le_reg_l</a> with y.<br/>
174
rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
175
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; left; apply (<a href="Coq.Reals.RIneq.html#Rnot_le_lt">Rnot_le_lt</a> _ _ n).<br/>
176
red in |- *; intro; rewrite H0 in H; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
177
assert (H1 : 0 < / y).<br/>
178
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; apply H.<br/>
179
assert (H2:= <a href="Coq.Reals.Rpower.html#ln_exists1">ln_exists1</a> _ H1 H0); elim H2; intros; apply <a href="Coq.Init.Specif.html#existT">existT</a> with (- x);<br/>
180
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x / y).<br/>
181
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.<br/>
182
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ y)); rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
183
rewrite <- <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>; <br/>
184
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; symmetry in |- *; apply p.<br/>
185
red in |- *; intro; rewrite H3 in H; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
186
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>.<br/>
187
assert (H3:= <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a> x); red in |- *; intro; rewrite H4 in H3;<br/>
188
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H3).<br/>
189
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; red in |- *; intro; rewrite H3 in H;<br/>
190
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
191
<code class="keyword">Qed</code>.<br/>
194
<code class="keyword">Definition</code> <a name="Rln"></a>Rln (y:<a href="Coq.Reals.RIneq.html#posreal">posreal</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> :=<br/>
195
match <a href="Coq.Reals.Rpower.html#ln_exists">ln_exists</a> (<a href="Coq.Reals.RIneq.html#pos">pos</a> y) (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> y) with<br/>
196
| <a href="Coq.Init.Specif.html#existT">existT</a> a b => a<br/>
197
end.<br/>
200
<code class="keyword">Definition</code> <a name="ln"></a>ln (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> :=<br/>
201
match <a href="Coq.Reals.RIneq.html#Rlt_dec">Rlt_dec</a> 0 x with<br/>
202
| <a href="Coq.Init.Specif.html#left">left</a> a => <a href="Coq.Reals.Rpower.html#Rln">Rln</a> (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> x a)<br/>
203
| <a href="Coq.Init.Specif.html#right">right</a> a => 0<br/>
204
end.<br/>
207
<code class="keyword">Lemma</code> <a name="exp_ln"></a>exp_ln : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> x) = x.<br/>
208
intros; unfold ln in |- *; case (<a href="Coq.Reals.RIneq.html#Rlt_dec">Rlt_dec</a> 0 x); intro.<br/>
209
unfold Rln in |- *;<br/>
210
case (<a href="Coq.Reals.Rpower.html#ln_exists">ln_exists</a> (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> x r) (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> x r))); <br/>
212
simpl in e; symmetry in |- *; apply e.<br/>
213
elim n; apply H.<br/>
214
<code class="keyword">Qed</code>.<br/>
217
<code class="keyword">Theorem</code> <a name="exp_inv"></a>exp_inv : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x = <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> y -> x = y.<br/>
218
intros x y H; case (<a href="Coq.Reals.RIneq.html#Rtotal_order">Rtotal_order</a> x y); [ intros H1 | intros [H1| H1] ]; auto;<br/>
219
assert (H2:= <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a> _ _ H1); rewrite H in H2;<br/>
220
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H2).<br/>
221
<code class="keyword">Qed</code>.<br/>
223
<code class="keyword">Theorem</code> <a name="exp_Ropp"></a>exp_Ropp : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- x) = / <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x.<br/>
224
intros x; assert (H : <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x <> 0).<br/>
225
assert (H:= <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a> x); red in |- *; intro; rewrite H0 in H;<br/>
226
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
227
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (r:= <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x).<br/>
228
rewrite <- <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>.<br/>
229
apply <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
232
<code class="keyword">Qed</code>.<br/>
234
<code class="keyword">Theorem</code> <a name="ln_increasing"></a>ln_increasing : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> x < y -> <a href="Coq.Reals.Rpower.html#ln">ln</a> x < <a href="Coq.Reals.Rpower.html#ln">ln</a> y.<br/>
235
intros x y H H0; apply <a href="Coq.Reals.Rpower.html#exp_lt_inv">exp_lt_inv</a>.<br/>
236
repeat rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>. <br/>
238
apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with x; assumption.<br/>
240
<code class="keyword">Qed</code>.<br/>
243
<code class="keyword">Theorem</code> <a name="ln_exp"></a>ln_exp : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rpower.html#ln">ln</a> (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x) = x.<br/>
244
intros x; apply <a href="Coq.Reals.Rpower.html#exp_inv">exp_inv</a>.<br/>
245
apply <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
246
apply <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a>.<br/>
247
<code class="keyword">Qed</code>.<br/>
249
<code class="keyword">Theorem</code> <a name="ln_1"></a>ln_1 : <a href="Coq.Reals.Rpower.html#ln">ln</a> 1 = 0.<br/>
250
rewrite <- <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>; rewrite <a href="Coq.Reals.Rpower.html#ln_exp">ln_exp</a>; reflexivity.<br/>
251
<code class="keyword">Qed</code>.<br/>
253
<code class="keyword">Theorem</code> <a name="ln_lt_inv"></a>ln_lt_inv : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> 0 < y -> <a href="Coq.Reals.Rpower.html#ln">ln</a> x < <a href="Coq.Reals.Rpower.html#ln">ln</a> y -> x < y.<br/>
254
intros x y H H0 H1; rewrite <- (<a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a> x); try rewrite <- (<a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a> y).<br/>
255
apply <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a>; apply H1.<br/>
258
<code class="keyword">Qed</code>.<br/>
260
<code class="keyword">Theorem</code> <a name="ln_inv"></a>ln_inv : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> 0 < y -> <a href="Coq.Reals.Rpower.html#ln">ln</a> x = <a href="Coq.Reals.Rpower.html#ln">ln</a> y -> x = y.<br/>
261
intros x y H H0 H'0; case (<a href="Coq.Reals.RIneq.html#Rtotal_order">Rtotal_order</a> x y); [ intros H1 | intros [H1| H1] ];<br/>
263
assert (H2:= <a href="Coq.Reals.Rpower.html#ln_increasing">ln_increasing</a> _ _ H H1); rewrite H'0 in H2;<br/>
264
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H2).<br/>
265
assert (H2:= <a href="Coq.Reals.Rpower.html#ln_increasing">ln_increasing</a> _ _ H0 H1); rewrite H'0 in H2;<br/>
266
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H2).<br/>
267
<code class="keyword">Qed</code>.<br/>
269
<code class="keyword">Theorem</code> <a name="ln_mult"></a>ln_mult : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> 0 < y -> <a href="Coq.Reals.Rpower.html#ln">ln</a> (x * y) = <a href="Coq.Reals.Rpower.html#ln">ln</a> x + <a href="Coq.Reals.Rpower.html#ln">ln</a> y.<br/>
270
intros x y H H0; apply <a href="Coq.Reals.Rpower.html#exp_inv">exp_inv</a>.<br/>
271
rewrite <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>.<br/>
272
repeat rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
276
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; assumption.<br/>
277
<code class="keyword">Qed</code>.<br/>
280
<code class="keyword">Theorem</code> <a name="ln_Rinv"></a>ln_Rinv : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> <a href="Coq.Reals.Rpower.html#ln">ln</a> (/ x) = - <a href="Coq.Reals.Rpower.html#ln">ln</a> x.<br/>
281
intros x H; apply <a href="Coq.Reals.Rpower.html#exp_inv">exp_inv</a>; repeat rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a> || rewrite <a href="Coq.Reals.Rpower.html#exp_Ropp">exp_Ropp</a>.<br/>
284
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; assumption.<br/>
285
<code class="keyword">Qed</code>.<br/>
288
<code class="keyword">Theorem</code> <a name="ln_continue"></a>ln_continue :<br/>
289
forall y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < y -> <a href="Coq.Reals.Rderiv.html#continue_in">continue_in</a> <a href="Coq.Reals.Rpower.html#ln">ln</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0 < x) y.<br/>
291
unfold continue_in, limit1_in, limit_in in |- *; intros eps Heps.<br/>
292
cut (1 < <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps); [ intros H1 | idtac ].<br/>
293
cut (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps) < 1); [ intros H2 | idtac ].<br/>
294
exists (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (y * (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps - 1)) (y * (1 - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps)))); split.<br/>
295
red in |- *; apply <a href="Coq.Reals.Rpower.html#P_Rmin">P_Rmin</a>.<br/>
296
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>.<br/>
298
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with 1.<br/>
299
rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; replace (1 + (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps - 1)) with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps);<br/>
300
[ apply H1 | ring ].<br/>
301
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>.<br/>
303
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps)).<br/>
304
rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; replace (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps) + (1 - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps))) with 1;<br/>
305
[ apply H2 | ring ].<br/>
306
unfold dist, R_met, R_dist in |- *; simpl in |- *.<br/>
307
intros x [[H3 H4] H5].<br/>
308
cut (y * (x * / y) = x).<br/>
310
replace (<a href="Coq.Reals.Rpower.html#ln">ln</a> x - <a href="Coq.Reals.Rpower.html#ln">ln</a> y) with (<a href="Coq.Reals.Rpower.html#ln">ln</a> (x * / y)).<br/>
311
case (<a href="Coq.Reals.RIneq.html#Rtotal_order">Rtotal_order</a> x y); [ intros Hxy | intros [Hxy| Hxy] ].<br/>
312
rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_left">Rabs_left</a>.<br/>
313
apply <a href="Coq.Reals.RIneq.html#Ropp_lt_cancel">Ropp_lt_cancel</a>; rewrite <a href="Coq.Reals.RIneq.html#Ropp_involutive">Ropp_involutive</a>.<br/>
314
apply <a href="Coq.Reals.Rpower.html#exp_lt_inv">exp_lt_inv</a>.<br/>
315
rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
316
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (r:= y).<br/>
319
apply <a href="Coq.Reals.RIneq.html#Ropp_lt_cancel">Ropp_lt_cancel</a>.<br/>
320
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (r:= y).<br/>
321
replace (y + - (y * <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps))) with (y * (1 - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (- eps)));<br/>
322
[ idtac | ring ].<br/>
323
replace (y + - x) with (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x - y)); [ idtac | ring ].<br/>
324
apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (1 := H5); apply <a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a>.<br/>
325
rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_left">Rabs_left</a>; [ ring | idtac ].<br/>
326
apply (<a href="Coq.Reals.RIneq.html#Rlt_minus">Rlt_minus</a> _ _ Hxy).<br/>
327
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].<br/>
328
rewrite <- <a href="Coq.Reals.Rpower.html#ln_1">ln_1</a>.<br/>
329
apply <a href="Coq.Reals.Rpower.html#ln_increasing">ln_increasing</a>.<br/>
330
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].<br/>
331
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (r:= y).<br/>
333
rewrite Hxyy; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; apply Hxy.<br/>
334
rewrite Hxy; rewrite <a href="Coq.Reals.RIneq.html#Rinv_r">Rinv_r</a>.<br/>
335
rewrite <a href="Coq.Reals.Rpower.html#ln_1">ln_1</a>; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; apply Heps.<br/>
336
red in |- *; intro; rewrite H0 in H; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
337
rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a>.<br/>
338
apply <a href="Coq.Reals.Rpower.html#exp_lt_inv">exp_lt_inv</a>.<br/>
339
rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
340
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (r:= y).<br/>
343
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (r:= - y).<br/>
344
replace (- y + y * <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps) with (y * (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps - 1)); [ idtac | ring ].<br/>
345
replace (- y + x) with (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x - y)); [ idtac | ring ].<br/>
346
apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (1 := H5); apply <a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a>.<br/>
347
rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a>; [ ring | idtac ].<br/>
348
left; apply (<a href="Coq.Reals.RIneq.html#Rgt_minus">Rgt_minus</a> _ _ Hxy).<br/>
349
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].<br/>
350
rewrite <- <a href="Coq.Reals.Rpower.html#ln_1">ln_1</a>.<br/>
351
apply <a href="Coq.Reals.RIneq.html#Rgt_ge">Rgt_ge</a>; red in |- *; apply <a href="Coq.Reals.Rpower.html#ln_increasing">ln_increasing</a>.<br/>
352
apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a>.<br/>
353
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (r:= y).<br/>
355
rewrite Hxyy; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; apply Hxy.<br/>
356
rewrite <a href="Coq.Reals.Rpower.html#ln_mult">ln_mult</a>.<br/>
357
rewrite <a href="Coq.Reals.Rpower.html#ln_Rinv">ln_Rinv</a>.<br/>
361
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; assumption.<br/>
362
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> x); rewrite <- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
364
red in |- *; intro; rewrite H0 in H; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H).<br/>
365
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> eps).<br/>
366
apply <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a>.<br/>
367
rewrite <- <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>;<br/>
369
rewrite <- <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>.<br/>
370
apply <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a>; apply Heps.<br/>
371
<code class="keyword">Qed</code>.<br/>
375
<code class="keyword">Definition</code> <a name="Rpower"></a>Rpower (x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) := <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (y * <a href="Coq.Reals.Rpower.html#ln">ln</a> x).<br/>
378
<code class="keyword">Infix</code> <code class="keyword">Local</code> "^R" := <a href="Coq.Reals.Rpower.html#Rpower">Rpower</a> (at level 30, right associativity) : R_scope.<br/>
382
<code class="keyword">Theorem</code> <a name="Rpower_plus"></a>Rpower_plus : forall x y z:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, z ^R (x + y) = z ^R x * z ^R y.<br/>
383
intros x y z; unfold Rpower in |- *.<br/>
384
rewrite <a href="Coq.Reals.RIneq.html#Rmult_plus_distr_r">Rmult_plus_distr_r</a>; rewrite <a href="Coq.Reals.Exp_prop.html#exp_plus">exp_plus</a>; auto.<br/>
385
<code class="keyword">Qed</code>.<br/>
387
<code class="keyword">Theorem</code> <a name="Rpower_mult"></a>Rpower_mult : forall x y z:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, (x ^R y) ^R z = x ^R (y * z).<br/>
388
intros x y z; unfold Rpower in |- *.<br/>
389
rewrite <a href="Coq.Reals.Rpower.html#ln_exp">ln_exp</a>.<br/>
390
replace (z * (y * <a href="Coq.Reals.Rpower.html#ln">ln</a> x)) with (y * z * <a href="Coq.Reals.Rpower.html#ln">ln</a> x).<br/>
393
<code class="keyword">Qed</code>.<br/>
395
<code class="keyword">Theorem</code> <a name="Rpower_O"></a>Rpower_O : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> x ^R 0 = 1.<br/>
396
intros x H; unfold Rpower in |- *.<br/>
397
rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>; apply <a href="Coq.Reals.Rtrigo_def.html#exp_0">exp_0</a>.<br/>
398
<code class="keyword">Qed</code>.<br/>
400
<code class="keyword">Theorem</code> <a name="Rpower_1"></a>Rpower_1 : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> x ^R 1 = x.<br/>
401
intros x H; unfold Rpower in |- *.<br/>
402
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; apply <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>; apply H.<br/>
403
<code class="keyword">Qed</code>.<br/>
405
<code class="keyword">Theorem</code> <a name="Rpower_pow"></a>Rpower_pow : forall (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>), 0 < x -> x ^R <a href="Coq.Reals.Raxioms.html#INR">INR</a> n = x ^ n.<br/>
406
intros n; elim n; simpl in |- *; auto; fold <a href="Coq.Reals.Raxioms.html#INR">INR</a> in |- *.<br/>
407
intros x H; apply <a href="Coq.Reals.Rpower.html#Rpower_O">Rpower_O</a>; auto.<br/>
408
intros n1; case n1.<br/>
409
intros H x H0; simpl in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; apply <a href="Coq.Reals.Rpower.html#Rpower_1">Rpower_1</a>; auto.<br/>
410
intros n0 H x H0; rewrite <a href="Coq.Reals.Rpower.html#Rpower_plus">Rpower_plus</a>; rewrite H; try rewrite <a href="Coq.Reals.Rpower.html#Rpower_1">Rpower_1</a>;<br/>
411
try apply <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> || assumption.<br/>
412
<code class="keyword">Qed</code>.<br/>
414
<code class="keyword">Theorem</code> <a name="Rpower_lt"></a>Rpower_lt :<br/>
415
forall x y z:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.<br/>
416
intros x y z H H0 H1.<br/>
417
unfold Rpower in |- *.<br/>
418
apply <a href="Coq.Reals.Rpower.html#exp_increasing">exp_increasing</a>.<br/>
419
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_compat_r">Rmult_lt_compat_r</a>.<br/>
420
rewrite <- <a href="Coq.Reals.Rpower.html#ln_1">ln_1</a>; apply <a href="Coq.Reals.Rpower.html#ln_increasing">ln_increasing</a>.<br/>
421
apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a>.<br/>
424
<code class="keyword">Qed</code>.<br/>
426
<code class="keyword">Theorem</code> <a name="Rpower_sqrt"></a>Rpower_sqrt : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> x ^R (/ 2) = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> x.<br/>
428
apply <a href="Coq.Reals.Rpower.html#ln_inv">ln_inv</a>.<br/>
429
unfold Rpower in |- *; apply <a href="Coq.Reals.Exp_prop.html#exp_pos">exp_pos</a>.<br/>
430
apply <a href="Coq.Reals.R_sqrt.html#sqrt_lt_R0">sqrt_lt_R0</a>; apply H.<br/>
431
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> 2).<br/>
432
apply <a href="Coq.Reals.Rpower.html#exp_inv">exp_inv</a>.<br/>
433
fold <a href="Coq.Reals.Rpower.html#Rpower">Rpower</a> in |- *.<br/>
434
cut ((x ^R (/ 2)) ^R <a href="Coq.Reals.Raxioms.html#INR">INR</a> 2 = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> x ^R <a href="Coq.Reals.Raxioms.html#INR">INR</a> 2).<br/>
435
unfold Rpower in |- *; auto.<br/>
436
rewrite <a href="Coq.Reals.Rpower.html#Rpower_mult">Rpower_mult</a>.<br/>
437
rewrite <a href="Coq.Reals.Raxioms.html#Rinv_l">Rinv_l</a>.<br/>
438
replace 1 with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> 1); auto.<br/>
439
repeat rewrite <a href="Coq.Reals.Rpower.html#Rpower_pow">Rpower_pow</a>; simpl in |- *.<br/>
440
pattern x at 1 in |- *; rewrite <- (<a href="Coq.Reals.R_sqrt.html#sqrt_sqrt">sqrt_sqrt</a> x (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> _ _ H)).<br/>
442
apply <a href="Coq.Reals.R_sqrt.html#sqrt_lt_R0">sqrt_lt_R0</a>; apply H.<br/>
444
apply <a href="Coq.Reals.RIneq.html#not_O_INR">not_O_INR</a>; discriminate.<br/>
445
apply <a href="Coq.Reals.RIneq.html#not_O_INR">not_O_INR</a>; discriminate.<br/>
446
<code class="keyword">Qed</code>.<br/>
448
<code class="keyword">Theorem</code> <a name="Rpower_Ropp"></a>Rpower_Ropp : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, x ^R (- y) = / x ^R y.<br/>
449
unfold Rpower in |- *.<br/>
450
intros x y; rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>.<br/>
451
apply <a href="Coq.Reals.Rpower.html#exp_Ropp">exp_Ropp</a>.<br/>
452
<code class="keyword">Qed</code>.<br/>
454
<code class="keyword">Theorem</code> <a name="Rle_Rpower"></a>Rle_Rpower :<br/>
455
forall e n m:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m.<br/>
456
intros e n m H H0 H1; case H1.<br/>
457
intros H2; left; apply <a href="Coq.Reals.Rpower.html#Rpower_lt">Rpower_lt</a>; assumption.<br/>
458
intros H2; rewrite H2; right; reflexivity.<br/>
459
<code class="keyword">Qed</code>.<br/>
461
<code class="keyword">Theorem</code> <a name="ln_lt_2"></a>ln_lt_2 : / 2 < <a href="Coq.Reals.Rpower.html#ln">ln</a> 2.<br/>
462
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (r:= 2).<br/>
464
rewrite <a href="Coq.Reals.RIneq.html#Rinv_r">Rinv_r</a>.<br/>
465
apply <a href="Coq.Reals.Rpower.html#exp_lt_inv">exp_lt_inv</a>.<br/>
466
apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with (1 := <a href="Coq.Reals.Rpower.html#exp_le_3">exp_le_3</a>).<br/>
467
change (3 < 2 ^R 2) in |- *.<br/>
468
repeat rewrite <a href="Coq.Reals.Rpower.html#Rpower_plus">Rpower_plus</a>; repeat rewrite <a href="Coq.Reals.Rpower.html#Rpower_1">Rpower_1</a>.<br/>
469
repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_plus_distr_r">Rmult_plus_distr_r</a>; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_plus_distr_l">Rmult_plus_distr_l</a>;<br/>
470
repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>.<br/>
471
pattern 3 at 1 in |- *; rewrite <- <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; replace (2 + 2) with (3 + 1);<br/>
472
[ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].<br/>
475
<code class="keyword">Qed</code>.<br/>
478
<code class="keyword">Theorem</code> <a name="limit1_ext"></a>limit1_ext :<br/>
479
forall (f g:<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) (l x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),<br/>
480
(forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, D x -> f x = g x) -> <a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> f D l x -> <a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> g D l x.<br/>
481
intros f g D l x H; unfold limit1_in, limit_in in |- *.<br/>
482
intros H0 eps H1; case (H0 eps); auto.<br/>
483
intros x0 [H2 H3]; exists x0; split; auto.<br/>
484
intros x1 [H4 H5]; rewrite <- H; auto.<br/>
485
<code class="keyword">Qed</code>.<br/>
488
<code class="keyword">Theorem</code> <a name="limit1_imp"></a>limit1_imp :<br/>
489
forall (f:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (D D1:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (l x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),<br/>
490
(forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, D1 x -> D x) -> <a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> f D l x -> <a href="Coq.Reals.Rlimit.html#limit1_in">limit1_in</a> f D1 l x.<br/>
491
intros f D D1 l x H; unfold limit1_in, limit_in in |- *.<br/>
492
intros H0 eps H1; case (H0 eps H1); auto.<br/>
493
intros alpha [H2 H3]; exists alpha; split; auto.<br/>
494
intros d [H4 H5]; apply H3; split; auto.<br/>
495
<code class="keyword">Qed</code>.<br/>
498
<code class="keyword">Theorem</code> <a name="Rinv_Rdiv"></a>Rinv_Rdiv : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, x <> 0 -> y <> 0 -> / (x / y) = y / x.<br/>
499
intros x y H1 H2; unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.<br/>
500
rewrite <a href="Coq.Reals.RIneq.html#Rinv_involutive">Rinv_involutive</a>.<br/>
501
apply <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>.<br/>
504
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.<br/>
505
<code class="keyword">Qed</code>.<br/>
508
<code class="keyword">Theorem</code> <a name="Dln"></a>Dln : forall y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < y -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> <a href="Coq.Reals.Rpower.html#ln">ln</a> <a href="Coq.Reals.Rdefinitions.html#Rinv">Rinv</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0 < x) y.<br/>
509
intros y Hy; unfold D_in in |- *.<br/>
510
apply <a href="Coq.Reals.Rpower.html#limit1_ext">limit1_ext</a> with<br/>
511
(f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => / ((<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> x) - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)) / (<a href="Coq.Reals.Rpower.html#ln">ln</a> x - <a href="Coq.Reals.Rpower.html#ln">ln</a> y))).<br/>
512
intros x [HD1 HD2]; repeat rewrite <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
513
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.<br/>
514
rewrite <a href="Coq.Reals.RIneq.html#Rinv_involutive">Rinv_involutive</a>.<br/>
515
apply <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>.<br/>
516
apply <a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a>.<br/>
517
red in |- *; intros H2; case HD2.<br/>
518
symmetry in |- *; apply (<a href="Coq.Reals.Rpower.html#ln_inv">ln_inv</a> _ _ HD1 Hy H2).<br/>
519
apply <a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a>; apply (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> HD2).<br/>
520
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; apply <a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a>; red in |- *; intros H2;<br/>
521
case HD2; apply <a href="Coq.Reals.Rpower.html#ln_inv">ln_inv</a>; auto.<br/>
524
apply <a href="Coq.Reals.Rlimit.html#limit_inv">limit_inv</a> with<br/>
525
(f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> x) - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)) / (<a href="Coq.Reals.Rpower.html#ln">ln</a> x - <a href="Coq.Reals.Rpower.html#ln">ln</a> y)).<br/>
526
apply <a href="Coq.Reals.Rpower.html#limit1_imp">limit1_imp</a> with<br/>
527
(f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)) / (x - <a href="Coq.Reals.Rpower.html#ln">ln</a> y)) (<a href="Coq.Reals.Rpower.html#ln">ln</a> x))<br/>
528
(D:= <a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0 < x) y) (<a href="Coq.Reals.Rderiv.html#D_x">D_x</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)) <a href="Coq.Reals.Rpower.html#ln">ln</a>).<br/>
529
intros x [H1 H2]; split.<br/>
532
red in |- *; intros H3; case H2; apply <a href="Coq.Reals.Rpower.html#ln_inv">ln_inv</a>; auto.<br/>
533
apply <a href="Coq.Reals.Rlimit.html#limit_comp">limit_comp</a> with<br/>
534
(l:= <a href="Coq.Reals.Rpower.html#ln">ln</a> y) (g:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => (<a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> x - <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)) / (x - <a href="Coq.Reals.Rpower.html#ln">ln</a> y)) (f:= <a href="Coq.Reals.Rpower.html#ln">ln</a>).<br/>
535
apply <a href="Coq.Reals.Rpower.html#ln_continue">ln_continue</a>; auto.<br/>
536
assert (H0:= <a href="Coq.Reals.Exp_prop.html#derivable_pt_lim_exp">derivable_pt_lim_exp</a> (<a href="Coq.Reals.Rpower.html#ln">ln</a> y)); unfold derivable_pt_lim in H0;<br/>
537
unfold limit1_in in |- *; unfold limit_in in |- *; <br/>
538
simpl in |- *; unfold R_dist in |- *; intros; elim (H0 _ H); <br/>
539
intros; exists (<a href="Coq.Reals.RIneq.html#pos">pos</a> x); split.<br/>
540
apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> x).<br/>
541
intros; pattern y at 3 in |- *; rewrite <- <a href="Coq.Reals.Rpower.html#exp_ln">exp_ln</a>.<br/>
542
pattern x0 at 1 in |- *; replace x0 with (<a href="Coq.Reals.Rpower.html#ln">ln</a> y + (x0 - <a href="Coq.Reals.Rpower.html#ln">ln</a> y));<br/>
543
[ idtac | ring ].<br/>
545
elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3;<br/>
546
apply <a href="Coq.Reals.RIneq.html#Rminus_eq_contra">Rminus_eq_contra</a>; apply (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> (A:=<a href="Coq.Reals.Rdefinitions.html#R">R</a>)); <br/>
548
elim H2; clear H2; intros _ H2; apply H2.<br/>
550
red in |- *; intro; rewrite H in Hy; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ Hy).<br/>
551
<code class="keyword">Qed</code>.<br/>
554
<code class="keyword">Lemma</code> <a name="derivable_pt_lim_ln"></a>derivable_pt_lim_ln : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim">derivable_pt_lim</a> <a href="Coq.Reals.Rpower.html#ln">ln</a> x (/ x).<br/>
555
intros; assert (H0:= <a href="Coq.Reals.Rpower.html#Dln">Dln</a> x H); unfold D_in in H0; unfold limit1_in in H0;<br/>
556
unfold limit_in in H0; simpl in H0; unfold R_dist in H0;<br/>
557
unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); <br/>
558
intros; elim H2; clear H2; intros; set (alp:= <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> x0 (x / 2));<br/>
559
assert (H4 : 0 < alp).<br/>
560
unfold alp in |- *; unfold Rmin in |- *; case (<a href="Coq.Reals.RIneq.html#Rle_dec">Rle_dec</a> x0 (x / 2)); intro.<br/>
562
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
563
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].<br/>
564
exists (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> _ H4); intros; pattern h at 2 in |- *;<br/>
565
replace h with (x + h - x); [ idtac | ring ].<br/>
566
apply H3; split.<br/>
567
unfold D_x in |- *; split.<br/>
568
case (<a href="Coq.Reals.Rbasic_fun.html#Rcase_abs">Rcase_abs</a> h); intro.<br/>
569
assert (H7 : <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> h < x / 2).<br/>
570
apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with alp.<br/>
572
unfold alp in |- *; apply <a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a>.<br/>
573
apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with (x / 2).<br/>
574
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
575
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].<br/>
576
rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_left">Rabs_left</a> in H7.<br/>
577
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (- h - x / 2).<br/>
578
replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].<br/>
579
pattern x at 2 in |- *; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>.<br/>
580
replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].<br/>
582
apply <a href="Coq.Reals.RIneq.html#Rplus_lt_le_0_compat">Rplus_lt_le_0_compat</a>; [ assumption | apply Rge_le; apply r ].<br/>
583
apply (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> (A:=<a href="Coq.Reals.Rdefinitions.html#R">R</a>)); apply <a href="Coq.Reals.RIneq.html#Rminus_not_eq">Rminus_not_eq</a>; replace (x + h - x) with h;<br/>
584
[ apply H5 | ring ].<br/>
585
replace (x + h - x) with h;<br/>
586
[ apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with alp;<br/>
587
[ apply H6 | unfold alp in |- *; apply Rmin_l ]<br/>
589
<code class="keyword">Qed</code>.<br/>
592
<code class="keyword">Theorem</code> <a name="D_in_imp"></a>D_in_imp :<br/>
593
forall (f g:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (D D1:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),<br/>
594
(forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, D1 x -> D x) -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> f g D x -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> f g D1 x.<br/>
595
intros f g D D1 x H; unfold D_in in |- *.<br/>
596
intros H0; apply <a href="Coq.Reals.Rpower.html#limit1_imp">limit1_imp</a> with (D:= <a href="Coq.Reals.Rderiv.html#D_x">D_x</a> D x); auto.<br/>
597
intros x1 [H1 H2]; split; auto.<br/>
598
<code class="keyword">Qed</code>.<br/>
601
<code class="keyword">Theorem</code> <a name="D_in_ext"></a>D_in_ext :<br/>
602
forall (f g h:<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) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),<br/>
603
f x = g x -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> h f D x -> <a href="Coq.Reals.Rderiv.html#D_in">D_in</a> h g D x.<br/>
604
intros f g h D x H; unfold D_in in |- *.<br/>
605
rewrite H; auto.<br/>
606
<code class="keyword">Qed</code>.<br/>
609
<code class="keyword">Theorem</code> <a name="Dpower"></a>Dpower :<br/>
610
forall y z:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,<br/>
611
0 < y -><br/>
612
<a href="Coq.Reals.Rderiv.html#D_in">D_in</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x ^R z) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => z * x ^R (z - 1)) (<br/>
613
fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0 < x) y.<br/>
615
apply <a href="Coq.Reals.Rpower.html#D_in_imp">D_in_imp</a> with (D:= <a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => 0 < x) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) <a href="Coq.Reals.Rpower.html#ln">ln</a>).<br/>
616
intros x H0; repeat split.<br/>
618
apply <a href="Coq.Reals.Rpower.html#D_in_ext">D_in_ext</a> with (f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => / x * (z * <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (z * <a href="Coq.Reals.Rpower.html#ln">ln</a> x))).<br/>
619
unfold Rminus in |- *; rewrite <a href="Coq.Reals.Rpower.html#Rpower_plus">Rpower_plus</a>; rewrite <a href="Coq.Reals.Rpower.html#Rpower_Ropp">Rpower_Ropp</a>;<br/>
620
rewrite (<a href="Coq.Reals.Rpower.html#Rpower_1">Rpower_1</a> _ H); ring.<br/>
621
apply <a href="Coq.Reals.Rderiv.html#Dcomp">Dcomp</a> with<br/>
622
(f:= <a href="Coq.Reals.Rpower.html#ln">ln</a>)<br/>
623
(g:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (z * x))<br/>
624
(df:= <a href="Coq.Reals.Rdefinitions.html#Rinv">Rinv</a>)<br/>
625
(dg:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => z * <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (z * x)).<br/>
626
apply (<a href="Coq.Reals.Rpower.html#Dln">Dln</a> _ H).<br/>
627
apply <a href="Coq.Reals.Rpower.html#D_in_imp">D_in_imp</a> with<br/>
628
(D:= <a href="Coq.Reals.Rlimit.html#Dgf">Dgf</a> (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) (fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => z * x)).<br/>
629
intros x H1; repeat split; auto.<br/>
631
(<a href="Coq.Reals.Rderiv.html#Dcomp">Dcomp</a> (fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) (fun _:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => <a href="Coq.Init.Logic.html#True">True</a>) (fun x => z) <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a><br/>
632
(fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => z * x) <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a>); simpl in |- *.<br/>
633
apply <a href="Coq.Reals.Rpower.html#D_in_ext">D_in_ext</a> with (f:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => z * 1).<br/>
634
apply <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.<br/>
635
apply (<a href="Coq.Reals.Rderiv.html#Dmult_const">Dmult_const</a> (fun x => <a href="Coq.Init.Logic.html#True">True</a>) (fun x => x) (fun x => 1)); apply <a href="Coq.Reals.Rderiv.html#Dx">Dx</a>.<br/>
636
assert (H0:= <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_D_in">derivable_pt_lim_D_in</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (z * <a href="Coq.Reals.Rpower.html#ln">ln</a> y)); elim H0; clear H0;<br/>
637
intros _ H0; apply H0; apply <a href="Coq.Reals.Exp_prop.html#derivable_pt_lim_exp">derivable_pt_lim_exp</a>.<br/>
638
<code class="keyword">Qed</code>.<br/>
641
<code class="keyword">Theorem</code> <a name="derivable_pt_lim_power"></a>derivable_pt_lim_power :<br/>
642
forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,<br/>
643
0 < x -> <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim">derivable_pt_lim</a> (fun x => x ^R y) x (y * x ^R (y - 1)).<br/>
645
unfold Rminus in |- *; rewrite <a href="Coq.Reals.Rpower.html#Rpower_plus">Rpower_plus</a>.<br/>
646
rewrite <a href="Coq.Reals.Rpower.html#Rpower_Ropp">Rpower_Ropp</a>.<br/>
647
rewrite <a href="Coq.Reals.Rpower.html#Rpower_1">Rpower_1</a>; auto.<br/>
648
rewrite <- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>.<br/>
649
unfold Rpower in |- *.<br/>
650
apply <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_comp">derivable_pt_lim_comp</a> with (f1:= <a href="Coq.Reals.Rpower.html#ln">ln</a>) (f2:= fun x => <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a> (y * x)).<br/>
651
apply <a href="Coq.Reals.Rpower.html#derivable_pt_lim_ln">derivable_pt_lim_ln</a>; assumption.<br/>
652
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> y).<br/>
653
apply <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_comp">derivable_pt_lim_comp</a> with (f1:= fun x => y * x) (f2:= <a href="Coq.Reals.Rtrigo_def.html#exp">exp</a>).<br/>
654
pattern y at 2 in |- *; replace y with (0 * <a href="Coq.Reals.Rpower.html#ln">ln</a> x + y * 1).<br/>
655
apply <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_mult">derivable_pt_lim_mult</a> with (f1:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => y) (f2:= fun x:<a href="Coq.Reals.Rdefinitions.html#R">R</a> => x).<br/>
656
apply <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_const">derivable_pt_lim_const</a> with (a:= y).<br/>
657
apply <a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim_id">derivable_pt_lim_id</a>.<br/>
659
apply <a href="Coq.Reals.Exp_prop.html#derivable_pt_lim_exp">derivable_pt_lim_exp</a>.<br/>
660
<code class="keyword">Qed</code>.</code>
661
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Reals.Rpower.html
