Bigcap series addn (#1196)

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -14,6 +14,13 @@
   + definition `subset_sigma_subadditive`
   + factory `isSubsetOuterMeasure`
 
+- in file `classical_sets.v`
+  + notations `\bigcup_(i >= n) F i` and `\bigcap_(i >= n) F i`
+  + lemmas `bigcup_addn`, `bigcap_addn`
+
+- in file `sequences.v`
+  + lemma `nneseries_addn`
+
 ### Changed
 
 ### Renamed

classical/classical_sets.v

@@ -56,7 +56,7 @@ From mathcomp Require Import mathcomp_extra boolp.
 (* |                 trivIset D F |==| F is a sequence of pairwise disjoint   *)
 (* |                              |  | sets indexed over the domain D         *)
 (*                                                                            *)
-(* Detailed documentation:                                                                   *)
+(* Detailed documentation:                                                    *)
 (* ## Sets                                                                    *)
 (* ```                                                                        *)
 (*                       set T == type of sets on T                           *)
@@ -94,11 +94,13 @@ From mathcomp Require Import mathcomp_extra boolp.
 (*                                index satisfies P                           *)
 (*           \bigcup_(i : T) F == union of the family F indexed on T          *)
 (*           \bigcup_(i < n) F := \bigcup_(i in `I_n) F                       *)
+(*          \bigcup_(i >= n) F := \bigcup_(i in [set i | i >= n]) F           *)
 (*                 \bigcup_i F == same as before with T left implicit         *)
 (*          \bigcap_(i in P) F == intersection of the elements of the family  *)
 (*                                F whose index satisfies P                   *)
 (*           \bigcap_(i : T) F == union of the family F indexed on T          *)
 (*           \bigcap_(i < n) F := \bigcap_(i in `I_n) F                       *)
+(*          \bigcap_(i >= n) F := \bigcap_(i in [set i | i >= n]) F           *)
 (*                 \bigcap_i F == same as before with T left implicit         *)
 (*                smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A  *)
 (*                   A `<=` B <-> A is included in B                          *)
@@ -251,6 +253,9 @@ Reserved Notation "\bigcup_ ( i : T ) F"
 Reserved Notation "\bigcup_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \bigcup_ ( i  <  n ) '/  '  F ']'").
+Reserved Notation "\bigcup_ ( i >= n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcup_ ( i  >=  n ) '/  '  F ']'").
 Reserved Notation "\bigcup_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \bigcup_ i '/  '  F ']'").
@@ -263,6 +268,9 @@ Reserved Notation "\bigcap_ ( i : T ) F"
 Reserved Notation "\bigcap_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \bigcap_ ( i  <  n ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i >= n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcap_ ( i  >=  n ) '/  '  F ']'").
 Reserved Notation "\bigcap_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \bigcap_ i '/  '  F ']'").
@@ -396,13 +404,17 @@ Notation "\bigcup_ ( i : T ) F" :=
   (\bigcup_(i in @setT T) F) : classical_set_scope.
 Notation "\bigcup_ ( i < n ) F" :=
   (\bigcup_(i in `I_n) F) : classical_set_scope.
+Notation "\bigcup_ ( i >= n ) F" :=
+  (\bigcup_(i in [set i | (n <= i)%N]) F) : classical_set_scope.
 Notation "\bigcup_ i F" := (\bigcup_(i : _) F) : classical_set_scope.
 Notation "\bigcap_ ( i 'in' P ) F" :=
   (bigcap P (fun i => F)) : classical_set_scope.
 Notation "\bigcap_ ( i : T ) F" :=
   (\bigcap_(i in @setT T) F) : classical_set_scope.
 Notation "\bigcap_ ( i < n ) F" :=
   (\bigcap_(i in `I_n) F) : classical_set_scope.
+Notation "\bigcap_ ( i >= n ) F" :=
+  (\bigcap_(i in [set i | (n <= i)%N]) F) : classical_set_scope.
 Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.
 
 Notation "A `<=` B" := (subset A B) : classical_set_scope.
@@ -2153,6 +2165,20 @@ move=> n m nm; rewrite big_mkcond [in X in _ `<=` X]big_mkcond/=.
 exact: (@subset_bigsetI (fun i => if P i then F i else _)).
 Qed.
 
+Lemma bigcup_addn F n : \bigcup_i F (n + i) = \bigcup_(i >= n) F i.
+Proof.
+rewrite eqEsubset; split => [x /= [m _ Fmnx]|x /= [m nm Fmx]].
+- by exists (n + m) => //=; rewrite leq_addr.
+- by exists (m - n) => //; rewrite subnKC.
+Qed.
+
+Lemma bigcap_addn F n : \bigcap_i F (n + i) = \bigcap_(i >= n) F i.
+Proof.
+rewrite eqEsubset; split=> [x /= Fnx m nm|x /= nFx m _].
+- by rewrite -(subnKC nm); exact: Fnx.
+- exact/nFx/leq_addr.
+Qed.
+
 End bigop_nat_lemmas.
 
 Definition is_subset1 {T} (A : set T) := forall x y, A x -> A y -> x = y.

theories/sequences.v

@@ -1991,6 +1991,17 @@ rewrite nneseries_sum_nat; last by move=> ? ?; case: ifP => // /f_ge0.
 by apply: eq_bigr => j _; case: ifP => //; rewrite eseries0.
 Qed.
 
+Lemma nneseries_addn {R : realType} (f : (\bar R)^nat) k :
+  (forall i, 0 <= f i) ->
+  \sum_(i <oo) f (i + k)%N = \sum_(k <= i <oo) f i.
+Proof.
+move=> f0; have /cvg_ex[/= l fl] : cvg (\sum_(k <= i < n) f i @[n --> \oo]).
+  by apply: ereal_nondecreasing_is_cvgn => m n mn; exact: lee_sum_nneg_natr.
+rewrite (cvg_lim _ fl)//; apply/cvg_lim => //=.
+move: fl; rewrite -(cvg_shiftn k) /=.
+by under eq_fun do rewrite -{1}(add0n k)// big_addn addnK.
+Qed.
+
 Lemma lte_lim (R : realFieldType) (u : (\bar R)^nat) (M : R) :
   nondecreasing_seq u -> cvgn u -> M%:E < limn u ->
   \forall n \near \oo, M%:E <= u n.