From b2c3d344a8f73bda5b39e66412c2a6a8f861ba59 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 May 2021 20:20:17 +0900 Subject: [PATCH] More examples of sequences and series - convergence of (1 + 1/n)^n - density of R --- _CoqProject | 1 + theories/sequences_wip.v | 385 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 386 insertions(+) create mode 100644 theories/sequences_wip.v diff --git a/_CoqProject b/_CoqProject index 594eaceef..fe93bdfc0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -31,6 +31,7 @@ theories/nsatz_realtype.v theories/esum.v theories/real_interval.v theories/lebesgue_measure.v +theories/sequences_wip.v theories/forms.v theories/derive.v theories/measure.v diff --git a/theories/sequences_wip.v b/theories/sequences_wip.v new file mode 100644 index 000000000..cca443005 --- /dev/null +++ b/theories/sequences_wip.v @@ -0,0 +1,385 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice seq. +From mathcomp Require Import bigop div ssralg ssrint ssrnum fintype order. +From mathcomp Require Import binomial matrix interval rat. +Require Import boolp reals ereal classical_sets functions signed topology. +Require Import normedtype landau sequences. + +(******************************************************************************) +(* More standard sequences and series (WIP) *) +(* *) +(* The main purpose of this file is to test extensions to sequences.v *) +(* *) +(* euler_seq n == the sequence (1 + 1 / n) ^ n *) +(* euler_constant == Euler constant e defined as lim euler_seq with *) +(* proof 2 < e <= 4 *) +(* riemann == Riemann sequence 1/(n + 1)^a *) +(* dvg_riemann == the Riemann series does not converge *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section euler_constant. +Variable (R : realType). +Implicit Types n m : nat. + +Definition euler_seq : (R^o) ^nat := [sequence (1 + 1 / n%:R) ^+ n]_n. +Local Notation u_ := euler_seq. + +Lemma euler_seq0 : u_ O = 1. +Proof. by rewrite /u_ {1}(_ : 1 = 1%:R) // ler_nat. Qed. + +Lemma euler_seq1 : u_ 1%nat = 2. +Proof. by rewrite /u_ /= expr1 divr1. Qed. + +Lemma euler_seq2 : u_ 2%nat = 9%:R / 4%:R. +Proof. +rewrite /euler_seq /= -{1}(@divrr _ 2) ?unitfE // -mulrDl. +by rewrite expr_div_n {2}(_ : 1 = 1%:R) // -natrD -2!natrX. +Qed. + +Section euler_seq_is_bounded_by_4. +Let v_ n m : R := (n - m + 2)%:R / (n - m)%:R. + +Let v_increasing n : forall m, (m < n)%nat -> v_ n.*2 m < v_ n.*2 m.+1. +Proof. +move=> m mn; rewrite /v_. +have H : forall p q, + (1 < q < p)%nat -> (p%:R : R) / q%:R < (p%:R - 1) / (q%:R - 1). + move=> p q pq; rewrite ltr_pdivr_mulr; last first. + move/andP : pq => -[a b]. + by rewrite (_ : 0 = 0%:R) // ltr_nat (ltn_trans _ a). + rewrite mulrAC ltr_pdivl_mulr; last first. + by rewrite subr_gt0 (_ : 1 = 1%:R) // ltr_nat; case/andP: pq. + by rewrite mulrBl mulrBr mul1r mulr1 ler_lt_sub // ltr_nat; case/andP : pq. +rewrite -(addn1 m) !subnDA (@natrB _ _ 1); last first. + by rewrite subn_gt0 (leq_trans mn) // -addnn leq_addr. +rewrite (_ : (n.*2 - m - 1 + 2)%:R = (n.*2 - m + 2 - 1)%:R); last first. + rewrite !subn1 !addn2 /= prednK // subn_gt0 (leq_trans mn) //. + by rewrite -addnn leq_addr. +rewrite (@natrB _ _ 1) ?subn_gt0 ?addn2 //. +apply H; apply/andP; split; last by rewrite ltnS. +move: (mn); rewrite -(ltn_add2r 1) !addn1 => mn'. +rewrite ltn_subRL addn1 (leq_trans mn'){mn'} // -addnn -{1}(addn0 n) ltn_add2l. +by rewrite (leq_trans _ mn). +Qed. + +Let v_nondecreasing n : forall i, (i < n)%nat -> v_ n.*2 0 <= v_ n.*2 i. +Proof. +elim=> // -[/= _ n1|i ih ni]. + by apply/ltW/v_increasing; rewrite (ltn_trans _ n1). +rewrite (le_trans (ih _)) // ?(leq_trans _ ni) //. +by apply/ltW/v_increasing; rewrite (leq_trans _ ni). +Qed. + +Let prod_v_ n : (0 < n)%nat -> + \prod_(i < n) v_ n.*2 i = (n.*2.+2 * n.*2.+1)%:R / (n.+2 * n.+1)%:R. +Proof. +move=> n0; set lhs := LHS. set rhs := RHS. +rewrite -(@divr1_eq _ lhs rhs) // {}/lhs {}/rhs invf_div mulrA. +rewrite /v_ big_split /= -mulrA mulrACA. +rewrite [X in X * _ = 1](_ : _ = \prod_(i < n.+2) (n.*2 - i + 2)%:R); last first. + rewrite 2!big_ord_recr /= -mulrA; congr (_ * _). + by rewrite -addnn addnK subnS addnK 2!addn2 /= natrM prednK. +rewrite [X in _ * X = 1](_ : _ = \prod_(i < n.+2) (n.*2 - i + 2)%:R^-1); last first. + rewrite 2!big_ord_recl /= mulrA [in LHS]mulrC; congr (_ * _). + rewrite subn0 addn2 subn1 addn2 prednK ?double_gt0 //. + by rewrite natrM invrM ?unitfE // mulrC. + apply eq_bigr => i _; congr (_ %:R^-1). + rewrite /bump !leq0n !add1n -addn2 subnDA subn2 addn2 /= prednK; last first. + rewrite -subnS subn_gt0 -addnn -(addn1 i) (@leq_trans n.+1) //. + by rewrite addn1 ltnS. + by rewrite -{1}(addn0 n) ltn_add2l. + by rewrite prednK // subn_gt0 -addnn (@leq_trans n) // leq_addr. +by rewrite -big_split /= big1 // => i _; rewrite divrr // ?unitfE addn2. +Qed. + +Lemma euler_seq_lt4 n : (0 < n)%nat -> u_ n < 4%:R. +Proof. +move=> n0. +rewrite /u_ /= -{1}(@divrr _ n%:R) ?unitfE ?pnatr_eq0 -?lt0n // -mulrDl. +rewrite (_ : _ ^+ n = \prod_(i < n) ((n%:R + 1) / n%:R)); last first. + move _ : (_ / _) => h. + elim: n n0 => // -[_ _|n ih _]. + by rewrite big_ord_recl big_ord0 mulr1 expr1. + by rewrite exprS ih // [in RHS]big_ord_recl. +rewrite (@le_lt_trans _ _ (\prod_(i < n) v_ n.*2 i)) //; last first. + rewrite prod_v_ // (_ : _ / _%:R = 2%:R * (n.*2.+1)%:R / n.+2%:R); last first. + rewrite -doubleS natrM -muln2 (natrM _ _ 2) natrM. + rewrite invrM ?unitfE ?pnatr_eq0 //. + rewrite mulrCA 3!mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r; congr (_ * _). + rewrite ltr_pdivr_mulr // (_ : 4 = 2 * 2)%nat // (natrM _ 2) -mulrA. + rewrite ltr_pmul2l // -natrM mul2n ltr_nat doubleS 2!ltnS -2!muln2. + by rewrite leq_mul2r /=. +apply ler_prod => i _; apply/andP; split. + apply divr_ge0; last exact/ler0n. + by rewrite [X in _ <= _ + X](_ : _ = 1%:R) // -natrD ler0n. +apply: (@le_trans _ _ (v_ n.*2 (@ord0 n))). + rewrite /v_ subn0 addn2 -doubleS. + rewrite -2!muln2 2!natrM invrM // ?unitfE //; last first. + by rewrite pnatr_eq0 -lt0n. + rewrite -mulrA (mulrA 2) divrr ?unitfE // div1r. + by rewrite [X in (_ + X) / _ <= _](_ : _ = 1%:R) // -natrD addn1. +exact/v_nondecreasing. +Qed. + +End euler_seq_is_bounded_by_4. + +Section euler_seq_increasing. + +(* NB: see also SUM_GROUP in the PR 383 *) +Let sum_group_by_2 n (f : nat -> R) : + \sum_(i < n) f i = \sum_(i < n./2) (f i.*2 + f i.*2.+1) + if + odd n.+1 then 0 else f n.-1. +Proof. +elim: n.+1 {-2}n (ltnSn n) => {n} // m ih [_|n]. + by rewrite 2!big_ord0 /= addr0. +rewrite ltnS => nm. +rewrite big_ord_recr /= ih // negbK; case: ifPn => /= [|]. + by move/negbTE => no; rewrite no addr0 uphalf_half no add0n. +rewrite negbK => no. +rewrite no uphalf_half no add1n addr0 big_ord_recr /= -!addrA; congr (_ + _). +move: (odd_double_half n); rewrite no add1n => nE. +by rewrite nE -{1}nE. +Qed. + +Lemma increasing_euler_seq : increasing_seq euler_seq. +Proof. +apply/increasing_seqP. +case=> [|n]; first by rewrite euler_seq0 euler_seq1 {1}(_ : 1 = 1%:R) // ltr_nat /u_. +rewrite -(@ltr_pmul2l _ (((n.+2%:R - 1) / n.+2%:R) ^+ n.+2)); last first. + apply/exprn_gt0/divr_gt0; last by rewrite ltr0n. + by rewrite subr_gt0 {1}(_ : 1 = 1%:R) // ltr_nat. +rewrite [X in X < _](_ : _ = (n.+2%:R - 1) / n.+2%:R); last first. + rewrite {1}/u_ exprS -[RHS]mulr1 -3!mulrA; congr (_ * _). + rewrite -mulrA; congr (_ * _). + rewrite (_ : _ / n.+2%:R = (1 + 1 / n.+1%:R) ^-1); last first. + rewrite -{4}(@divrr _ n.+1%:R) ?unitfE ?pnatr_eq0 // -mulrDl. + by rewrite invf_div {2 6}(_ : 1 = 1%:R) // -natrD -natrB // subn1 addn1. + by rewrite exprVn mulVr // unitfE expf_eq0 /= paddr_eq0 //= oner_eq0. +rewrite [X in _ < X](_ : _ = ((n.+2%:R ^+ 2 - 1) / n.+2%:R ^+ 2) ^+ n.+2); last first. + rewrite /u_ /=. + rewrite -{4}(@divrr _ n.+2%:R) ?unitfE ?pnatr_eq0 // -mulrDl. + rewrite -exprMn_comm; last by rewrite /GRing.comm mulrC. + congr (_ ^+ _); rewrite mulrACA -subr_sqr expr1n; congr (_ * _). + by rewrite -invrM // unitfE pnatr_eq0. +rewrite mulrBl divrr ?unitfE ?pnatr_eq0 // mulrBl. +rewrite divrr ?unitfE ?expf_eq0 /= ?pnatr_eq0 //. +rewrite exprBn_comm; last by rewrite /GRing.comm mulrC. +rewrite big_ord_recl 2!expr0 expr1n bin0 mulr1n 2![in X in _ < X]mul1r. +rewrite big_ord_recl 2!expr1 expr1n bin1 [in X in _ < X]mul1r mulN1r. +rewrite (_ : -1 / _ *+ _ = -1 / n.+2%:R); last first. + rewrite 2!mulN1r mulNrn; congr (- _). + rewrite expr2 invrM ?unitfE ?pnatr_eq0 //. + rewrite -mulrnAr -[RHS]mulr1; congr (_ * _). + by rewrite -mulr_natl divrr // unitfE pnatr_eq0. +rewrite addrA mulN1r div1r -ltr_subl_addl subrr. +pose F : 'I_n.+1 -> R := + fun i => (-1) ^+ i.+2 * n.+2%:R ^- 2 ^+ i.+2 *+ 'C(n.+2, i.+2). +rewrite (eq_bigr F); last first. + by move=> i _; congr (_ *+ _); rewrite /= expr1n mulr1. +rewrite (sum_group_by_2 n.+1 + (fun i => ((-1) ^+ i.+2 * n.+2%:R ^- 2 ^+ i.+2 *+ 'C(n.+2, i.+2)))). +move: n => [|n'] in F *. + by rewrite /= big_ord0 add0r binn mulr1n mulr_gt0// -signr_odd/= expr0. +set n := n'.+1. +set G := BIG_F. +have G_gt0 : forall i, 0 < G i. + move=> /= i; rewrite /G. + rewrite -signr_odd /= negbK odd_double expr0 mul1r. + rewrite -signr_odd /= negbK odd_double /= expr1 mulN1r. + rewrite mulNrn (@exprSr _ _ i.*2.+2) -mulrnAr -mulr_natr -mulrBr. + rewrite mulr_gt0 // ?exprn_gt0 //. + rewrite subr_gt0 -mulr_natr ltr_pdivr_mull // -natrX -natrM. + move: (@mul_bin_left n.+2 i.*2.+2). + move/(congr1 (fun x => x%:R : R)). + move/(congr1 (fun x => (i.*2.+3)%:R^-1 * x)). + rewrite natrM mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r => ->. + rewrite 2!natrM mulrA. + have ? : (i.*2.+1 < n.+2)%nat. + move: (ltn_ord i). + rewrite 3!ltnS -(@leq_pmul2r 2) // !muln2 => /leq_trans; apply. + case/boolP : (odd n') => on'. + move: (odd_geq n' on'); rewrite leqnn => /esym. + by move/leq_trans; apply; rewrite leqnSn. + by move: (@odd_geq n' n on') => <-; rewrite leqnSn. + rewrite ltr_pmul2r ?ltr0n ?bin_gt0 // ltr_pdivr_mull // -natrM ltr_nat. + rewrite -(@ltn_add2r i.*2.+2) subnK // ltn_addr // -{1}(mul1n n.+2) -mulnn. + by rewrite mulnA ltn_mul2r /= mulSn addSn ltnS addSn. +have sum_G_gt0 : 0 < \big[+%R/0]_i G i. + rewrite {1}(_ : 0 = \big[+%R/0]_(i < n.+1./2) 0); last by rewrite big1. + apply: (@lt_leif _ _ _ _ false). + rewrite (_ : false = [forall i : 'I_n.+1./2, false]); last first. + apply/idP/forallP => //=; apply; exact: (@Ordinal _ 0). + apply: leif_sum => i _; exact/leifP/G_gt0. +case: ifPn => no; first by rewrite addr0. +rewrite addr_gt0 //= -signr_odd (negbTE no) expr0 mul1r. +by rewrite pmulrn_lgt0 ?bin_gt0 // exprn_gt0. +Qed. + +End euler_seq_increasing. + +Lemma cvg_euler_seq : cvg u_. +Proof. +apply: (@near_nondecreasing_is_cvg _ _ 4%:R). + by apply: nearW => x y ?; rewrite increasing_euler_seq. +by near=> n; rewrite ltW// euler_seq_lt4//; near: n. +Unshelve. all: by end_near. Qed. + +Lemma lim_euler_seq_gt2 : 2 < lim u_. +Proof. +apply: (@lt_le_trans _ _ (u_ 2%nat)). + by rewrite euler_seq2 ltr_pdivl_mulr // -natrM ltr_nat. +rewrite limr_ge//; first exact: cvg_euler_seq. +by near=> n; rewrite increasing_euler_seq; near: n. +Unshelve. all: by end_near. Qed. + +Definition euler_constant : R := lim euler_seq. + +Lemma euler_constant_gt0 : 0 < euler_constant. +Proof. by rewrite (lt_trans _ lim_euler_seq_gt2). Qed. + +Lemma euler_constant_neq1 : euler_constant != 1. +Proof. by rewrite eq_sym lt_eqF // (lt_trans _ lim_euler_seq_gt2) // ltr1n. Qed. + +End euler_constant. + +(* Density of R (i.e., for any x in R and 0 < a, there is an nonincreasing *) +(* sequence of Q.a that converges to x) *) +Section R_dense. + +(*Lemma ratr_fracq (G : realType) (p : int) (q : nat) : + (p + 1)%:~R / q.+1%:~R = @ratr [unitRingType of G] ((p + 1)%:Q / q.+1%:Q). +Proof. by rewrite rmorph_div /= ?ratr_int // unitfE. Qed.*) + +(* sequence in Q.a that converges to x \in R *) +Section rat_approx_def. +Variables (G : archiFieldType) (a x : G) (m : int). + +Fixpoint rat_approx (n : nat) : rat := + if n is n'.+1 then + if x - ratr (rat_approx n') * a < ratr (2 ^ n)%:Q^-1 * a then rat_approx n' + else rat_approx n' + (2 ^ n)%:Q^-1 + else m%:~R. +End rat_approx_def. + +Section rat_approx_archiFieldType. +Variables (G : archiFieldType) (a x : G) (m : int). +Hypothesis a0 : 0 < a. + +Let u := rat_approx a x m. + +Lemma nondecreasing_rat_approx : + (forall q, x != ratr q * a) -> nondecreasing_seq u. +Proof. +move=> /(_ _)/negPf xa_alg; apply/nondecreasing_seqP => n /=. +have [//||/eqP] := ltgtP; last by rewrite subr_eq -mulrDl -rmorphD/= xa_alg. +by rewrite ler_addl invr_ge0 // ler0z exprn_ge0. +Qed. + +Lemma rat_approx_dist (xma : x < (m + 1)%:~R * a) : + (forall q, x != ratr q * a) -> + forall n, x - ratr (u n) * a < ratr (2 ^ n)%:Q^-1 * a. +Proof. +move=> xqa; elim => [|n ih] /=. + rewrite expr0z invr1 ratr_int rmorph1 mul1r ltr_subl_addr. + by move: xma; rewrite intrD mulrDl mul1r addrC. +have [//| ? |/esym/eqP abs] := ltgtP (x - ratr (u n) * a) _. + rewrite rmorphD /= mulrDl opprD addrA ltr_sub_addr -mulrDl -rmorphD. + rewrite -mulr2n exprSz intrM invrM ?unitfE ?intr_eq0 ?expf_neq0//. + by rewrite -mulr_natr -(mulrA _ _ 2) mulVf ?intr_eq0// mulr1. +exfalso; move: abs; apply/negP. +by rewrite eq_sym subr_eq -mulrDl -rmorphD /=; exact: xqa. +Qed. + +Lemma rat_approx_ub (max : m%:~R * a < x) : + (forall q, x != ratr q * a) -> forall n, ratr (u n) * a <= x. +Proof. +move=> xa; elim => [|n unx] /=; first by rewrite ratr_int ltW. +have [//| ? |/esym/eqP abs] := ltgtP (x - ratr (u n) * a) _. +- by rewrite rmorphD /= mulrDl -lter_sub_addl ltW. +- exfalso; move: abs; apply/negP. + by rewrite eq_sym subr_eq -mulrDl -rmorphD /= xa. +Qed. + +End rat_approx_archiFieldType. + +Section rat_approx_realType. +Variables (R : realType) (a x : R) (m : int). +Hypothesis a0 : 0 < a. +Hypothesis xma : x < (m + 1)%:~R * a. +Hypothesis max : m%:~R * a < x. + +Let u := rat_approx a x m. + +Lemma is_cvg_rat_approx (xa : (forall q, x != ratr q * a)) : + cvg (ratr \o u : _ -> R^o). +Proof. +apply: nondecreasing_is_cvg. + by apply/nondecreasing_seqP => n; rewrite ler_rat; apply: nondecreasing_rat_approx. +exists (x / a) => n; rewrite ler_pdivl_mulr //= => -[k _ <-]. +by apply: rat_approx_ub => //; exact/ltW. +Qed. + +Lemma cvg_rat_approx (xa : (forall q, x != ratr q * a)) : + (fun n => ratr (u n) * a : R^o) --> (x : R^o). +Proof. +apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n. +move: (rat_approx_ub max xa n); rewrite -/u => u_ub. +rewrite [X in X < _](_ : _ = `|x - ratr (u n) * a|%R) //. +rewrite ger0_norm // ?subr_ge0 //. +move: (rat_approx_dist xma xa); rewrite -/u => /(_ n)/lt_le_trans ->//. +rewrite -ler_pdivl_mulr // ltW //. +rewrite [X in X < _](_ : _ = `| (0 - ratr ((2 ^ n)%:Q)^-1) : R^o |); last first. + by rewrite distrC subr0 ger0_norm // ler0q invr_ge0// ler0z // -exprnP exprn_ge0. +near: n. +have cvg_geo : (fun n : nat => ratr ((2 ^ n)%:~R)^-1 : R^o) --> (0 : R^o). + rewrite (_ : (fun _ => _) = (fun n : nat => ratr (1%:~R / (2 ^ n)%:~R))); last first. + by rewrite funeqE => n; rewrite div1r. + rewrite (_ : (fun _ => _) = geometric 1 (2 ^ -1)); last first. + rewrite funeqE => n; rewrite /geometric /ratr. + rewrite coprimeq_num ?absz1 ?coprime1n // gtr0_sg ?exprn_gt0 // mul1r. + rewrite coprimeq_den ?absz1 ?coprime1n // expfz_eq0 andbF div1r. + by rewrite ger0_norm // ?exprn_ge0 // -exprz_pintl //= mul1r exprVn. + apply: cvg_geometric. + by rewrite exprN1 gtr0_norm// invr_lt1// ?ltr1n// unitfE. +have ea0 : 0 < e%:num / a by rewrite divr_gt0. +by move/cvg_distP : cvg_geo => /(_ _ ea0) /=; rewrite near_map. +Unshelve. all: by end_near. Qed. + +Lemma start_rat_approx : (forall q, x != ratr q * a) -> + {m : int | m%:~R * a < x < (m + 1)%:~R * a}. +Proof. +move=> xa; exists (floor (x / a)); apply/andP; split; last first. + by rewrite -ltr_pdivr_mulr // intrD -RfloorE lt_succ_Rfloor. +rewrite -ltr_pdivl_mulr // lt_neqAle -{2}RfloorE Rfloor_le andbT. +apply/negP => /eqP H. +move: (xa (floor (x / a))%:~R) => /negP; apply; apply/eqP. +by rewrite ratr_int H -mulrA mulVr ?mulr1 // unitfE gt_eqF. +Qed. + +End rat_approx_realType. + +Lemma R_dense_corollary (R : realType) (a x : R) (a0 : 0 < a) : + exists u : rat ^nat, nondecreasing_seq u /\ + cvg (ratr \o u : _ -> R^o) /\ lim (fun n => ratr (u n) * a : R^o) = x. +Proof. +have [[q qxa]|/forallNP xa] := pselect (exists q, x = ratr q * a). + exists (fun=> q); split => //; split. + by rewrite (_ : _ \o _ = cst (ratr q)) //; exact: is_cvg_cst. + by rewrite -qxa; exact: lim_cst. +have {}xa : forall q, x != ratr q * a by move=> q; apply/eqP/xa. +have [m /andP[max xma]] := start_rat_approx a0 xa. +set x0 := m%:~R * a; exists (rat_approx a x m). +split; first exact: nondecreasing_rat_approx. +split; first by apply: is_cvg_rat_approx => //; rewrite addrC in xma => //; exact/ltW. +by apply/cvg_lim => //; apply/cvg_rat_approx => //; exact/ltW. +Qed. + +End R_dense.