minor generalizations, renaming

CHANGELOG_UNRELEASED.md

@@ -63,6 +63,8 @@
 
 - in `classical_sets.v`:
   + lemma `Zorn_bigcup`
+- in `sequences.v`:
+  + lemma `eseries_cond`
 
 ### Changed
 
@@ -75,6 +77,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`:
@@ -161,6 +166,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/sequences.v

@@ -1571,9 +1571,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 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) if (N <= i)%N then f i else 0.
+Proof.
+congr (lim _); apply: eq_fun => n /=; have [Nn|nN] := leqP N n; last first.
+  rewrite [in LHS]/index_iota (@size0nil _ (iota _ _)) ?big_nil; last first.
+    by apply/eqP; rewrite size_iota subn_eq0 ltnW.
+  rewrite /index_iota subn0 big_seq_cond big1// => /= k.
+  rewrite mem_iota add0n leq0n/= => /andP[+ _].
+  by move/ltn_trans/(_ nN); rewrite ltnNge => /negbTE ->.
+rewrite {2}/index_iota subn0 -[in RHS](@subnKC N n)// iotaD big_cat/= add0n.
+rewrite [X in _ = X + _]big_seq_cond [X in _ = X + _]big1 ?adde0 /=; last first.
+  move=> i; rewrite mem_iota add0n leq0n/= => /andP[+ _].
+  by rewrite ltnNge => /negbTE ->.
+rewrite add0e [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr => /= k.
+by rewrite mem_iota subnKC// => /andP[/andP[-> _]].
+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) :
@@ -1658,7 +1675,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).
@@ -1688,6 +1707,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).
@@ -1703,9 +1723,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.
@@ -1755,15 +1775,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) :
@@ -1951,10 +1972,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.
@@ -2635,8 +2656,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.