minor generalizations, additions, fixes (#974)

- fixes #938

CHANGELOG_UNRELEASED.md

@@ -51,6 +51,9 @@
 - in file `lebesgue_integral.v`,
   + new lemma `approximation_sfun_integrable`.
 
+- in `classical_sets.v`:
+  + lemmas `properW`, `properxx`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
@@ -119,6 +122,15 @@
   + `powere_posM` -> `poweRM`
   + `powere12_sqrt` -> `poweR12_sqrt`
 
+- in `lebesgue_integral.v`:
+  + `ge0_integralM_EFin` -> `ge0_integralZl_EFin`
+  + `ge0_integralM` -> `ge0_integralZl`
+  + `integralM_indic` -> `integralZl_indic`
+  + `integralM_indic_nnsfun` -> `integralZl_indic_nnsfun`
+  + `integrablerM` -> `integrableZl`
+  + `integrableMr` -> `integrableZr`
+  + `integralM` -> `integralZl`
+
 ### Generalized
 
 - in `exp.v`:
@@ -128,6 +140,11 @@
   + lemma `ln_power_pos`
 - in file `lebesgue_integral.v`, updated `le_approx`.
 
+- in `sequences.v`:
+  + lemmas `is_cvg_nneseries_cond`, `is_cvg_npeseries_cond`
+  + lemmas `is_cvg_nneseries`, `is_cvg_npeseries`
+  + lemmas `nneseries_ge0`, `npeseries_le0`
+
 ### Deprecated
 
 ### Removed

classical/classical_sets.v

@@ -60,6 +60,7 @@ From mathcomp Require Import mathcomp_extra boolp.
 (*                 \bigcap_i F == same as before with T left implicit.        *)
 (*                smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A  *)
 (*                   A `<=` B <-> A is included in B.                         *)
+(*                    A `<` B := A `<=` B /\ ~ (B `<=` A)                     *)
 (*                  A `<=>` B <-> double inclusion A `<=` B and B `<=` A.     *)
 (*                   f @^-1` A == preimage of A by f.                         *)
 (*                      f @` A == image of A by f. Notation for `image A f`.  *)
@@ -531,6 +532,10 @@ Proof. by move=> sAB sBC ? ?; apply/sBC/sAB. Qed.
 
 Lemma sub0set A : set0 `<=` A. Proof. by []. Qed.
 
+Lemma properW A B : A `<` B -> A `<=` B. Proof. by case. Qed.
+
+Lemma properxx A : ~ A `<` A. Proof. by move=> [?]; apply. Qed.
+
 Lemma setC0 : ~` set0 = setT :> set T.
 Proof. by rewrite predeqE; split => ?. Qed.
 

classical/mathcomp_extra.v

@@ -830,3 +830,18 @@ Reserved Notation "f \min g" (at level 50, left associativity).
 Definition min_fun T (R : numDomainType) (f g : T -> R) x := Num.min (f x) (g x).
 Notation "f \min g" := (min_fun f g) : ring_scope.
 Arguments min_fun {T R} _ _ _ /.
+
+(* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type
+   making the following lemma redundant *)
+Section dependent_choice_Type.
+Context X (R : X -> X -> Prop).
+
+Lemma dependent_choice_Type : (forall x, {y | R x y}) ->
+  forall x0, {f | f 0%N = x0 /\ forall n, R (f n) (f n.+1)}.
+Proof.
+move=> h x0.
+set (f := fix f n := if n is n'.+1 then proj1_sig (h (f n')) else x0).
+exists f; split => //.
+intro n; induction n; simpl; apply: proj2_sig.
+Qed.
+End dependent_choice_Type.

theories/charge.v

@@ -69,21 +69,6 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
 
-(* NB: in the next releases of Coq, dependent_choice will be
-   generalized from Set to Type making the following lemma redundant *)
-Section dependent_choice_Type.
-Context X (R : X -> X -> Prop).
-
-Lemma dependent_choice_Type : (forall x, {y | R x y}) ->
-  forall x0, {f | f 0 = x0 /\ forall n, R (f n) (f n.+1)}.
-Proof.
-move=> h x0.
-set (f := fix f n := if n is n'.+1 then proj1_sig (h (f n')) else x0).
-exists f; split => //.
-intro n; induction n; simpl; apply: proj2_sig.
-Qed.
-End dependent_choice_Type.
-
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
 Local Open Scope ereal_scope.
@@ -723,7 +708,7 @@ move=> /cvg_ex[[l| |]]; first last.
     have : nu N <= -oo by rewrite -limNoo// nuN.
     by rewrite leNgt => /negP; apply; rewrite ltNye_eq fin_num_measure.
   - move/cvg_lim => limoo.
-    have := @npeseries_le0 _ (fun n => maxe (z_ (v n) * 2^-1%:E) (- 1%E)) xpredT.
+    have := @npeseries_le0 _ (fun n => maxe (z_ (v n) * 2^-1%:E) (- 1%E)) xpredT 0.
     by rewrite limoo// leNgt => /(_ (fun n _ => max_le0 n))/negP; apply.
 move/fine_cvgP => [Hfin cvgl].
 have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> \oo]).