minor generalizations, renaming (#985)

* decomposing eseries_cond into bits

Co-authored-by: Cyril Cohen <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -79,6 +79,9 @@
 - in `constructive_ereal.v`:
   + lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull`
   + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n`
+- in `sequences.v`:
+  + lemma `eseries_cond`
+  + lemmas `eseries_mkcondl`, `eseries_mkcondr`
 
 - in file `numfun.v`,
   + new lemma `continuous_bounded_extension`.
@@ -98,6 +101,9 @@
 - in `exp.v`:
   + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)
 
+- in `sequences.v`:
+  + lemma `nneseriesrM` generalized and renamed to `nneseriesZl`
+
 ### Renamed
 
 - in `boolp.v`:
@@ -184,6 +190,9 @@
     (from measure to content)
   + lemma `subset_measure0` (from `realType` to `realFieldType`)
 
+- in `sequences.v`:
+  + lemmas `eq_eseriesr`, `lee_nneseries`
+
 ### Deprecated
 
 ### Removed

theories/lebesgue_integral.v

@@ -2769,7 +2769,7 @@ rewrite ge0_integral_fsum//; last 2 first.
 transitivity (\sum_(i \in range f)
     (\sum_(n <oo) i%:E * \int[m_ n]_x (\1_(f @^-1` [set i]) x)%:E)).
   apply: eq_fsbigr => r _.
-  rewrite integralZl_indic_nnsfun// integral_measure_series_indic// nneseriesrM//.
+  rewrite integralZl_indic_nnsfun// integral_measure_series_indic// nneseriesZl//.
   by move=> n _; apply: integral_ge0 => t _; rewrite lee_fin.
 rewrite fsbig_finite//= -nneseries_sum; last first.
   move=> r j _.

theories/lebesgue_measure.v

@@ -2079,9 +2079,9 @@ apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT.
 case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU.
 have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
 exists (badn N) => // r badNr x.
-rewrite /patch; case xAB: (x \in A`\`_) => //; apply: (lt_trans _ Ndel).
+rewrite /patch; case xAB: (x \in A `\` _) => //; apply: (lt_trans _ Ndel).
 move/set_mem: xAB; rewrite setDE; case => Ax; rewrite setC_bigcup => /(_ N I).
-rewrite /E setC_bigcup => /(_ (r)) /=; rewrite /h => /(_ badNr) /not_andP [] //.
+rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP [] //.
 by move/negP; rewrite real_ltNge // distrC.
 Qed.
 

theories/normedtype.v

@@ -2876,16 +2876,16 @@ rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin.
   by have := edist_fin_open efin; apply: filter_app; near=> w.
 move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE.
 move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=.
-have r2p : 0 < r%:num / 4 by rewrite divr_gt0// ltr0n.
-exists (ball x (r%:num / 4), ball y (r%:num / 4)).
+have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n.
+exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)).
   by split => //=; exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)).
 case => a b /= [/ball_sym xar yar]; apply: distrU => /=.
 have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E.
   by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle.
 have abfin : edist (a, b) \is a fin_num.
   rewrite ge0_fin_numE// (le_lt_trans abxy)//.
   by apply: lte_add_pinfty; [apply: lte_add_pinfty|];
-    rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4).
+    rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R).
 have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num.
   by rewrite abse_fin_num fin_numB abfin efin.
 have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4).

theories/reals.v

@@ -335,7 +335,7 @@ apply: le_anti; apply/andP; split.
   by move=> ? [p Ap [q Bq] <-]; apply: ler_add; exact: sup_ub.
 rewrite real_leNgt ?num_real// -subr_gt0; apply/negP.
 set eps := (_ + _ - _) => epos.
-have e2pos : 0 < eps / 2 by rewrite divr_gt0// ltr0n.
+have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
 have [r Ar supBr] := sup_adherent e2pos supA.
 have [s Bs supAs] := sup_adherent e2pos supB.
 have := ltr_add supBr supAs.

theories/sequences.v

@@ -1590,14 +1590,26 @@ Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat)
   nondecreasing_seq (fun n => \sum_(0 <= 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 : realFieldType) (f g : nat -> \bar R) :
+Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) :
   f = g -> limn f = limn g.
 Proof. by move=> ->. Qed.
 
-Lemma eq_eseriesr (R : realFieldType) (f g : (\bar R)^nat) (P : pred nat) :
+Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) 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 : nat -> \bar R) P Q :
+  \sum_(i <oo | P i && Q i) f i = \sum_(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 : nat -> \bar R) P Q :
+  \sum_(i <oo | P i && Q i) f i = \sum_(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_(i <oo | P i) f i = \sum_(i <oo | P i) g i.
-Proof. by move=> efg; congr (limn _); apply/funext => n; exact: eq_bigr. Qed.
+  \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.
@@ -1681,7 +1693,9 @@ Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n /u_le0. Qed.
 
 Lemma is_cvg_nneseries_cond P N : (forall n, P n -> 0 <= u_ n) ->
   cvgn (fun n => \sum_(N <= i < n | P i) u_ i).
-Proof. by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _ /u_ge0. Qed.
+Proof.
+by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _; exact: u_ge0.
+Qed.
 
 Lemma is_cvg_npeseries_cond P N : (forall n, P n -> u_ n <= 0) ->
   cvgn (fun n => \sum_(N <= i < n | P i) u_ i).
@@ -1711,14 +1725,7 @@ Qed.
 
 End cvg_eseries.
 Arguments is_cvg_nneseries {R}.
-
-Lemma nneseriesrM (R : realType) (f : nat -> \bar R) (P : pred nat) x :
-  (forall i, P i -> 0 <= f i)%E ->
-  (\sum_(i <oo | P i) (x%:E * f i) = x%:E * \sum_(i <oo | P i) f i)%E.
-Proof.
-move=> f0; rewrite -limeMl//; last exact: is_cvg_nneseries.
-by apply/congr_lim/funext => /= n; rewrite ge0_sume_distrr.
-Qed.
+Arguments nneseries_ge0 {R u_ P} N.
 
 Lemma nnseries_is_cvg {R : realType} (u : nat -> R) :
     (forall i, 0 <= u i)%R -> \sum_(k <oo) (u k)%:E < +oo ->
@@ -1735,6 +1742,14 @@ rewrite /ubound/= => _ [n _ <-]; rewrite -lee_fin fineK//; last first.
 by rewrite -sumEFin; apply: nneseries_lim_ge => i _; rewrite lee_fin.
 Qed.
 
+Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N :
+  (forall i, P i -> 0 <= f i) ->
+  (\sum_(N <= i <oo | P i) (x%:E * f i) = x%:E * \sum_(N <= i <oo | P i) f i).
+Proof.
+move=> f0; rewrite -limeMl//; last exact: is_cvg_nneseries.
+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) :
   (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) ->
@@ -1779,15 +1794,16 @@ move=> u_ge0 Pk ukoo; apply: (eseries_pinfty _ Pk ukoo) => // n Pn.
 by rewrite gt_eqF// (lt_le_trans _ (u_ge0 _ Pn)).
 Qed.
 
-Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) :
-  (forall i, P i -> 0 <= u i) -> (forall n, P n -> u n <= v n) ->
-  \sum_(i <oo | P i) u i <= \sum_(i <oo | P i) v i.
+Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N :
+  (forall i, P i -> 0 <= u i) ->
+  (forall n, P n -> u n <= v n) ->
+  \sum_(N <= i <oo | P i) u i <= \sum_(N <= i <oo | P i) v i.
 Proof.
 move=> u0 Puv; apply: lee_lim.
-- by apply: is_cvg_ereal_nneg_natsum_cond => n _ /u0.
+- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact.
 - apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn.
   by rewrite (le_trans _ (Puv _ Pn))// u0.
-- by near=> n; exact: lee_sum.
+- by near=> n; apply: lee_sum => k; exact: Puv.
 Unshelve. all: by end_near. Qed.
 
 Lemma lee_npeseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) :
@@ -1976,10 +1992,10 @@ 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.
 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.
+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.
 Proof.
 move=> f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr.
   by rewrite big_nil eseries0// => i; rewrite big_nil.