From 60ff32fb53feaa5162d1b0fce1a0e4e6c255ff41 Mon Sep 17 00:00:00 2001 From: IshYosh <103252572+IshiguroYoshihiro@users.noreply.github.com> Date: Wed, 10 Apr 2024 12:07:53 +0900 Subject: [PATCH] Bigcap series addn (#1196) --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 7 +++++++ classical/classical_sets.v | 28 +++++++++++++++++++++++++++- theories/sequences.v | 11 +++++++++++ 3 files changed, 45 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index aa01301cb..243eada92 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 1363854d9..a892748e9 100644 --- a/classical/classical_sets.v +++ b/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,6 +404,8 @@ 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. @@ -403,6 +413,8 @@ 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. diff --git a/theories/sequences.v b/theories/sequences.v index 15e2b45df..b4648f70d 100644 --- a/theories/sequences.v +++ b/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 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.