minor additions (#1558)

* minor additions

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

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -96,6 +96,12 @@
   + `lebesgue_integral_differentiation.v`
   + `lebesgue_integral.v`
 
+- in `sequences.v`:
+  + lemmas `nneseriesD1`, `geometric_ge0`
+
+- in `constructive_ereal.v`:
+  + lemmas `EFin_fin_numP`, `EFin_bigmax`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package
@@ -158,6 +164,9 @@
 - in `real_interval.v`:
   + lemmas `bigcup_itvT`, `itv_bndy_bigcup_BRight`, `itv_bndy_bigcup_BLeft_shift`
 
+- in `sequences.v`:
+  + lemma `nneseries_recl` genralized with a filtering predicate `P`
+
 ### Deprecated
 
 ### Removed

reals/constructive_ereal.v

@@ -739,6 +739,9 @@ Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
 Fact fin_num_key : pred_key fin_num. Proof. by []. Qed.
 (*Canonical fin_num_keyd := KeyedQualifier fin_num_key.*)
 
+Lemma EFin_fin_numP x : reflect (exists r, x = r%:E) (x \in fin_num).
+Proof. by case: x => [r'||]//=; constructor; [exists r'| case | case ]. Qed.
+
 Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
 Proof. by []. Qed.
 

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -965,7 +965,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variables (m1 : {sfinite_measure set X -> \bar R}).
 Variables (m2 : {sfinite_measure set Y -> \bar R}).
 Variables (f : X * Y -> \bar R) (f0 : forall xy, 0 <= f xy).
-Hypothesis mf : measurable_fun setT f.
+Hypothesis mf : measurable_fun [set: X * Y] f.
 
 Lemma sfinite_Fubini :
   \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).

theories/measure.v

@@ -4250,7 +4250,7 @@ Lemma le_outer_measure : {homo mu : A B / A `<=` B >-> A <= B}.
 Proof.
 move=> A B AB; pose B_ k := if k is 0%N then B else set0.
 have -> : mu B = \sum_(n <oo) mu (B_ n).
-  rewrite nneseries_recl; last by move=> ?; rewrite outer_measure_ge0.
+  rewrite nneseries_recl//; last by move=> *; rewrite outer_measure_ge0.
   rewrite eseries_cond/= eseries0 ?adde0// => -[|]//= k _ _.
   by rewrite outer_measure0.
 apply: subset_outer_measure_sigma_subadditive => //.

theories/sequences.v

@@ -964,6 +964,10 @@ rewrite exprDn (bigD1 (inord 1)) ?inordK// subn1 expr1 bin1 lerDl sumr_ge0//.
 by move=> i; rewrite ?(mulrn_wge0, mulr_ge0, exprn_ge0, subr_ge0)// ltW.
 Unshelve. all: by end_near. Qed.
 
+Lemma geometric_ge0 (R : numFieldType) (a z : R) n :
+  0 <= a -> 0 <= z -> geometric a z n >= 0.
+Proof. by move=> *; rewrite mulr_ge0// exprn_ge0. Qed.
+
 Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 ->
   series (geometric a z) = [sequence a * (1 - z ^+ n) / (1 - z)]_n.
 Proof.
@@ -1773,7 +1777,7 @@ rewrite -lim_shift_cst; last by rewrite (@lt_le_trans _ _ 0)// f0// leq_addr.
 Unshelve. all: by end_near. Qed.
 
 Lemma nneseries_split_cond (R : realType) (f : nat -> \bar R) N n (P : pred nat) :
-  (forall k, P k -> 0 <= f k)%E ->
+  (forall k, P k -> 0 <= f k) ->
   \sum_(N <= k <oo | P k) f k =
   \sum_(N <= k < N + n | P k) f k + \sum_(N + n <= k <oo | P k) f k.
 Proof.
@@ -1782,15 +1786,36 @@ rewrite big_mkcond/= (nneseries_split n)// => k Nk.
 by case: ifPn => //; exact: NPf.
 Qed.
 
+Lemma nneseriesD1 {R : realType} (f : nat -> \bar R) n (P : pred nat) :
+  (forall k, P k -> 0 <= f k) -> P n ->
+  \sum_(0 <= k <oo | P k) f k =
+  f n + \sum_(0 <= k <oo | P k && (k != n)) f k.
+Proof.
+move=> f0 Pn.
+rewrite (@nneseries_split_cond _ f 0%N n.+1 P)// add0n big_mkcond/=.
+rewrite big_nat_recr//= Pn -big_mkcond/= -addrA addrCA; congr +%E.
+rewrite [RHS]eseries_mkcondr.
+rewrite [in RHS](@nneseries_split_cond _ _ _ n.+1 P)//; last first.
+  by move=> k Pk; case: ifPn => // _; exact: f0.
+rewrite add0n [X in _ = X + _]big_mkcond/= big_nat_recr//= Pn eqxx/= adde0.
+rewrite -big_mkcond//=; congr +%E.
+  rewrite big_seq_cond [RHS]big_seq_cond; apply: eq_bigr => /= i.
+  by rewrite mem_index_iota leq0n/= => /andP[ij Pi]; rewrite lt_eqF.
+rewrite eseries_cond [RHS]eseries_cond; apply: eq_eseriesr => i /andP[Pi ji].
+by rewrite gt_eqF.
+Qed.
+
 End nneseries_split.
 Arguments nneseries_split {R f} _ _.
 Arguments nneseries_split_cond {R f} _ _ _.
+Arguments nneseriesD1 {R f} n {P}.
 
-Lemma nneseries_recl (R : realType) (f : nat -> \bar R) :
-  (forall k, 0 <= f k) -> \sum_(k <oo) f k = f 0%N + \sum_(1 <= k <oo) f k.
+Lemma nneseries_recl {R : realType} (P : pred nat) (f : nat -> \bar R) :
+  (forall k, P k -> 0 <= f k) -> P 0%N ->
+  \sum_(0 <= k <oo | P k) f k = f 0%N + \sum_(1 <= k <oo | P k) f k.
 Proof.
-move=> f0; rewrite [LHS](nneseries_split _ 1)// add0n.
-by rewrite /index_iota subn0/= big_cons big_nil addr0.
+move=> F0 P0; rewrite (nneseriesD1 0%N)//; congr +%E.
+by rewrite [RHS]eseries_cond; apply: eq_eseriesl => n; rewrite lt0n.
 Qed.
 
 Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) P :