diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e66ff73374..fbd713a931 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -19,6 +19,14 @@ + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`, `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`, `lee_subl_addr`, `lte_spaddr` +- in `normedtype.v`, lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`. +- in `sequences.v`: + + definitions `arithmetic`, `geometric`, `geometric_invn` + + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`, + `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`, + `geometric_seriesE`, `cvg_geometric_series`, + `is_cvg_geometric_series`. + + ### Changed @@ -152,6 +160,12 @@ + `derivable_locallyP` -> `derivable_nbhsP` + `derivable_locallyx` -> `derivable_nbhsx` + `derivable_locallyxP` -> `derivable_nbhsxP` +- in `sequences.v`, + + `cvg_comp_subn` -> `cvg_centern`, + + `cvg_comp_addn` -> `cvg_shiftn`, + + `telescoping` -> `telescope` + + `sderiv1_series` -> `seriesSB` + + `telescopingS0` -> `eq_sum_telescope` ### Removed diff --git a/theories/normedtype.v b/theories/normedtype.v index 99dda4b334..8497f242c5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2759,6 +2759,14 @@ rewrite !near_simpl /=; near=> a b => /=; rewrite opprD addrACA. by rewrite normm_lt_split //; [near: a|near: b]; apply: cvg_dist. Grab Existential Variables. all: end_near. Qed. +Lemma natmul_continuous n : continuous (fun x : V => x *+ n). +Proof. +case: n => [|n] x; first exact: cvg_cst. +apply/cvg_distP=> _/posnumP[e]; rewrite !near_simpl /=; near=> a. +rewrite -mulrnBl normrMn -mulr_natr -ltr_pdivl_mulr//. +by near: a; apply: cvg_dist. +Grab Existential Variables. all: end_near. Qed. + Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). Proof. move=> [k x]; apply/cvg_distP=> _/posnumP[e]. @@ -2854,6 +2862,12 @@ Proof. by move=> /cvgN /cvgP. Qed. Lemma is_cvgNE f : cvg ((- f) @ F) = cvg (f @ F). Proof. by rewrite propeqE; split=> /cvgN; rewrite ?opprK => /cvgP. Qed. +Lemma cvgMn f n a : f @ F --> a -> ((@GRing.natmul _)^~n \o f) @ F --> a *+ n. +Proof. by move=> ?; apply: continuous_cvg => //; exact: natmul_continuous. Qed. + +Lemma is_cvgMn f n : cvg (f @ F) -> cvg (((@GRing.natmul _)^~n \o f) @ F). +Proof. by move=> /cvgMn /cvgP. Qed. + Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. Proof. by move=> ? ?; apply: continuous2_cvg => //; exact: add_continuous. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 0fa8a9988c..c26889bf68 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -17,6 +17,8 @@ Require Import classical_sets posnum topology normedtype landau derive forms. (* R ^nat == notation for sequences, *) (* i.e., functions of type nat -> R *) (* harmonic == harmonic sequence *) +(* arithmetic == arithmetic sequence *) +(* geometric == geometric sequence *) (* series u_ == the sequence of partial sums of u_ *) (* [sequence u_n]_n == the sequence of general element u_n *) (* [series u_n]_n == the series of general element u_n *) @@ -121,6 +123,8 @@ Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter). Section sequences_patched. (* TODO: generalizations to numDomainType *) +Section NatShift. + Variables (N : nat) (V : topologicalType). Implicit Types (f : nat -> V) (u : V ^nat) (l : V). @@ -140,7 +144,7 @@ by rewrite propeqE; split; [rewrite cvg_restrict|rewrite -(cvg_restrict f)] => /cvgP. Qed. -Lemma cvg_comp_subn u_ l : ([sequence u_ (n - N)%N]_n --> l) = (u_ --> l). +Lemma cvg_centern u_ l : ([sequence u_ (n - N)%N]_n --> l) = (u_ --> l). Proof. rewrite propeqE; split; last by apply: cvg_comp; apply: cvg_subnr. gen have cD : u_ l / u_ --> l -> (fun n => u_ (n + N)%N) --> l. @@ -148,13 +152,23 @@ gen have cD : u_ l / u_ --> l -> (fun n => u_ (n + N)%N) --> l. by move=> /cD /=; under [X in X --> l]funext => n do rewrite addnK. Qed. -Lemma cvg_comp_addn u_ l : ([sequence u_ (n + N)%N]_n --> l) = (u_ --> l). +Lemma cvg_shiftn u_ l : ([sequence u_ (n + N)%N]_n --> l) = (u_ --> l). Proof. rewrite propeqE; split; last by apply: cvg_comp; apply: cvg_addnr. -rewrite -[X in X -> _]cvg_comp_subn; apply: cvg_trans => /=. +rewrite -[X in X -> _]cvg_centern; apply: cvg_trans => /=. by apply: near_eq_cvg; near=> n; rewrite subnK//; near: n; exists N. Grab Existential Variables. all: end_near. Qed. +End NatShift. + +Variables (V : topologicalType). + +Lemma cvg_shiftS u_ (l : V) : ([sequence u_ n.+1]_n --> l) = (u_ --> l). +Proof. +suff -> : [sequence u_ n.+1]_n = [sequence u_(n + 1)%N]_n by rewrite cvg_shiftn. +by rewrite funeqE => n/=; rewrite addn1. +Qed. + End sequences_patched. Section sequences_R_lemmas_realFieldType. @@ -274,6 +288,7 @@ Section partial_sum. Variables (V : zmodType) (u_ : V ^nat). Definition series : V ^nat := [sequence \sum_(k < n) u_ k]_n. +Definition telescope : V ^nat := [sequence u_ n.+1 - u_ n]_n. Lemma seriesSr n : series n.+1 = series n + u_ n. Proof. by rewrite /series/= big_ord_recr/=. Qed. @@ -281,7 +296,7 @@ Proof. by rewrite /series/= big_ord_recr/=. Qed. Lemma seriesS n : series n.+1 = u_ n + series n. Proof. by rewrite addrC seriesSr. Qed. -Lemma sderiv1_series (n : nat) : series n.+1 - series n = u_ n. +Lemma seriesSB (n : nat) : series n.+1 - series n = u_ n. Proof. by rewrite seriesS addrK. Qed. Lemma seriesEord : series = [sequence \sum_(k < n) u_ k]_n. @@ -308,8 +323,20 @@ Proof. by rewrite sub_series_geq// -addnn leq_addl. Qed. End partial_sum. Arguments series {V} u_ n : simpl never. +Arguments telescope {V} u_ n : simpl never. Notation "[ 'series' E ]_ n" := (series [sequence E]_n) : ring_scope. +Lemma telescopeK (V : zmodType) (u_ : V ^nat) : + series (telescope u_) = [sequence u_ n - u_ 0%N]_n. +Proof. by rewrite funeqE => n; rewrite seriesEnat/= telescope_sumr. Qed. + +Lemma seriesK (V : zmodType) : cancel (@series V) telescope. +Proof. move=> ?; exact/funext/seriesSB. Qed. + +Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n : + u_ n = u_ 0%N + series (telescope u_) n. +Proof. by rewrite telescopeK/= addrC addrNK. Qed. + (* TODO: port to mathcomp *) (* missing mathcomp lemmas *) Lemma ler_sum_nat (R : numDomainType) (m n : nat) (F G : nat -> R) : @@ -408,7 +435,7 @@ Lemma near_nondecreasing_is_cvg (u_ : (R^o) ^nat) (M : R) : cvg u_. Proof. move=> [k _ u_nd] [k' _ u_M]; suff : cvg [sequence u_ (n + maxn k k')%N]_n. - by case/cvg_ex => /= l; rewrite cvg_comp_addn => ul; apply/cvg_ex; exists l. + by case/cvg_ex => /= l; rewrite cvg_shiftn => ul; apply/cvg_ex; exists l. apply (@nondecreasing_is_cvg _ M) => [/= ? ? ? | ?]. by rewrite u_nd ?leq_add2r ?(leq_trans (leq_maxl _ _) (leq_addl _ _))//. by rewrite u_M // (leq_trans (leq_maxr _ _) (leq_addl _ _)). @@ -522,17 +549,6 @@ Grab Existential Variables. all: end_near. Qed. End cesaro. -Definition telescoping (R : numDomainType) (u_ : R^o ^nat) := - [sequence u_ n.+1 - u_ n]_n. - -Lemma telescopingS0 (R : numDomainType) (u_ : R^o ^nat) n : - u_ n.+1 = u_ O + \sum_(i < n.+1) (telescoping u_) i. -Proof. -apply/eqP; rewrite addrC -subr_eq; apply/eqP. -elim: n => [|n ih]; first by rewrite big_ord_recl big_ord0 addr0. -by rewrite big_ord_recr /= -ih addrCA (addrC (u_ n.+1)) addrK. -Qed. - Section cesaro_converse. Variable R : archiFieldType. @@ -552,10 +568,10 @@ by rewrite lef_pinv // ?ler_nat // posrE // ltr0n. Grab Existential Variables. all: end_near. Qed. Lemma cesaro_converse (u_ : R^o ^nat) (l : R^o) : - telescoping u_ =o_\oo (harmonic) -> + telescope u_ =o_\oo harmonic -> arithmetic_mean u_ --> l -> u_ --> l. Proof. -pose a_ := telescoping u_ => a_o u_l. +pose a_ := telescope u_ => a_o u_l. suff abel : forall n, u_ n - arithmetic_mean u_ n = \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1. suff K : u_ - arithmetic_mean u_ --> (0 : R^o). @@ -570,7 +586,7 @@ suff abel : forall n, fun n => n.+1%:R^-1 * \sum_(k < n) k.+1%:R * a_ k); last first. rewrite funeqE => n; rewrite big_add1 /= big_mkord /= big_distrr /=. by apply eq_bigr => i _; rewrite mulrCA mulrA. - have {a_o}a_o : [sequence n.+1%:R * telescoping u_ n]_n --> (0 : R^o). + have {a_o}a_o : [sequence n.+1%:R * telescope u_ n]_n --> (0 : R^o). apply: (@eqolim0 R nat [normedModType R of R^o] eventually_filterType). rewrite a_o. set h := 'o_[filter of \oo] harmonic. @@ -585,10 +601,10 @@ case => [|n]. rewrite /arithmetic_mean /= invr1 mul1r /series /= big_ord_recl !big_ord0. by rewrite addr0 subrr big_nil. rewrite /arithmetic_mean /= /series /= big_ord_recl /=. -under eq_bigr do rewrite /bump /= add1n telescopingS0. +under eq_bigr do rewrite /bump /= add1n eq_sum_telescope. rewrite big_split /= big_const card_ord iter_addr addr0 addrA -mulrS mulrDr. rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA. -rewrite telescopingS0 (addrC (u_ O)) addrK. +rewrite eq_sum_telescope (addrC (u_ O)) addrK. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) \sum_(0 <= k < n.+1 | (k < i.+1)%N) a_ k); last first. by rewrite big_mkord; apply eq_bigr => i _; rewrite big_mkord -big_ord_widen. @@ -624,13 +640,13 @@ End cesaro_converse. Section series_convergence. Lemma cvg_series_cvg_0 (K : numFieldType) (V : normedModType K) (u_ : V ^nat) : - cvg (series u_) -> u_ --> (0 : V^o). + cvg (series u_) -> u_ --> (0 : V). Proof. move=> cvg_series. rewrite (_ : u_ = fun n => series u_ (n + 1)%nat - series u_ n); last first. - by rewrite funeqE => i; rewrite addn1 sderiv1_series. + by rewrite funeqE => i; rewrite addn1 seriesSB. rewrite -(subrr (lim (series u_))). -by apply: cvgD; rewrite ?cvg_comp_addn//; apply: cvgN. +by apply: cvgD; rewrite ?cvg_shiftn//; apply: cvgN. Qed. Lemma nondecreasing_series (R : numFieldType) (u_ : R^o ^nat) : @@ -640,8 +656,77 @@ move=> u_ge0; apply: nondecreasing_seqP => n. by rewrite /series/= big_ord_recr ler_addl. Qed. +Lemma increasing_series (R : numFieldType) (u_ : R^o ^nat) : + (forall n, 0 < u_ n) -> increasing_seq (series u_). +Proof. +move=> u_ge0; apply: increasing_seqP => n. +by rewrite /series/= big_ord_recr ltr_addl. +Qed. + End series_convergence. +Definition arithmetic (R : zmodType) a z : R^o ^nat := [sequence a + z *+ n]_n. +Arguments arithmetic {R} a z n /. + +Lemma mulrn_arithmetic (R : zmodType) : @GRing.natmul R = arithmetic 0. +Proof. by rewrite funeq2E => z n /=; rewrite add0r. Qed. + +Definition geometric (R : fieldType) a z : R^o ^nat := [sequence a * z ^+ n]_n. +Arguments geometric {R} a z n /. + +Lemma exprn_geometric (R : fieldType) : (@GRing.exp R) = geometric 1. +Proof. by rewrite funeq2E => z n /=; rewrite mul1r. Qed. + +Lemma cvg_arithmetic (R : archiFieldType) a (z : R^o) : + z > 0 -> arithmetic a z --> +oo. +Proof. +move=> z_gt0; apply/cvgPpinfty => _ /posnumP[A]; near=> n => /=. +rewrite -ler_subl_addl -mulr_natl -ler_pdivr_mulr//; set x := (X in X <= _). +rewrite ler_normlW// ltW// (lt_le_trans (archi_boundP _))// ler_nat. +by near: n; apply: nbhs_infty_ge. +Grab Existential Variables. all: end_near. Qed. + +(* Cyril: I think the shortest proof would rely on cauchy completion *) +Lemma cvg_expr (R : archiFieldType) (z : R) : + `|z| < 1 -> (@GRing.exp R z : R^o^nat) --> (0 : R^o). +Proof. +move=> Nz_lt1; apply: cvg_dist0; pose t := (1 - `|z|). +pose oo_filter := eventually_filterType. (* Cyril: fixme *) +apply: (@squeeze _ _ (cst 0) _ (t^-1 *: harmonic) oo_filter); last 2 first. +- exact: (@cvg_cst [topologicalType of R^o]). +- by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic). +near=> n; rewrite normr_ge0 normrX/= ler_pdivl_mull ?subr_gt0//. +rewrite -(@ler_pmul2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl. +have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n. +rewrite exprDn (bigD1 (inord 1)) ?inordK// subn1 expr1 bin1 ler_addl sumr_ge0//. +by move=> i; rewrite ?(mulrn_wge0, mulr_ge0, exprn_ge0, subr_ge0)// ltW. +Grab Existential Variables. all: end_near. Qed. + +Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 -> + series (geometric a z) = [sequence a * (1 - z ^+ n) / (1 - z)]_n. +Proof. +rewrite funeqE => z_neq1 n. +apply: (@mulIf _ (1 - z)); rewrite ?mulfVK ?subr_eq0 1?eq_sym//. +rewrite seriesEnat !mulrBr [in LHS]mulr1 mulr_suml -opprB -sumrB. +by under eq_bigr do rewrite -mulrA -exprSr; rewrite telescope_sumr// opprB. +Qed. + +Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> + series (geometric a z) --> (a * (1 - z)^-1 : R^o). +Proof. +move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//. +have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1. +by apply: cvgMl; apply: cvgMr; apply: cvgB; [apply: cvg_cst|apply: cvg_expr]. +Qed. + +Lemma cvg_geometric (R : archiFieldType) (a z : R) : `|z| < 1 -> + geometric a z --> (0 : R^o). +Proof. by move=> /cvg_geometric_series/cvgP/cvg_series_cvg_0. Qed. + +Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> + cvg (series (geometric a z)). +Proof. by move=> /cvg_geometric_series/cvgP; apply. Qed. + Definition normed_series_of (K : numDomainType) (V : normedModType K) (u_ : V ^nat) of phantom V^nat (series u_) : K^o ^nat := [series `|u_ n|]_n. @@ -736,7 +821,7 @@ have [Spoo|Spoo] := pselect (S +oo%E). case: Spoo => N _ uNoo; exists N => n Nn. by move: (nd_u_ _ _ Nn); rewrite uNoo lee_pinfty_eq => /eqP. have -> : l = +oo%E by rewrite /l /ereal_sup; exact: supremum_pinfty. - rewrite -(cvg_comp_addn N); set f := (X in X --> _). + rewrite -(cvg_shiftn N); set f := (X in X --> _). rewrite (_ : f = (fun=> +oo%E)); first exact: cvg_cst. by rewrite funeqE => n; rewrite /f /= Nu // leq_addl. have [Snoo|Snoo] := pselect (u_ = fun=> -oo%E).