break mine_cvg_0_cvg_0 into pieces

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -147,6 +147,11 @@
     `discrete_pseudoMetricType`, and `pseudoMetric_bool`.
   + new lemmas `finite_compact`, `discrete_ball_center`, `compact_cauchy_cvg`
 
+- in `mathcomp_extra.v`:
+  + lemma `lt_min_lt`
+- in `constructive_ereal.v`:
+  + lemmas `EFin_min`, `EFin_max`
+
 ### Changed
 
 - in `mathcomp_extra.v`
@@ -176,6 +181,10 @@
   + weaken condition of `exp_fun_mulrn` and rename to `power_pos_mulrn`
   + the notation ``` `^ ``` has now scope `real_scope`
   + weaken condition of `riemannR_gt0` and `dvg_riemannR`
+- in `constructive_ereal.v`:
+  + `maxEFin` changed to `fine_max`
+  + `minEFin` changed to `fine_min`
+
 
 ### Renamed
 

classical/mathcomp_extra.v

@@ -1134,3 +1134,17 @@ have [b_gt0 _|//|<- _] := ltgtP; last first.
 have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt.
 by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
 Qed.
+
+Section order_min.
+Variables (d : unit) (T : orderType d).
+Import Order.
+Local Open Scope order_scope.
+
+Lemma lt_min_lt (x y z : T) : (min x z < min y z)%O -> (x < y)%O.
+Proof.
+rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
+- by move=> /lt_le_trans; apply; rewrite leNgt.
+- by rewrite ltNge (ltW yz).
+Qed.
+
+End order_min.

theories/charge.v

@@ -383,9 +383,7 @@ Let nuA_d_ x : nu (A_ x) >= mine (d_ x * 2^-1%:E) 1.
 Proof. by move: x => [[[? ?] ?]] []. Qed.
 
 Let nuA_ge0 x : 0 <= nu (A_ x).
-Proof.
-by rewrite (le_trans _ (nuA_d_ _))// /mine; case: ifP => // _; rewrite mule_ge0.
-Qed.
+Proof. by rewrite (le_trans _ (nuA_d_ _))// le_minr lee01 andbT mule_ge0. Qed.
 
 Let subDD A := [set nu E | E in [set E | measurable E /\ E `<=` D `\` A] ].
 
@@ -408,39 +406,62 @@ have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < t_ A.
     by rewrite min_r ?ltey ?gt0_mulye ?leey.
   rewrite -(@fineK _ (t_ A)); last first.
     by rewrite ge0_fin_numE// ?(ltW d_gt0)// lt_neqAle dn1oo leey.
-  rewrite -EFinM minEFin lte_fin lt_minl; apply/orP; left.
+  rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left.
   by rewrite ltr_pdivr_mulr// ltr_pmulr ?ltr1n// fine_gt0// d_gt0/= ltey.
 by exists B; split => //; rewrite (le_trans _ (ltW mnuB)).
 Qed.
 
-(* NB: move outside? *)
-Let mine_cvg_0_cvg_0 (x : (\bar R)^nat) : (forall k, 0 <= x k) ->
-  (fun n => mine (x n * (2^-1)%:E) 1) --> 0 -> x --> 0.
+(* TODO: generalize? *)
+Let minr_cvg_0_cvg_0 (x : R^nat) : (forall k, 0 <= x k)%R ->
+  (fun n => minr (x n * 2^-1) 1)%R --> (0:R)%R -> x --> (0:R)%R.
 Proof.
-move=> x_ge0 /fine_cvgP[_] /[dup] mine_cvg_0.
-move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ ltr01)[N _ hN].
-have xfin : \forall n \near \oo, x n \is a fin_num.
-  near=> n; have /hN : (N <= n)%N by near: n; exists N.
-  rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first.
-    by rewrite le_minr mule_ge0//=.
-  rewrite /mine; case: ifPn => [+ _|_]; last by rewrite ltxx.
-  rewrite ge0_fin_numE// lte_pdivr_mulr// mul1e => /lt_le_trans; apply.
-  by rewrite leey.
-apply/fine_cvgP; split => //.
+move=> x_ge0 minr_cvg.
 apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => _ /posnumP[e].
-move: mine_cvg_0 => /(@cvgrPdist_lt _ [normedModType R of R^o]).
 have : (0 < minr (e%:num / 2) 1)%R by rewrite lt_minr// ltr01 andbT divr_gt0.
-move=> /[swap] /[apply] -[M _ hM].
+move/(@cvgrPdist_lt _ [normedModType R of R^o]) : minr_cvg => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.
 have /hM : (M <= n)%N by near: n; exists M.
-rewrite sub0r normrN /mine/=; case: ifPn => [_|_].
-  rewrite fineM//=; last by near: n; exact: xfin.
-  rewrite normrM (@gtr0_norm _ 2^-1%R); last by rewrite invr_gt0.
-  rewrite ltr_pdivr_mulr// => /lt_le_trans; apply.
-  by rewrite minr_pmull// -mulrA mulVr ?unitfE// mulr1 le_minl lexx.
-by rewrite ger0_norm//= lt_minr ltxx andbF.
+rewrite sub0r normrN !ger0_norm// ?le_minr ?divr_ge0//=.
+rewrite -[X in minr _ X](@divrr _ 2) ?unitfE -?minr_pmull//.
+rewrite -[X in (_ < minr _ X)%R](@divrr _ 2) ?unitfE -?minr_pmull//.
+by rewrite ltr_pmul2r//; exact: lt_min_lt.
+Unshelve. all: by end_near. Qed.
+
+Let mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) : (forall k, 0 <= x k) ->
+  (fun n => mine (x n * (2^-1)%:E) 1) --> 0 ->
+  \forall n \near \oo, x n \is a fin_num.
+Proof.
+move=> x_ge0 /fine_cvgP[_].
+move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ ltr01)[N _ hN].
+near=> n; have /hN : (N <= n)%N by near: n; exists N.
+rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first.
+  by rewrite le_minr mule_ge0//=.
+by have := x_ge0 n; case: (x n) => //=; rewrite gt0_mulye//= ltxx.
 Unshelve. all: by end_near. Qed.
 
+Let mine_cvg_minr_cvg (x : (\bar R)^nat) : (forall k, 0 <= x k) ->
+  (fun n => mine (x n * (2^-1)%:E) 1) --> 0 ->
+  (fun n => minr ((fine \o x) n / 2) 1%R) --> (0:R)%R.
+Proof.
+move=> x_ge0 mine_cvg.
+apply: (cvg_trans _ (fine_cvg mine_cvg)).
+move/fine_cvgP : mine_cvg => [_ /=] /(@cvgrPdist_lt _ [normedModType R of R^o]).
+move=> /(_ _ ltr01)[N _ hN]; apply: near_eq_cvg; near=> n.
+have xnoo : x n < +oo.
+  rewrite ltNge leye_eq; apply/eqP => xnoo.
+  have /hN : (N <= n)%N by near: n; exists N.
+  by rewrite /= sub0r normrN xnoo gt0_mulye//= normr1 ltxx.
+by rewrite /= -(@fineK _ (x n)) ?ge0_fin_numE//= -fine_min.
+Unshelve. all: by end_near. Qed.
+
+Let mine_cvg_0_cvg_0 (x : (\bar R)^nat) : (forall k, 0 <= x k) ->
+  (fun n => mine (x n * (2^-1)%:E) 1) --> 0 -> x --> 0.
+Proof.
+move=> x_ge0 h; apply/fine_cvgP; split; first exact: mine_cvg_0_cvg_fin_num.
+apply: (@minr_cvg_0_cvg_0 (fine \o x)) => //; last exact: mine_cvg_minr_cvg.
+by move=> k /=; rewrite fine_ge0.
+Qed.
+
 Lemma hahn_decomposition_lemma : measurable D ->
   {A | [/\ A `<=` D, negative_set nu A & nu A <= nu D]}.
 Proof.
@@ -562,7 +583,7 @@ have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m.
     by rewrite max_r ?ltNye// gt0_mulNye// leNye.
   rewrite -(@fineK _ (s_ U)); last first.
     by rewrite le0_fin_numE// ?(ltW s_lt0)// lt_neqAle leNye eq_sym s0oo.
-  rewrite -EFinM maxEFin lte_fin lt_maxr; apply/orP; left.
+  rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left.
   by rewrite ltr_pdivl_mulr// gtr_nmulr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT.
 have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB.
 exists C; split => //; first exact: (subset_trans CB).

theories/constructive_ereal.v

@@ -2270,18 +2270,26 @@ move=> [x| |] [y| |] //=; first by rewrite normrM.
 - by rewrite mulyy.
 Qed.
 
-Lemma maxEFin r1 r2 : maxe r1%:E r2%:E = (Num.max r1 r2)%:E.
+Lemma fine_max :
+  {in fin_num &, {mono @fine R : x y / maxe x y >-> (Num.max x y)%:E}}.
 Proof.
-by have [ab|ba] := leP r1 r2;
+by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y;
   [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW].
 Qed.
 
-Lemma minEFin r1 r2 : mine r1%:E r2%:E = (Num.min r1 r2)%:E.
+Lemma EFin_max : {morph (@EFin R) : r s / Num.max r s >-> maxe r s}.
+Proof. by move=> a b /=; rewrite -fine_max. Qed.
+
+Lemma fine_min :
+  {in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}.
 Proof.
-by have [ab|ba] := leP r1 r2;
+by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y;
   [apply/min_idPl; rewrite lee_fin|apply/min_idPr; rewrite lee_fin ltW].
 Qed.
 
+Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> mine r s}.
+Proof. by move=> a b /=; rewrite -fine_min. Qed.
+
 Lemma adde_maxl : left_distributive (@adde R) maxe.
 Proof.
 move=> x y z; have [xy|yx] := leP x y.
@@ -2329,7 +2337,7 @@ Canonical mine_comoid := Monoid.ComLaw minC.
 Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
 Proof.
 move=> [x| |] [y| |] //=.
-- by rewrite maxEFin minEFin -EFinN oppr_max.
+- by rewrite -fine_max//= -fine_min//= oppr_max.
 - by rewrite maxey mineNy.
 - by rewrite miney.
 - by rewrite minNye.

theories/lebesgue_integral.v

@@ -1873,7 +1873,7 @@ Proof.
 rewrite bigmax_nnsfunE.
 apply: (@le_trans _ _ (\big[maxe/0%:E]_(i < k) g k x)); last first.
   by apply/bigmax_leP; split => //; apply: g0D.
-rewrite (@big_morph _ _ EFin 0%:E maxe) //; last by move=> *; rewrite maxEFin.
+rewrite (big_morph _ (@EFin_max R) erefl) //.
 apply: le_bigmax2 => i _; rewrite nnsfun_approxE /=.
 by rewrite (le_trans (le_approx _ _ _)) => //; exact/nd_g/ltnW.
 Qed.
@@ -3122,11 +3122,11 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
 have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+.
   rewrite funeqE => x.
   apply/eqP; rewrite -2!addeA [in eqRHS]addeC -sube_eq; last 2 first.
-    by rewrite /funepos /funeneg /g1 /g2 /= !maxEFin.
-    by rewrite /funepos /funeneg /g1 /g2 /= !maxEFin.
+    by rewrite /funepos /funeneg -!fine_max.
+    by rewrite /funepos /funeneg -!fine_max.
   rewrite addeAC eq_sym -sube_eq; last 2 first.
-    by rewrite /funepos /funeneg !maxEFin.
-    by rewrite /funepos /funeneg !maxEFin.
+    by rewrite /funepos /funeneg -!fine_max.
+    by rewrite /funepos /funeneg -!fine_max.
   apply/eqP.
   rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD.
   by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos.

theories/numfun.v

@@ -217,7 +217,7 @@ Qed.
 Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x).
 Proof.
 by rewrite /funeneg /funepos; case: (f x) => [r| |];
-  [rewrite !maxEFin|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr].
+  [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr].
 Qed.
 
 Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.