small theory about arithmetic and geometric sequences

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
 

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.
 

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,21 +144,31 @@ 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.
    by apply: cvg_comp; apply: cvg_addnr.
 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,14 +288,15 @@ 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.
 
 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).