fixes (#843)

* fixes

- fixes #828
- fixes #835
- fixes #838

CHANGELOG_UNRELEASED.md

@@ -118,6 +118,8 @@
 
 - in file `topology.v`,
   + lemma `compact_near_coveringP`
+- in `functions.v`:
+  + notation `mem_fun_`
 ### Renamed
 
 - in `measurable.v`:
@@ -146,6 +148,9 @@
   + `finSubCover` -> `finite_subset_cover`
 - in `sequences.v`:
   + `eq_eseries` -> `eq_eseriesr`
+- in `esum.v`:
+  + `summable_nneseries_esum` -> `summable_eseries_esum`
+  + `summable_nneseries` -> `summable_eseries`
 
 ### Generalized
 

classical/functions.v

@@ -389,7 +389,7 @@ Definition mem_fun aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) :=
 
 Definition phant_mem_fun aT rT (A : set aT) (B : set rT)
   (f : {fun A >-> B}) of phantom (_ -> _) f := homo_setP.2 (@funS _ _ _ _ f).
-Notation "'mem_fun_  f" := (phant_funS (Phantom (_ -> _) f))
+Notation "'mem_fun_  f" := (phant_mem_fun (Phantom (_ -> _) f))
   (at level 8, f at level 2) : form_scope.
 
 Lemma some_inv {aT rT} (f : {inv aT >-> rT}) x : Some (f^-1 x) = 'oinv_f x.

theories/esum.v

@@ -545,7 +545,7 @@ transitivity (lim (EFin \o A_)).
 by rewrite EFin_lim//; apply: summable_cvg.
 Qed.
 
-Lemma summable_nneseries (f : nat -> \bar R) (P : pred nat) : summable P f ->
+Lemma summable_eseries (f : nat -> \bar R) (P : pred nat) : summable P f ->
   \sum_(i <oo | P i) (f i) =
   \sum_(i <oo | P i) f^\+ i - \sum_(i <oo | P i) f^\- i.
 Proof.
@@ -559,11 +559,10 @@ suff: ((fun n => C_ n - (A - B)) --> (0 : R^o))%R.
   move=> CAB.
   rewrite [X in  X - _]summable_nneseries_lim//; last exact/summable_funepos.
   rewrite [X in _ - X]summable_nneseries_lim//; last exact/summable_funeneg.
-  rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split.
-    apply: nearW => n.
-    rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
-    by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge.
-  by apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB) => //; exact: cvg_cst.
+  rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
+    apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB); exact: cvg_cst.
+  apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
+  by rewrite -nneseries_esum ?(le_trans (lee_abs_sum _ _ _)) ?nneseries_lim_ge.
 have : ((fun x => A_ x - B_ x) --> A - B)%R.
   apply: cvgD.
   - by apply: summable_cvg => //; exact/summable_funepos.
@@ -575,23 +574,20 @@ rewrite distrC subr0.
 have -> : (C_ = A_ \- B_)%R.
   apply/funext => k.
   rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
-  apply eq_bigr => i Pi.
-  rewrite -fineB//.
+  apply eq_bigr => i Pi; rewrite -fineB//.
   - by rewrite [in LHS](funeposneg f).
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg.
 by rewrite distrC; apply: hN; near: n; exists N.
 Unshelve. all: by end_near. Qed.
 
-Lemma summable_nneseries_esum  (f : nat -> \bar R) (P : pred nat) :
+Lemma summable_eseries_esum  (f : nat -> \bar R) (P : pred nat) :
   summable P f -> \sum_(i <oo | P i) f i = esum P f^\+ - esum P f^\-.
 Proof.
-move=> Pfoo.
-rewrite -nneseries_esum; last first.
+move=> Pfoo; rewrite -nneseries_esum; last first.
   by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt.
-rewrite -nneseries_esum; last first.
-  by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt.
-by rewrite [LHS]summable_nneseries.
+rewrite -nneseries_esum ?[LHS]summable_eseries//.
+by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt.
 Qed.
 
 End summable_nat.

theories/lebesgue_integral.v

@@ -2864,15 +2864,15 @@ rewrite -esumB//; last 4 first.
   - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo.
   - by move=> n _; exact/fine_ge0/integral_ge0.
   - by move=> n _; exact/fine_ge0/integral_ge0.
-rewrite -summable_nneseries_esum; last first.
-  rewrite /summable.
+rewrite -summable_eseries_esum; last first.
   apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true))
      `|(fine (\int[m_ i]_(x in D) f x))%:E|)).
-    apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//;
+    by apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//;
       [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num].
   rewrite -nneseries_esum; last by [].
-  apply: (@le_lt_trans _ _ (\sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\+ x))%:E| +
-                            \sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\- x))%:E|)).
+  apply: (@le_lt_trans _ _
+      (\sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\+ x))%:E| +
+       \sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\- x))%:E|)).
     rewrite -nneseriesD//; apply: lee_nneseries => // n _.
     rewrite integralE fineB// ?EFinB.
     - exact: (le_trans (lee_abs_sub _ _)).
@@ -3841,7 +3841,7 @@ rewrite set_true -esumB//=; last 4 first.
   - exact: integrableN.
   - by move=> n _; exact: integral_ge0.
   - by move=> n _; exact: integral_ge0.
-rewrite summable_nneseries; last first.
+rewrite summable_eseries; last first.
   under [X in summable _ X]eq_fun do rewrite -integralE.
   by rewrite fun_true; exact: integrable_summable.
 by congr (_ - _)%E; rewrite nneseries_esum// set_true.

theories/topology.v

@@ -188,6 +188,8 @@ Require Import reals signed.
 (*                                     a pointedType, as well as the carrier. *)
 (*                                     nbhs_of_open \o open_from must be      *)
 (*                                     used to declare a filterType           *)
+(*                    finI_from D f == set of \bigcap_(i in E) f i where E is *)
+(*                                     a finite subset of D                   *)
 (*       topologyOfSubbaseMixin D b == builds the mixin for a topological     *)
 (*                                     space from a subbase of open sets b    *)
 (*                                     indexed on domain D; the type of       *)