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

forall (fn:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (An:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x l1 l2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>)

(N:<a href="Coq.Init.Datatypes.html#nat">nat</a>),

(forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (fn n x) <= An n) ->

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 - <a href="Coq.Reals.PartSum.html#SP">SP</a> fn N x) <= l2 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N.

intros;

cut

(<a href="Coq.Init.Specif.html#sigT">sigT</a>

(fun l:<a href="Coq.Reals.Rdefinitions.html#R">R</a> =>

<a href="Coq.Reals.Rseries.html#Un_cv">Un_cv</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> <a href="Coq.NArith.BinNat.html#N">N</a> + l)%nat x) n) l)).

intro;

cut

(<a href="Coq.Init.Specif.html#sigT">sigT</a>

(fun l:<a href="Coq.Reals.Rdefinitions.html#R">R</a> =>

<a href="Coq.Reals.Rseries.html#Un_cv">Un_cv</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat) n) l)).

intro; elim X; intros l1N H2.

elim X0; intros l2N H3.

cut (l1 - <a href="Coq.Reals.PartSum.html#SP">SP</a> fn N x = l1N).

intro; cut (l2 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N = l2N).

intro; rewrite H4; rewrite H5.

apply <a href="Coq.Reals.PartSum.html#sum_cv_maj">sum_cv_maj</a> with

(fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat) (fun (l:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) x.

unfold SP in |- *; apply H2.

apply H3.

intros; apply H1.

symmetry in |- *; eapply <a href="Coq.Reals.SeqProp.html#UL_sequence">UL_sequence</a>.

apply H3.

unfold Un_cv in H0; unfold Un_cv in |- *; intros; elim (H0 eps H5);

intros N0 H6.

unfold R_dist in H6; exists N0; intros.

unfold R_dist in |- *;

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat) n - (l2 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N))

with (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N + <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat) n - l2);

[ idtac | ring ].

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N + <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat) n) with

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

apply H6; unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with n.

apply H7.

apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (N + n)%nat.

apply <a href="Coq.Arith.Plus.html#le_plus_r">le_plus_r</a>.

apply <a href="Coq.Arith.Le.html#le_n_Sn">le_n_Sn</a>.

cut (0 <= N)%nat.

cut (N < <a href="Coq.Init.Datatypes.html#S">S</a> (N + n))%nat.

intros; assert (H10:= <a href="Coq.Reals.Rsigma.html#sigma_split">sigma_split</a> An H9 H8).

unfold sigma in H10.

do 2 rewrite <- <a href="Coq.Arith.Minus.html#minus_n_O">minus_n_O</a> in H10.

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))) with

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (0 + k)%nat) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N) with (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (0 + k)%nat) N).

cut ((<a href="Coq.Init.Datatypes.html#S">S</a> (N + n) - <a href="Coq.Init.Datatypes.html#S">S</a> N)%nat = n).

intro; rewrite H11 in H10.

apply H10.

apply <a href="Coq.Reals.RIneq.html#INR_eq">INR_eq</a>; rewrite <a href="Coq.Reals.RIneq.html#minus_INR">minus_INR</a>.

do 2 rewrite <a href="Coq.Reals.RIneq.html#S_INR">S_INR</a>; rewrite <a href="Coq.Reals.RIneq.html#plus_INR">plus_INR</a>; ring.

apply <a href="Coq.Arith.Le.html#le_n_S">le_n_S</a>; apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

reflexivity.

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

reflexivity.

apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>; apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

apply <a href="Coq.Arith.Le.html#le_O_n">le_O_n</a>.

symmetry in |- *; eapply <a href="Coq.Reals.SeqProp.html#UL_sequence">UL_sequence</a>.

apply H2.

unfold Un_cv in H; unfold Un_cv in |- *; intros.

elim (H eps H4); intros N0 H5.

unfold R_dist in H5; exists N0; intros.

unfold R_dist, SP in |- *;

replace

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n -

(l1 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N)) with

100

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N +

101

<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n - l1);

102

[ idtac | ring ].

103

replace

104

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N +

105

<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n) with

106

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

107

unfold SP in H5; apply H5; unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with n.

108

apply H6.

109

apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (N + n)%nat.

110

apply <a href="Coq.Arith.Plus.html#le_plus_r">le_plus_r</a>.

111

apply <a href="Coq.Arith.Le.html#le_n_Sn">le_n_Sn</a>.

112

cut (0 <= N)%nat.

113

cut (N < <a href="Coq.Init.Datatypes.html#S">S</a> (N + n))%nat.

114

intros; assert (H9:= <a href="Coq.Reals.Rsigma.html#sigma_split">sigma_split</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) H8 H7).

115

unfold sigma in H9.

116

do 2 rewrite <- <a href="Coq.Arith.Minus.html#minus_n_O">minus_n_O</a> in H9.

117

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))) with

118

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (0 + k)%nat x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

119

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N) with

120

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (0 + k)%nat x) N).

121

cut ((<a href="Coq.Init.Datatypes.html#S">S</a> (N + n) - <a href="Coq.Init.Datatypes.html#S">S</a> N)%nat = n).

122

intro; rewrite H10 in H9.

123

apply H9.

124

apply <a href="Coq.Reals.RIneq.html#INR_eq">INR_eq</a>; rewrite <a href="Coq.Reals.RIneq.html#minus_INR">minus_INR</a>.

125

do 2 rewrite <a href="Coq.Reals.RIneq.html#S_INR">S_INR</a>; rewrite <a href="Coq.Reals.RIneq.html#plus_INR">plus_INR</a>; ring.

126

apply <a href="Coq.Arith.Le.html#le_n_S">le_n_S</a>; apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

127

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

128

reflexivity.

129

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

130

reflexivity.

131

apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>.

132

apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

133

apply <a href="Coq.Arith.Le.html#le_O_n">le_O_n</a>.

134

apply <a href="Coq.Init.Specif.html#existT">existT</a> with (l2 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An N).

135

unfold Un_cv in H0; unfold Un_cv in |- *; intros.

136

elim (H0 eps H2); intros N0 H3.

137

unfold R_dist in H3; exists N0; intros.

138

unfold R_dist in |- *;

139

140

141

[ idtac | ring ].

142

143

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

144

apply H3; unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with n.

145

apply H4.

146

apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (N + n)%nat.

147

apply <a href="Coq.Arith.Plus.html#le_plus_r">le_plus_r</a>.

148

apply <a href="Coq.Arith.Le.html#le_n_Sn">le_n_Sn</a>.

149

cut (0 <= N)%nat.

150

cut (N < <a href="Coq.Init.Datatypes.html#S">S</a> (N + n))%nat.

151

intros; assert (H7:= <a href="Coq.Reals.Rsigma.html#sigma_split">sigma_split</a> An H6 H5).

152

unfold sigma in H7.

153

do 2 rewrite <- <a href="Coq.Arith.Minus.html#minus_n_O">minus_n_O</a> in H7.

154

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))) with

155

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (0 + k)%nat) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

156

157

cut ((<a href="Coq.Init.Datatypes.html#S">S</a> (N + n) - <a href="Coq.Init.Datatypes.html#S">S</a> N)%nat = n).

158

intro; rewrite H8 in H7.

159

apply H7.

160

apply <a href="Coq.Reals.RIneq.html#INR_eq">INR_eq</a>; rewrite <a href="Coq.Reals.RIneq.html#minus_INR">minus_INR</a>.

161

do 2 rewrite <a href="Coq.Reals.RIneq.html#S_INR">S_INR</a>; rewrite <a href="Coq.Reals.RIneq.html#plus_INR">plus_INR</a>; ring.

162

apply <a href="Coq.Arith.Le.html#le_n_S">le_n_S</a>; apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

163

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

164

reflexivity.

165

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

166

reflexivity.

167

apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>.

168

apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

169

apply <a href="Coq.Arith.Le.html#le_O_n">le_O_n</a>.

170

apply <a href="Coq.Init.Specif.html#existT">existT</a> with (l1 - <a href="Coq.Reals.PartSum.html#SP">SP</a> fn N x).

171

unfold Un_cv in H; unfold Un_cv in |- *; intros.

172

elim (H eps H2); intros N0 H3.

173

unfold R_dist in H3; exists N0; intros.

174

unfold R_dist, SP in |- *.

175

replace

176

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n -

177

(l1 - <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N)) with

178

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N +

179

<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n - l1);

180

[ idtac | ring ].

181

replace

182

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N +

183

<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun l:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (<a href="Coq.Init.Datatypes.html#S">S</a> N + l)%nat x) n) with

184

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

185

unfold SP in H3; apply H3.

186

unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with n.

187

apply H4.

188

apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (N + n)%nat.

189

apply <a href="Coq.Arith.Plus.html#le_plus_r">le_plus_r</a>.

190

apply <a href="Coq.Arith.Le.html#le_n_Sn">le_n_Sn</a>.

191

cut (0 <= N)%nat.

192

cut (N < <a href="Coq.Init.Datatypes.html#S">S</a> (N + n))%nat.

193

intros; assert (H7:= <a href="Coq.Reals.Rsigma.html#sigma_split">sigma_split</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) H6 H5).

194

unfold sigma in H7.

195

do 2 rewrite <- <a href="Coq.Arith.Minus.html#minus_n_O">minus_n_O</a> in H7.

196

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))) with

197

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (0 + k)%nat x) (<a href="Coq.Init.Datatypes.html#S">S</a> (N + n))).

198

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn k x) N) with

199

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => fn (0 + k)%nat x) N).

200

cut ((<a href="Coq.Init.Datatypes.html#S">S</a> (N + n) - <a href="Coq.Init.Datatypes.html#S">S</a> N)%nat = n).

201

intro; rewrite H8 in H7.

202

apply H7.

203

apply <a href="Coq.Reals.RIneq.html#INR_eq">INR_eq</a>; rewrite <a href="Coq.Reals.RIneq.html#minus_INR">minus_INR</a>.

204

do 2 rewrite <a href="Coq.Reals.RIneq.html#S_INR">S_INR</a>; rewrite <a href="Coq.Reals.RIneq.html#plus_INR">plus_INR</a>; ring.

205

apply <a href="Coq.Arith.Le.html#le_n_S">le_n_S</a>; apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

206

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

207

reflexivity.

208

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros.

209

reflexivity.

210

apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>.

211

apply <a href="Coq.Arith.Plus.html#le_plus_l">le_plus_l</a>.

212

apply <a href="Coq.Arith.Le.html#le_O_n">le_O_n</a>.

213

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

214

215

216

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

217

forall An Bn:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>,

218

(forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, 0 <= An n <= Bn n) ->

219

220

221

intros; apply <a href="Coq.Reals.PartSum.html#cv_cauchy_2">cv_cauchy_2</a>.

222

assert (H0:= <a href="Coq.Reals.PartSum.html#cv_cauchy_1">cv_cauchy_1</a> _ X).

223

unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.

224

intros; elim (H0 eps H1); intros.

225

exists x; intros.

226

cut

227

(<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n) (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An m) <=

228

<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn n) (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn m)).

229

intro; apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with (<a href="Coq.Reals.Rfunctions.html#R_dist">R_dist</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn n) (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn m)).

230

assumption.

231

apply H2; assumption.

232

assert (H5:= <a href="Coq.Arith.Compare_dec.html#lt_eq_lt_dec">lt_eq_lt_dec</a> n m).

233

elim H5; intro.

234

elim a; intro.

235

rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> An n m); [ idtac | assumption ].

236

rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> Bn n m); [ idtac | assumption ].

237

unfold R_dist in |- *; unfold Rminus in |- *; do 2 rewrite <a href="Coq.Reals.RIneq.html#Ropp_plus_distr">Ropp_plus_distr</a>;

238

do 2 rewrite <- <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>; do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>;

239

do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rplus_0_l">Rplus_0_l</a>; do 2 rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a>; repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a>.

240

apply <a href="Coq.Reals.PartSum.html#sum_Rle">sum_Rle</a>; intros.

241

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> n + n0)%nat); intros.

242

apply H8.

243

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; apply <a href="Coq.Reals.PartSum.html#cond_pos_sum">cond_pos_sum</a>; intro.

244

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> n + n0)%nat); intros.

245

apply <a href="Coq.Reals.RIneq.html#Rle_trans">Rle_trans</a> with (An (<a href="Coq.Init.Datatypes.html#S">S</a> n + n0)%nat); assumption.

246

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; apply <a href="Coq.Reals.PartSum.html#cond_pos_sum">cond_pos_sum</a>; intro.

247

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> n + n0)%nat); intros; assumption.

248

rewrite b; unfold R_dist in |- *; unfold Rminus in |- *;

249

do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; right;

250

reflexivity.

251

rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> An m n); [ idtac | assumption ].

252

rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> Bn m n); [ idtac | assumption ].

253

unfold R_dist in |- *; unfold Rminus in |- *; do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>;

254

rewrite (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An m)); rewrite (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn m));

255

do 2 rewrite <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>; do 2 rewrite <a href="Coq.Reals.RIneq.html#Rplus_opp_l">Rplus_opp_l</a>;

256

do 2 rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a>.

257

apply <a href="Coq.Reals.PartSum.html#sum_Rle">sum_Rle</a>; intros.

258

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> m + n0)%nat); intros; apply H8.

259

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; apply <a href="Coq.Reals.PartSum.html#cond_pos_sum">cond_pos_sum</a>; intro.

260

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> m + n0)%nat); intros.

261

apply <a href="Coq.Reals.RIneq.html#Rle_trans">Rle_trans</a> with (An (<a href="Coq.Init.Datatypes.html#S">S</a> m + n0)%nat); assumption.

262

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>.

263

apply <a href="Coq.Reals.PartSum.html#cond_pos_sum">cond_pos_sum</a>; intro.

264

elim (H (<a href="Coq.Init.Datatypes.html#S">S</a> m + n0)%nat); intros; assumption.

265

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

266

267

268

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

269

forall (An Bn:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (l:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

270

271

(forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, 0 < An n) ->

272

<a href="Coq.Reals.SeqProp.html#cv_infty">cv_infty</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n) ->

273

<a href="Coq.Reals.Rseries.html#Un_cv">Un_cv</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * Bn k) n / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)

274

l.

275

<code class="keyword">Proof</code> with trivial.

276

unfold Un_cv in |- *; intros; assert (H3 : forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, 0 < <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

277

intro; apply <a href="Coq.Reals.PartSum.html#tech1">tech1</a>...

278

assert (H4 : forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n <> 0)...

279

intro; red in |- *; intro; assert (H5:= H3 n); rewrite H4 in H5;

280

elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H5)...

281

assert (H5:= <a href="Coq.Reals.SeqProp.html#cv_infty_cv_R0">cv_infty_cv_R0</a> _ H4 H1); assert (H6 : 0 < eps / 2)...

282

unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>...

283

apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup...

284

elim (H _ H6); clear H; intros N1 H;

285

set (C:= <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * (Bn k - l)) N1));

286

assert

287

(H7 :

288

exists N : <a href="Coq.Init.Datatypes.html#nat">nat</a>,

289

(forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, (N <= n)%nat -> C / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n < eps / 2))...

290

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> C 0); intro...

291

exists 0%nat; intros...

292

rewrite H7; unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>...

293

apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup...

294

assert (H8 : 0 < eps / (2 * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> C))...

295

unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>...

296

apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>...

297

prove_sup...

298

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

299

elim (H5 _ H8); intros; exists x; intros; assert (H11:= H9 _ H10);

300

unfold R_dist in H11; unfold Rminus in H11; rewrite <a href="Coq.Reals.RIneq.html#Ropp_0">Ropp_0</a> in H11;

301

rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a> in H11...

302

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (C / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n))...

303

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

304

unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> C)...

305

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>...

306

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>...

307

rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; replace (/ <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> C * (eps * / 2)) with (eps / (2 * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> C))...

308

unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>...

309

ring...

310

discrR...

311

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

312

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

313

elim H7; clear H7; intros N2 H7; set (N:= <a href="Coq.Arith.Max.html#max">max</a> N1 N2); exists (<a href="Coq.Init.Datatypes.html#S">S</a> N); intros;

314

unfold R_dist in |- *;

315

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * Bn k) n / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n - l) with

316

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * (Bn k - l)) n / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

317

assert (H9 : (N1 < n)%nat)...

318

apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (<a href="Coq.Init.Datatypes.html#S">S</a> N)...

319

apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>; unfold N in |- *; apply <a href="Coq.Arith.Max.html#le_max_l">le_max_l</a>...

320

rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * (Bn k - l)) _ _ H9); unfold Rdiv in |- *;

321

rewrite <a href="Coq.Reals.RIneq.html#Rmult_plus_distr_r">Rmult_plus_distr_r</a>;

322

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

323

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * (Bn k - l)) N1 / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n) +

324

325

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat * (Bn (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat - l))

326

(n - <a href="Coq.Init.Datatypes.html#S">S</a> N1) / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n))...

327

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

328

rewrite (<a href="Coq.Reals.RIneq.html#double_var">double_var</a> eps); apply <a href="Coq.Reals.RIneq.html#Rplus_lt_compat">Rplus_lt_compat</a>...

329

unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>; fold C in |- *; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a>...

330

apply (H7 n); apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (<a href="Coq.Init.Datatypes.html#S">S</a> N)...

331

apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with N; [ unfold N in |- *; apply le_max_r | apply le_n_Sn ]...

332

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; left; apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>...

333

334

335

unfold R_dist in H; unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>;

336

rewrite (<a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a> (/ <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n))...

337

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

338

(<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.Rbasic_fun.html#Rabs">Rabs</a> (An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat * (Bn (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat - l)))

339

(n - <a href="Coq.Init.Datatypes.html#S">S</a> N1) * / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

340

do 2 rewrite <- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)); apply <a href="Coq.Reals.RIneq.html#Rmult_le_compat_l">Rmult_le_compat_l</a>...

341

left; apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>...

342

apply

343

(<a href="Coq.Reals.PartSum.html#Rsum_abs">Rsum_abs</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat * (Bn (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat - l))

344

(n - <a href="Coq.Init.Datatypes.html#S">S</a> N1))...

345

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

346

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat * (eps / 2)) (n - <a href="Coq.Init.Datatypes.html#S">S</a> N1) *

347

/ <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

348

349

left; apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>...

350

apply <a href="Coq.Reals.PartSum.html#sum_Rle">sum_Rle</a>; intros; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>;

351

pattern (An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + n0)%nat) at 2 in |- *;

352

rewrite <- (<a href="Coq.Reals.Rbasic_fun.html#Rabs_right">Rabs_right</a> (An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + n0)%nat))...

353

apply <a href="Coq.Reals.RIneq.html#Rmult_le_compat_l">Rmult_le_compat_l</a>...

354

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

355

left; apply H; unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_trans">le_trans</a> with (<a href="Coq.Init.Datatypes.html#S">S</a> N1);

356

[ apply le_n_Sn | apply le_plus_l ]...

357

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; left...

358

rewrite <- (<a href="Coq.Reals.PartSum.html#scal_sum">scal_sum</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat) (n - <a href="Coq.Init.Datatypes.html#S">S</a> N1) (eps / 2));

359

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; apply <a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a>...

360

pattern (/ 2) at 2 in |- *; rewrite <- <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; apply <a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a>...

361

apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup...

362

rewrite <a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

363

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>...

364

rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite (<a href="Coq.Reals.PartSum.html#tech2">tech2</a> An N1 n)...

365

rewrite <a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a>;

366

pattern (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun i:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An (<a href="Coq.Init.Datatypes.html#S">S</a> N1 + i)%nat) (n - <a href="Coq.Init.Datatypes.html#S">S</a> N1)) at 1 in |- *;

367

rewrite <- <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; apply <a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a>...

368

apply <a href="Coq.Reals.RIneq.html#Rle_ge">Rle_ge</a>; left; apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>...

369

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * (Bn k - l)) n) with

370

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * Bn k) n +

371

<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * - l) n)...

372

rewrite <- (<a href="Coq.Reals.PartSum.html#scal_sum">scal_sum</a> An n (- l)); field...

373

rewrite <- <a href="Coq.Reals.PartSum.html#plus_sum">plus_sum</a>; apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros; ring...

374

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

375

376

377

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

378

forall (An:<a href="Coq.Init.Datatypes.html#nat">nat</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (l:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

379

<a href="Coq.Reals.Rseries.html#Un_cv">Un_cv</a> An l -> <a href="Coq.Reals.Rseries.html#Un_cv">Un_cv</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Peano.html#pred">pred</a> n) / <a href="Coq.Reals.Raxioms.html#INR">INR</a> n) l.

380

<code class="keyword">Proof</code> with trivial.

381

intros Bn l H; set (An:= fun _:<a href="Coq.Init.Datatypes.html#nat">nat</a> => 1)...

382

assert (H0 : forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, 0 < An n)...

383

intro; unfold An in |- *; apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a>...

384

assert (H1 : forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, 0 < <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n)...

385

intro; apply <a href="Coq.Reals.PartSum.html#tech1">tech1</a>...

386

assert (H2 : <a href="Coq.Reals.SeqProp.html#cv_infty">cv_infty</a> (fun n:<a href="Coq.Init.Datatypes.html#nat">nat</a> => <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An n))...

387

unfold cv_infty in |- *; intro; case (<a href="Coq.Reals.RIneq.html#Rle_dec">Rle_dec</a> M 0); intro...

388

exists 0%nat; intros; apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with 0...

389

assert (H2 : 0 < M)...

390

auto with real...

391

clear n; set (m:= <a href="Coq.Reals.Rdefinitions.html#up">up</a> M); elim (<a href="Coq.Reals.Raxioms.html#archimed">archimed</a> M); intros;

392

assert (H5 : (0 <= m)%Z)...

393

apply <a href="Coq.Reals.RIneq.html#le_IZR">le_IZR</a>; unfold m in |- *; simpl in |- *; left; apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with M...

394

elim (<a href="Coq.Reals.RIneq.html#IZN">IZN</a> _ H5); intros; exists x; intros; unfold An in |- *; rewrite <a href="Coq.Reals.PartSum.html#sum_cte">sum_cte</a>;

395

rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> (<a href="Coq.Reals.Rdefinitions.html#up">up</a> M))...

396

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> x)...

397

rewrite <a href="Coq.Reals.RIneq.html#INR_IZR_INZ">INR_IZR_INZ</a>; fold m in |- *; rewrite <- H6; right...

398

apply <a href="Coq.Reals.RIneq.html#lt_INR">lt_INR</a>; apply <a href="Coq.Arith.Lt.html#le_lt_n_Sm">le_lt_n_Sm</a>...

399

assert (H3:= <a href="Coq.Reals.SeqSeries.html#Cesaro">Cesaro</a> _ _ _ H H0 H2)...

400

unfold Un_cv in |- *; unfold Un_cv in H3; intros; elim (H3 _ H4); intros;

401

exists (<a href="Coq.Init.Datatypes.html#S">S</a> x); intros; unfold R_dist in |- *; unfold R_dist in H5;

402

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

403

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

404

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => An k * Bn k) (<a href="Coq.Init.Peano.html#pred">pred</a> n) / <a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> An (<a href="Coq.Init.Peano.html#pred">pred</a> n) - l))...

405

right;

406

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn (<a href="Coq.Init.Peano.html#pred">pred</a> n) / <a href="Coq.Reals.Raxioms.html#INR">INR</a> n - l) with

407

408

unfold Rminus in |- *; do 2 rewrite <- (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (- l));

409

apply <a href="Coq.Reals.RIneq.html#Rplus_eq_compat_l">Rplus_eq_compat_l</a>...

410

unfold An in |- *;

411

replace (<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> (fun k:<a href="Coq.Init.Datatypes.html#nat">nat</a> => 1 * Bn k) (<a href="Coq.Init.Peano.html#pred">pred</a> n)) with

412

(<a href="Coq.Reals.Rfunctions.html#sum_f_R0">sum_f_R0</a> Bn (<a href="Coq.Init.Peano.html#pred">pred</a> n))...

413

rewrite <a href="Coq.Reals.PartSum.html#sum_cte">sum_cte</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; replace (<a href="Coq.Init.Datatypes.html#S">S</a> (<a href="Coq.Init.Peano.html#pred">pred</a> n)) with n...

414

apply <a href="Coq.Arith.Lt.html#S_pred">S_pred</a> with 0%nat; apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (<a href="Coq.Init.Datatypes.html#S">S</a> x)...

415

apply <a href="Coq.Arith.Lt.html#lt_O_Sn">lt_O_Sn</a>...

416

apply <a href="Coq.Reals.PartSum.html#sum_eq">sum_eq</a>; intros; ring...

417

apply H5; unfold ge in |- *; apply <a href="Coq.Arith.Le.html#le_S_n">le_S_n</a>; replace (<a href="Coq.Init.Datatypes.html#S">S</a> (<a href="Coq.Init.Peano.html#pred">pred</a> n)) with n...

418

apply <a href="Coq.Arith.Lt.html#S_pred">S_pred</a> with 0%nat; apply <a href="Coq.Arith.Lt.html#lt_le_trans">lt_le_trans</a> with (<a href="Coq.Init.Datatypes.html#S">S</a> x)...

419

apply <a href="Coq.Arith.Lt.html#lt_O_Sn">lt_O_Sn</a>...

420

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

421

</code>

422

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

423

</body>

424

</html>

b'\\ No newline at end of file'

Older »