From 687806ca79ccba3ab20efe3045d764f7e64b8016 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 15 Nov 2024 10:33:49 +0900 Subject: [PATCH 1/2] generalize some lemmas for series --- classical/mathcomp_extra.v | 9 +++++ theories/sequences.v | 68 +++++++++++++++++++++----------------- 2 files changed, 46 insertions(+), 31 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f0ecf3733..47202c242 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -539,3 +539,12 @@ Qed. Definition sigT_fun {I : Type} {X : I -> Type} {T : Type} (f : forall i, X i -> T) (x : {i & X i}) : T := (f (projT1 x) (projT2 x)). + +Lemma eq_lt_total {disp : unit} {T : orderType disp} (x y : T) : + [|| x == y, (x < y)%O | (y < x)%O]. +Proof. by case/boolP: (x == y)=> // ?; apply/orP; right; exact:lt_total. Qed. + +Lemma le_lt_total {disp : unit} {T : orderType disp} (x y : T) : + (x <= y)%O || (y < x)%O. +Proof. by rewrite le_eqVlt -orbA eq_lt_total. Qed. + diff --git a/theories/sequences.v b/theories/sequences.v index 1e803af79..0526b9317 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -951,13 +951,15 @@ rewrite -(subrr (limn (series u_))). by apply: cvgB => //; rewrite ?cvg_shiftS. Qed. -Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) : +Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) m : (forall n, P n -> 0 <= u_ n)%R -> - nondecreasing_seq (fun n=> \sum_(0 <= k < n | P k) u_ k)%R. + nondecreasing_seq (fun n=> \sum_(m <= k < n | P k) u_ k)%R. Proof. move=> u_ge0; apply/nondecreasing_seqP => n. -rewrite [in leRHS]big_mkcond [in leRHS]big_nat_recr//=. -by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +have/orP[mn|] := le_lt_total m n. + rewrite [in leRHS]big_mkcond [in leRHS]big_nat_recr//=. + by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +by move=> /[dup] /ltW *; rewrite !big_geq. Qed. Lemma increasing_series (R : numFieldType) (u_ : R ^nat) : @@ -1546,8 +1548,8 @@ Proof. by move=> ?; apply/cvg_ex; eexists; apply: ereal_nonincreasing_cvgn. Qed. (* NB: see also nondecreasing_series *) Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat) - (P : pred nat) : (forall n, P n -> 0 <= u_ n) -> - nondecreasing_seq (fun n => \sum_(0 <= i < n | P i) u_ i). + (P : pred nat) N : (forall n, P n -> 0 <= u_ n) -> + nondecreasing_seq (fun n => \sum_(N <= i < n | P i) u_ i). Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) : @@ -1558,12 +1560,14 @@ Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N : \sum_(N <= i n /=; apply: big_nat_widenl. Qed. -Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondl. Qed. -Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondr. Qed. Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : @@ -1571,8 +1575,8 @@ Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : \sum_(N <= i efg; apply/congr_lim/funext => n; exact: eq_bigr. Qed. -Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) : - P =1 Q -> \sum_(i \sum_(N <= i efg; apply/congr_lim/funext => n; apply: eq_bigl. Qed. Arguments eq_eseriesl {R P} Q. @@ -1617,9 +1621,9 @@ Qed. End ereal_series. -Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : +Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) {m} k : (forall n, P n -> 0 <= u_ n) -> - \sum_(0 <= i < k | P i) u_ i <= \sum_(i -> //. by apply: ereal_sup_ubound; exists k. @@ -1723,13 +1727,13 @@ by apply/congr_lim/funext => /= n; rewrite ge0_sume_distrr. Qed. Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat) - (P Q : pred nat) : + (P Q : pred nat) m : (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> - (\sum_(i f0 g0; rewrite /adde_def !negb_and; apply/andP; split; apply/orP. -- by right; apply/eqP => Qg; have := nneseries_ge0 0 g0; rewrite Qg. -- by left; apply/eqP => Pf; have := nneseries_ge0 0 f0; rewrite Pf. +- by right; apply/eqP => Qg; have := nneseries_ge0 m g0; rewrite Qg. +- by left; apply/eqP => Pf; have := nneseries_ge0 m f0; rewrite Pf. Qed. Lemma __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) : @@ -1962,35 +1966,37 @@ apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. Qed. -Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) : +Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) N : (forall i, P i -> 0 <= f i) -> (forall i, P i -> 0 <= g i) -> - \sum_(i f_eq0 g_eq0. -transitivity (limn (fun n => \sum_(0 <= i < n | P i) f i + - \sum_(0 <= i < n | P i) g i)). +transitivity (limn (fun n => \sum_(N <= i < n | P i) f i + + \sum_(N <= i < n | P i) g i)). by apply/congr_lim/funext => n; rewrite big_split. rewrite limeD /adde_def //=; do ? exact: is_cvg_nneseries. by rewrite ![_ == -oo]gt_eqF ?andbF// (@lt_le_trans _ _ 0) ?[_ < _]real0// nneseries_ge0. Qed. -Lemma nneseries_sum_nat (R : realType) n (f : nat -> nat -> \bar R) : +Lemma nneseries_sum_nat (R : realType) m n (f : nat -> nat -> \bar R) N : (forall i j, 0 <= f i j) -> - \sum_(j f0; elim: n => [|n IHn]. by rewrite big_geq// eseries0// => i; rewrite big_geq. -rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. -by apply/congr_lim/funext => m; apply: eq_bigr => i _; rewrite big_nat_recr. +have/orP[mn|nm]:= le_lt_total m n. + rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. + by apply/congr_lim/funext => ?; apply: eq_bigr => i _; rewrite big_nat_recr. +by rewrite big_geq// eseries0// => i; rewrite big_geq. Qed. Lemma nneseries_sum I (r : seq I) (P : {pred I}) [R : realType] - [f : I -> nat -> \bar R] : (forall i j, P i -> 0 <= f i j) -> - \sum_(j nat -> \bar R] N : (forall i j, P i -> 0 <= f i j) -> + \sum_(N <= j f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr. by rewrite big_nil eseries0// => i; rewrite big_nil. From 56dbde781ce8e37df07f4a26cb7225ce7625bba6 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 15 Nov 2024 10:43:48 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 11 +++++++++++ classical/mathcomp_extra.v | 1 - 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 312bf7076..477025a9f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,9 @@ ### Added +- in file `mathcomp_extra.v`, + + lemmas `eq_lt_total`, `le_lt_total` + - file `Rstruct_topology.v` - package `coq-mathcomp-reals` depending on `coq-mathcomp-classical` @@ -182,6 +185,14 @@ * definition `mfun` * lemmas `mfun_rect`, `mfun_valP`, `mfuneqP` +- in `sequences.v`, + + generalized indexing from zero-based ones (`0 <= k < n` and `k // ?; apply/orP; right; exact:lt_total. Qed. Lemma le_lt_total {disp : unit} {T : orderType disp} (x y : T) : (x <= y)%O || (y < x)%O. Proof. by rewrite le_eqVlt -orbA eq_lt_total. Qed. -