Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

generalize indexing in lemmas for series #1397

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

generalize indexing in lemmas for series #1397

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
687806c
generalize some lemmas for series
t6s Nov 15, 2024
56dbde7
changelog
t6s Nov 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down Expand Up @@ -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 <oo`)
to `m <= k < n` and `m <= k <oo`
* lemmas `nondecreasing_series`, `ereal_nondecreasing_series`,
`eseries_mkcondl`, `eseries_mkcondr`, `eq_eseriesl`,
`nneseries_lim_ge`, `adde_def_nneseries`,
`nneseriesD`, `nneseries_sum_nat`, `nneseries_sum`

### Deprecated

- in `topology_structure.v`:
Expand Down
8 changes: 8 additions & 0 deletions classical/mathcomp_extra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -539,3 +539,11 @@ 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.
68 changes: 37 additions & 31 deletions theories/sequences.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down Expand Up @@ -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) :
Expand All @@ -1558,21 +1560,23 @@ Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N :
\sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i.
Proof. by apply/congr_lim/eq_fun => n /=; apply: big_nat_widenl. Qed.

Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q :
\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | Q i) if P i then f i else 0.
Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q N :
\sum_(N <= i <oo | P i && Q i) f i =
\sum_(N <= i <oo | Q i) if P i then f i else 0.
Proof. by apply/congr_lim/funext => n; rewrite big_mkcondl. Qed.

Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q :
\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0.
Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q N :
\sum_(N <= i <oo | P i && Q i) f i =
\sum_(N <= i <oo | P i) if Q i then f i else 0.
Proof. by apply/congr_lim/funext => n; rewrite big_mkcondr. Qed.

Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} :
(forall i, P i -> f i = g i) ->
\sum_(N <= i <oo | P i) f i = \sum_(N <= i <oo | P i) g i.
Proof. by move=> 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 <oo | P i) f i = \sum_(i <oo | Q i) f i.
Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) N :
P =1 Q -> \sum_(N <= i <oo | P i) f i = \sum_(N <= i <oo | Q i) f i.
Proof. by move=> efg; apply/congr_lim/funext => n; apply: eq_bigl. Qed.
Arguments eq_eseriesl {R P} Q.

Expand Down Expand Up @@ -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 <oo | P i) u_ i.
\sum_(m <= i < k | P i) u_ i <= \sum_(m <= i <oo | P i) u_ i.
Proof.
move/ereal_nondecreasing_series/ereal_nondecreasing_cvgn/cvg_lim => -> //.
by apply: ereal_sup_ubound; exists k.
Expand Down Expand Up @@ -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 <oo | P i) f i) +? (\sum_(i <oo | Q i) g i).
(\sum_(m <= i <oo | P i) f i) +? (\sum_(m <= i <oo | Q i) g i).
Proof.
move=> 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) :
Expand Down Expand Up @@ -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 <oo | P i) (f i + g i) =
\sum_(i <oo | P i) f i + \sum_(i <oo | P i) g i.
\sum_(N <= i <oo | P i) (f i + g i) =
\sum_(N <= i <oo | P i) f i + \sum_(N <= i <oo | P i) g i.
Proof.
move=> 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 <oo) (\sum_(0 <= i < n) f i j) =
\sum_(0 <= i < n) (\sum_(j <oo) (f i j)).
\sum_(N <= j <oo) (\sum_(m <= i < n) f i j) =
\sum_(m <= i < n) (\sum_(N <= j <oo) (f i j)).
Proof.
move=> 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 <oo) \sum_(i <- r | P i) f i j =
\sum_(i <- r | P i) \sum_(j <oo) f i j.
[f : I -> nat -> \bar R] N : (forall i j, P i -> 0 <= f i j) ->
\sum_(N <= j <oo) \sum_(i <- r | P i) f i j =
\sum_(i <- r | P i) \sum_(N <= j <oo) f i j.
Proof.
move=> f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr.
by rewrite big_nil eseries0// => i; rewrite big_nil.
Expand Down
Loading