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

@@ -2673,7 +2673,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

@@ -2076,9 +2076,9 @@ apply/uniform_restrict_cvg => /= U /=; rewrite ?uniform_nbhsT.
 case/nbhs_ex => del /filterS; apply.
 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

@@ -3714,8 +3714,8 @@ rewrite -[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 => //=; rewrite nbhs_ballE;
     exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)).
 case => a b /= [/ball_sym xar yar]; apply: distrU => /=.
@@ -3724,11 +3724,11 @@ have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E.
 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).
-have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4).
+have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R).
+have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R).
 rewrite -fineB// -fine_abse ?fin_numB ?abfin ?efin//.
 rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//.
   rewrite fine_le// ?fin_numD ?daxr ?dybr//.
@@ -3739,7 +3739,7 @@ rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//.
   rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC.
   by rewrite lee_subl_addr// addeAC.
 rewrite fineD // [_%:num]splitr.
-have r42 : r%:num / 4 < r%:num / 2.
+have r42 : r%:num / 4%:R < r%:num / 2.
   by rewrite ltr_pmul2l// ltf_pinv ?posrE ?ltr0n// ltr_nat.
 by apply: ltr_add; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin.
 Unshelve. end_near. Qed.

theories/probability.v

@@ -488,8 +488,8 @@ rewrite -sqrteM ?variance_ge0//.
 rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//.
 rewrite -(fineK (variance_fin_num X1 X2)) -(fineK (variance_fin_num Y1 Y2)).
 rewrite -(fineK (covariance_fin_num X1 Y1 XY1)).
-rewrite -EFin_expe -EFinM lee_fin -(@ler_pmul2l _ 4) ?ltr0n// [leRHS]mulrA.
-rewrite [in leLHS](_ : 4 = 2 * 2)%R -natrM// natrM mulrACA -expr2 -subr_le0.
+rewrite -EFin_expe -EFinM lee_fin -(@ler_pmul2l _ 4%:R) ?ltr0n// [leRHS]mulrA.
+rewrite [in leLHS](natrM _ 2 2) mulrACA -expr2 -subr_le0.
 apply: deg_le2_ge0 => r; rewrite -lee_fin !EFinD.
 rewrite EFinM fineK ?variance_fin_num// muleC -varianceZ//.
 rewrite -mulrA EFinM mulrC EFinM ?fineK ?covariance_fin_num// -covarianceZl//.
@@ -630,7 +630,7 @@ pose u0 := (fine 'V_P[X] / lambda)%R.
 have u0ge0 : (0 <= u0)%R.
   by apply: divr_ge0 (ltW lambda_gt0); rewrite -lee_fin finVK variance_ge0.
 apply: le_trans (le _ u0ge0) _; rewrite lee_fin le_eqVlt; apply/orP; left.
-rewrite eqr_div; [|apply: lt0r_neq0..]; last 2 first.
+rewrite GRing.eqr_div; [|apply: lt0r_neq0..]; last 2 first.
 - by rewrite exprz_gt0 -1?[ltLHS]addr0 ?ltr_le_add.
 - by rewrite ltr_paddl ?fine_ge0 ?variance_ge0 ?exprz_gt0.
 apply/eqP; have -> : fine 'V_P[X] = (u0 * lambda)%R.

theories/reals.v

@@ -460,7 +460,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

@@ -1577,9 +1577,21 @@ 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 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 congr (lim _); apply: 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 congr (lim _); apply/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 congr (lim _); apply/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.
+  \sum_(N <= i <oo | P i) f i = \sum_(N <= i <oo | P i) g i.
 Proof. by move=> efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed.
 
 Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) :
@@ -1664,7 +1676,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) ->
   cvg (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) ->
   cvg (fun n => \sum_(N <= i < n | P i) u_ i).
@@ -1694,6 +1708,7 @@ Qed.
 
 End cvg_eseries.
 Arguments is_cvg_nneseries {R}.
+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 -> cvg (series u).
@@ -1709,9 +1724,9 @@ rewrite /ubound/= => _ [n _ <-]; rewrite -lee_fin fineK//; last first.
 by rewrite -sumEFin; apply: nneseries_lim_ge => i _; rewrite lee_fin.
 Qed.
 
-Lemma nneseriesrM (R : realType) (f : nat -> \bar R) (P : pred nat) x :
+Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N :
   (forall i, P i -> 0 <= f i) ->
-  (\sum_(i <oo | P i) (x%:E * f i) = x%:E * \sum_(i <oo | P i) 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 congr (lim _); apply/funext => /= n; rewrite ge0_sume_distrr.
@@ -1761,15 +1776,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) :
@@ -1957,10 +1973,10 @@ rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0.
 by congr (lim _); apply/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.
@@ -2651,8 +2667,8 @@ have [q_gt0 | | q0] := ltrgt0P q%:num.
 - near=> n => /=; apply: (le_lt_trans (@ctrfq (_, _) _)) => //=.
   + split; last exact: funS.
     by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS.
-  + rewrite -ltr_pdivl_mull //; near: n; move/cvgrPdist_lt: contraction_cvg; apply.
-    by rewrite mulr_gt0 // invr_gt0.
+  + rewrite -ltr_pdivl_mull //; near: n; move/cvgrPdist_lt: contraction_cvg.
+    by apply; rewrite mulr_gt0 // invr_gt0.
 - by rewrite ltNge//; exact: contraNP.
 - apply: nearW => /= n; apply: (le_lt_trans (@ctrfq (_, _) _)).
   + split; last exact: funS.