fixes #1052 (#1085)

CHANGELOG_UNRELEASED.md

@@ -160,6 +160,22 @@
   + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup`
   + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup`
 
+- in `sequences.v`:
+  + `ereal_nondecreasing_cvg` -> `ereal_nondecreasing_cvgn`
+  + `ereal_nondecreasing_is_cvg` -> `ereal_nondecreasing_is_cvgn`
+  + `ereal_nonincreasing_cvg` -> `ereal_nonincreasing_cvgn`
+  + `ereal_nonincreasing_is_cvg` -> `ereal_nonincreasing_is_cvgn`
+  + `ereal_nondecreasing_opp` -> `ereal_nondecreasing_oppn`
+  + `nonincreasing_cvg_ge` -> `nonincreasing_cvgn_ge`
+  + `nondecreasing_cvg_le` -> `nondecreasing_cvgn_le`
+  + `nonincreasing_cvg` -> `nonincreasing_cvgn`
+  + `nondecreasing_cvg` -> `nondecreasing_cvgn`
+  + `nonincreasing_is_cvg` -> `nonincreasing_is_cvgn`
+  + `nondecreasing_is_cvg` -> `nondecreasing_is_cvgn`
+  + `near_nonincreasing_is_cvg` -> `near_nonincreasing_is_cvgn`
+  + `near_nondecreasing_is_cvg` -> `near_nondecreasing_is_cvgn`
+  + `nondecreasing_dvg_lt` -> `nondecreasing_dvgn_lt`
+
 ### Generalized
 
 - in `topology.v`:

theories/charge.v

@@ -1027,12 +1027,12 @@ Lemma max_approxRN_seq_nd x : nondecreasing_seq (F_ ^~ x).
 Proof. by move=> a b ab; rewrite (le_bigmax_ord xpredT (g_ ^~ x)). Qed.
 
 Lemma is_cvg_max_approxRN_seq n : cvg (F_ ^~ n @ \oo).
-Proof. by apply: ereal_nondecreasing_is_cvg; exact: max_approxRN_seq_nd. Qed.
+Proof. by apply: ereal_nondecreasing_is_cvgn; exact: max_approxRN_seq_nd. Qed.
 
 Lemma is_cvg_int_max_approxRN_seq A :
   measurable A -> cvg ((fun n => \int[mu]_(x in A) F_ n x) @ \oo).
 Proof.
-move=> mA; apply: ereal_nondecreasing_is_cvg => a b ab.
+move=> mA; apply: ereal_nondecreasing_is_cvgn => a b ab.
 apply: ge0_le_integral => //.
 - by move=> ? ?; exact: max_approxRN_seq_ge0.
 - by apply: measurable_funS (measurable_max_approxRN_seq a).

theories/esum.v

@@ -519,7 +519,7 @@ Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) :
   (forall i, P i -> 0 <= f i)%E -> summable P f ->
   cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo).
 Proof.
-move=> f0 Pf; apply: nondecreasing_is_cvg.
+move=> f0 Pf; apply: nondecreasing_is_cvgn.
   by apply: nondecreasing_series => n Pn; exact/fine_ge0/f0.
 exists (fine (\sum_(i <oo | P i) `|f i|)) => x /= [n _ <-].
 rewrite summable_fine_sum// -lee_fin fineK//; last first.

theories/kernel.v

@@ -520,7 +520,7 @@ rewrite (_ : (fun x => _) =
   apply/funext => x.
   transitivity (lim (\int[l x]_y (k_ n (x, y))%:E @[n --> \oo])); last first.
     rewrite is_cvg_limn_esupE//.
-    apply: ereal_nondecreasing_is_cvg => m n mn.
+    apply: ereal_nondecreasing_is_cvgn => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
     - exact/EFin_measurable_fun/measurableT_comp.

theories/lebesgue_integral.v

@@ -835,7 +835,7 @@ Lemma is_cvg_sintegral d (T : measurableType d) (R : realType)
   (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) :
   (forall x, nondecreasing_seq (f ^~ x)) -> cvgn (sintegral m \o f).
 Proof.
-move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
 by apply: le_sintegral => // => x; exact/nd_f.
 Qed.
 
@@ -905,7 +905,7 @@ have [cf|df] := pselect (cvgn (g^~ x)).
   suff [n cfgn] : exists n, g n x >= c * f x by exists n.
   move/(@lt_lim _ _ _ (nd_g x) cf) : cfg => [n _ nf].
   by exists n; apply: nf => /=.
-have /cvgryPge/(_ (c * f x))[n _ ncfgn]:= nondecreasing_dvg_lt (nd_g x) df.
+have /cvgryPge/(_ (c * f x))[n _ ncfgn]:= nondecreasing_dvgn_lt (nd_g x) df.
 by exists n => //; rewrite /fleg /=; apply: ncfgn => /=.
 Qed.
 
@@ -985,9 +985,9 @@ apply/eqP; rewrite eq_le; apply/andP; split.
   by apply: nd_sintegral_lim_lemma => // x; rewrite -limg.
 have : nondecreasing_seq (sintegral mu \o g).
   by move=> m n mn; apply: le_sintegral => // x; exact/nd_g.
-move=> /ereal_nondecreasing_cvg/cvg_lim -> //.
+move=> /ereal_nondecreasing_cvgn/cvg_lim -> //.
 apply: ub_ereal_sup => _ [n _ <-] /=; apply: le_sintegral => // x.
-rewrite -limg // (nondecreasing_cvg_le (nd_g x)) //.
+rewrite -limg // (nondecreasing_cvgn_le (nd_g x)) //.
 by apply/cvg_ex; exists (f x); exact: gf.
 Qed.
 
@@ -1189,7 +1189,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
   near=> n; apply: ereal_sup_ub; exists (g n) => //= => x.
   have <- : limn (EFin \o g ^~ x) = f x by apply/cvg_lim => //; exact: gf.
   have : EFin \o g ^~ x @ \oo --> ereal_sup (range (EFin \o g ^~ x)).
-    by apply: ereal_nondecreasing_cvg => p q pq /=; rewrite lee_fin; exact/nd_g.
+    by apply: ereal_nondecreasing_cvgn => p q pq /=; rewrite lee_fin; exact/nd_g.
   by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n.
 have := leey (\int[mu]_x (f x)).
 rewrite le_eqVlt => /predU1P[|] mufoo; last first.
@@ -1524,7 +1524,7 @@ have nd_ag : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}.
 have fi0 y : D y -> (0 <= f y)%E by move=> ?; exact: f0.
 have cvg_af := cvg_approx fi0 Dx fixoo.
 have is_cvg_af : cvgn (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af.
-have {is_cvg_af} := nondecreasing_cvg_le nd_ag is_cvg_af k.
+have {is_cvg_af} := nondecreasing_cvgn_le nd_ag is_cvg_af k.
 rewrite -lee_fin => /le_trans; apply.
 rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0.
 by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->.
@@ -1561,7 +1561,7 @@ move=> Dx; have := leey (f x); rewrite le_eqVlt => /predU1P[|] fxoo.
 have dvg_approx := dvg_approx Dx fxoo.
   have : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}.
     by move=> m n mn; have := nd_approx mn => /lefP; exact.
-  move/nondecreasing_dvg_lt => /(_ dvg_approx).
+  move/nondecreasing_dvgn_lt => /(_ dvg_approx).
   by rewrite fxoo => ?; apply/cvgeryP.
 rewrite -(@fineK _ (f x)); first exact: (cvg_comp (cvg_approx f0 Dx fxoo)).
 by rewrite ge0_fin_numE// f0.
@@ -1714,7 +1714,7 @@ have := gh1 t.
 rewrite -(fineK h1tfin) => /fine_cvgP[ft_near].
 set u_ := (X in X --> _) => u_h1 g1h1.
 have <- : lim u_ = fine (h1 t) by exact/cvg_lim.
-rewrite lee_fin; apply: nondecreasing_cvg_le.
+rewrite lee_fin; apply: nondecreasing_cvgn_le.
   by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_g1.
 by apply/cvg_ex; eexists; exact: u_h1.
 Unshelve. all: by end_near. Qed.
@@ -2110,7 +2110,9 @@ Qed.
 Let f := fun x => limn (g^~ x).
 
 Let is_cvg_g t : cvgn (g^~ t).
-Proof. by move=> ?; apply: ereal_nondecreasing_is_cvg => m n ?; apply/nd_g. Qed.
+Proof.
+by move=> ?; apply: ereal_nondecreasing_is_cvgn => m n ?; exact/nd_g.
+Qed.
 
 Local Definition g2' n : (T -> R)^nat := approx setT (g n).
 Local Definition g2 n : {nnsfun T >-> R}^nat := nnsfun_approx measurableT (mg n).
@@ -2122,7 +2124,7 @@ Local Definition max_g2 : {nnsfun T >-> R}^nat :=
 
 Let is_cvg_g2 n t : cvgn (EFin \o (g2 n ^~ t)).
 Proof.
-apply: ereal_nondecreasing_is_cvg => a b ab.
+apply: ereal_nondecreasing_is_cvgn => a b ab.
 by rewrite lee_fin 2!nnsfun_approxE; exact/lefP/nd_approx.
 Qed.
 
@@ -2141,7 +2143,7 @@ Qed.
 
 Let is_cvg_max_g2 t : cvgn (EFin \o max_g2 ^~ t).
 Proof.
-apply: ereal_nondecreasing_is_cvg => m n mn; rewrite lee_fin.
+apply: ereal_nondecreasing_is_cvgn => m n mn; rewrite lee_fin.
 exact/lefP/nd_max_g2.
 Qed.
 
@@ -2183,7 +2185,7 @@ have := leey (g n t); rewrite le_eqVlt => /predU1P[|] fntoo.
     under [in X in X --> _]eq_fun do rewrite nnsfun_approxE.
     have : {homo (approx setT (g n))^~ t : n0 m / (n0 <= m)%N >-> (n0 <= m)%R}.
       exact/lef_at/nd_approx.
-    by move/nondecreasing_dvg_lt => /(_ h).
+    by move/nondecreasing_dvgn_lt => /(_ h).
   have -> : limn (EFin \o max_g2 ^~ t) = +oo.
     by have := lim_g2_max_g2 t n; rewrite g2oo leye_eq => /eqP.
   by rewrite leey.
@@ -2214,18 +2216,18 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
     - move=> x _; apply: lime_ge => //.
       by apply: nearW => k; exact/g0.
     - apply: emeasurable_fun_cvg mg _ => x _.
-      exact: ereal_nondecreasing_is_cvg.
+      exact: ereal_nondecreasing_is_cvgn.
     - move=> x Dx; apply: lime_ge => //.
       near=> m; have nm : (n <= m)%N by near: m; exists n.
       exact/nd_g.
-  by apply: lime_le => //; [exact:ereal_nondecreasing_is_cvg|exact:nearW].
+  by apply: lime_le => //; [exact:ereal_nondecreasing_is_cvgn|exact:nearW].
 rewrite (@nd_ge0_integral_lim _ _ _ mu _ max_g2) //; last 2 first.
   - move=> t; apply: lime_ge => //.
     by apply: nearW => n; exact: g0.
   - by move=> t m n mn; exact/lefP/nd_max_g2.
 apply: lee_lim.
 - by apply: is_cvg_sintegral => // t m n mn; exact/lefP/nd_max_g2.
-- apply: ereal_nondecreasing_is_cvg => // n m nm; apply: ge0_le_integral => //.
+- apply: ereal_nondecreasing_is_cvgn => // n m nm; apply: ge0_le_integral => //.
   by move=> *; exact/nd_g.
 - apply: nearW => n; rewrite ge0_integralTE//.
   by apply: ereal_sup_ub; exists (max_g2 n) => // t; exact: max_g2_g.
@@ -2234,7 +2236,7 @@ Unshelve. all: by end_near. Qed.
 Lemma cvg_monotone_convergence :
   \int[mu]_(x in D) g' n x @[n \oo] --> \int[mu]_(x in D) f' x.
 Proof.
-rewrite monotone_convergence; apply: ereal_nondecreasing_is_cvg => m n mn.
+rewrite monotone_convergence; apply: ereal_nondecreasing_is_cvgn => m n mn.
 by apply: ge0_le_integral => // t Dt; [exact: g'0|exact: g'0|exact: nd_g'].
 Qed.
 
@@ -2431,7 +2433,7 @@ rewrite (_ : \int[m]_(x in D) _ =
   - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin.
 rewrite -limeMl//.
   by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun.
-apply/ereal_nondecreasing_is_cvg => a b ab; apply: ge0_le_integral => //.
+apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
 - exact/EFin_measurable_fun/measurable_funTS.
 - by move=> x _; rewrite lee_fin.
@@ -2460,11 +2462,11 @@ rewrite monotone_convergence //; last first.
   move=> x Dx m n mn /=; apply: le_ereal_inf => _ /= [p /= np <-].
   by exists p => //=; rewrite (leq_trans mn).
 apply: lee_lim.
-- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
   apply: ge0_le_integral => //; [exact: g0| exact: mg| exact: g0| exact: mg|].
   move=> x Dx; apply: le_ereal_inf => _ [n /= bn <-].
   by exists n => //=; rewrite (leq_trans ab).
-- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
   apply: le_ereal_inf => // _ [n /= bn <-].
   by exists n => //=; rewrite (leq_trans ab).
 - apply: nearW => m.
@@ -2739,11 +2741,11 @@ have mf_ n : measurable_fun D (fun x => (f_ n x)%:E).
 have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin.
 have cvg_f_ (m : {measure set T -> \bar R}) :
     cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E).
-  apply: ereal_nondecreasing_is_cvg => a b ab.
+  apply: ereal_nondecreasing_is_cvgn => a b ab.
   apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|].
   by move=> t Dt; rewrite lee_fin; apply/lefP/f_nd.
 transitivity (limn (fun n =>
-    \int[measure_add [the measure _ _ of msum m_ N] (m_ N)]_(x in D) (f_ n x)%:E)).
+    \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//; last first.
     by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd.
   by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: f_f.
@@ -3215,7 +3217,7 @@ have lim_f_ t : f_ ^~ t @ \oo --> (f \_ D) t.
       by rewrite /f_ patchN// big_mkord big_ord0 inE/= in_set0.
     apply: ub_ereal_sup => x [n _ <-].
     by rewrite /f_ restrict_lee// big_mkord; exact: bigsetU_bigcup.
-  apply: ereal_nondecreasing_cvg => a b ab.
+  apply: ereal_nondecreasing_cvgn => a b ab.
   rewrite /f_ !big_mkord restrict_lee //; last exact: subset_bigsetU.
   by move=> x Dx; apply: f0 => //; exact: bigsetU_bigcup Dx.
 transitivity (\int[mu]_x limn (f_ ^~ x)).

theories/measure.v

@@ -3566,7 +3566,7 @@ suff : forall n, \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X.
   move=> XA; rewrite (_ : limn _ = ereal_sup
       ((fun n => \sum_(k < n) mu (X `&` A k)) @` setT)); last first.
     under eq_fun do rewrite big_mkord.
-    apply/cvg_lim => //; apply: ereal_nondecreasing_cvg.
+    apply/cvg_lim => //; apply: ereal_nondecreasing_cvgn.
     apply: (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _.
     exact: outer_measure_ge0.
   move XAx : (mu (X `&` ~` A')) => [x| |].