fixes #1131 (#1132)

* fixes #1131

CHANGELOG_UNRELEASED.md

@@ -155,7 +155,10 @@
   + `sigma_finite_measure` instance on product measure `\x`
 
 ### Changed
-
+
+- in `topology.v`:
+  + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}`
+
 ### Renamed
 
 ### Generalized

theories/derive.v

@@ -682,7 +682,7 @@ Qed.
 Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) :
   continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|.
 Proof.
-move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)).
 move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
 have [|xn0] := real_le0P (normr_real x).
   by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
@@ -751,7 +751,7 @@ Lemma bilinear_schwarz (U V' W' : normedModType R)
   (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) ->
   exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|.
 Proof.
-move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx _ _ ltr01)).
 move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
 have [|un0] := real_le0P (normr_real u).
   by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r.

theories/lebesgue_measure.v

@@ -1951,7 +1951,7 @@ have finDn n : mu (Dn n) \is a fin_num.
   by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl].
 have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs.
 rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[].
-  exact/nbhs_interior/(nbhsx_ballx _ (PosNum epspos)).
+  exact/nbhs_interior/nbhsx_ballx.
 move=> n _ /(_ _ (leqnn n))/interior_subset muDN.
 exists (-n%:R, n%:R)%R; rewrite measureD//=.
 move: muDN; rewrite /ball/= /ereal_ball/= -fineB//=; last exact: finDn.
@@ -2090,9 +2090,7 @@ have mE k n : measurable (E k n).
 have nEcvg x k : exists n, A x -> (~` (E k n)) x.
   case : (pselect (A x)); last by move => ?; exists point.
   move=> Ax; have [] := fptwsg _ Ax (interior (ball (g x) (k.+1%:R^-1))).
-    apply: open_nbhs_nbhs; split; first exact: open_interior.
-    have ki0 : ((0:R) < k.+1%:R^-1)%R by rewrite invr_gt0.
-    rewrite (_ : k.+1%:R^-1 = (PosNum ki0)%:num ) //; exact: nbhsx_ballx.
+    by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
   move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
   apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
   by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
@@ -2110,8 +2108,7 @@ have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E.
     - by apply: bigcap_measurable => ?.
   rewrite measure0; case/fine_cvg/(_ (interior (ball (0:R) ek))%R).
     apply: open_nbhs_nbhs; split; first exact: open_interior.
-    have ekpos : (0 < ek)%R by rewrite divr_gt0 // divr_gt0.
-    by move: ek ekpos => _/posnumP[ek]; exact: nbhsx_ballx.
+    by apply: nbhsx_ballx; rewrite !divr_gt0.
   move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
   rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
   by apply:(le_lt_trans _ finA); apply: le_measure; rewrite ?inE// => ? [? _ []].

theories/normedtype.v

@@ -1033,7 +1033,7 @@ Lemma dnbhs0_le e : 0 < e -> \forall x \near (0 : V)^', `|x| <= e.
 Proof. by move=> e_gt0; apply: cvg_within; apply: nbhs0_le. Qed.
 
 Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num).
-Proof. rewrite nbhs_nbhs_norm; by apply: nbhsx_ballx. Qed.
+Proof. by rewrite nbhs_nbhs_norm; exact: nbhsx_ballx. Qed.
 
 Lemma nbhsDl (P : set V) (x y : V) :
   (\forall z \near (x + y), P z) <-> (\near x, P (x + y)).
@@ -3180,36 +3180,33 @@ move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E.
 rewrite -ltey -ge0_fin_numE// => efin.
 rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin.
   by have := edist_fin_open efin; apply: filter_app; near=> w.
-move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE.
-move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=.
-have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n.
-exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)).
-  by split => //=; exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)).
-case => a b /= [/ball_sym xar yar]; apply: distrU => /=.
-have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E.
-  by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle.
+apply/cvgrPdist_le => _/posnumP[eps].
+suff: \forall t \near (nbhs x, nbhs y),
+   `|fine (edist (x, y)) - fine (edist t)| <= eps%:num by [].
+rewrite -near2_pair; near=> a b => /=.
+have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E.
+  rewrite (edist_sym x a) -addeA.
+  by rewrite (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle.
+have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E.
+  rewrite (edist_sym y b) -addeA.
+  by rewrite (le_trans (@edist_triangle _ a _))// ?lee_add// ?edist_triangle.
+have xafin : edist (x, a) \is a fin_num.
+  by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx.
+have ybfin : edist (y, b) \is a fin_num.
+  by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx.
 have abfin : edist (a, b) \is a fin_num.
-  rewrite ge0_fin_numE// (le_lt_trans abxy)//.
-  by apply: lte_add_pinfty; [apply: lte_add_pinfty|];
-    rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R).
-have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num.
-  by rewrite abse_fin_num fin_numB abfin efin.
-have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4).
-have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4).
-rewrite /ball/= -fineB// -fine_abse ?fin_numB ?abfin ?efin//.
-rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//.
-  rewrite fine_le// ?fin_numD ?daxr ?dybr//.
-  have [xyab|xyab] := leP (edist (a, b)) (edist (x, y)).
-    rewrite gee0_abs ?subre_ge0// lee_subl_addr//.
-    rewrite (le_trans (@edist_triangle _ a _))// (edist_sym a x) -addeA.
-    by rewrite lee_add// addeC (edist_sym y) edist_triangle.
-  rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC.
-  by rewrite lee_subl_addr// addeAC.
-rewrite fineD // [_%:num]splitr.
-have r42 : r%:num / 4 < r%:num / 2.
-  by rewrite ltr_pM2l// ltf_pV2 ?posrE ?ltr0n// ltr_nat.
-by apply: ltrD; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin.
-Unshelve. end_near. Qed.
+  by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE.
+have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num
+  by rewrite fin_numB abfin efin.
+rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//.
+rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first.
+  by rewrite [eps%:num]splitr/= EFinD lee_add//; apply: edist_fin => //=;
+       [near: a | near: b]; exact: nbhsx_ballx.
+have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)).
+  by rewrite gee0_abs ?subre_ge0// lee_subl_addr// addeAC.
+rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//.
+by rewrite addeC lee_subl_addr// addeAC.
+Unshelve. all: end_near. Qed.
 
 Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E.
 Proof.
@@ -3297,7 +3294,7 @@ have fwfin : \forall w \near z, edist_inf w \is a fin_num.
   rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //.
   exact/ball_sym.
 split => //; apply/cvgrPdist_le => _/posnumP[eps].
-have : nbhs z (ball z eps%:num) by apply: nbhsx_ballx.
+have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx.
 apply: filter_app; near_simpl; move: fwfin; apply: filter_app.
 near=> t => tfin /= /[dup] ?.
 have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num.
@@ -4644,7 +4641,8 @@ move=> x clAx; have abx : x \in `[a, b].
   by apply: interval_closed; have /closureI [] := clAx.
 split=> //; have /sabUf [i Di fx] := abx.
 have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi].
-have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := nbhsx_ballx x e.
+have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] :=
+  nbhsx_ballx x e%:num ltac:(by []).
 exists (i |` E)%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE.
 split=> [z axz|]; last first.
   exists i; first by rewrite /= !inE eq_refl.

theories/topology.v

@@ -5033,13 +5033,13 @@ Lemma ball_triangle (y x z : M) (e1 e2 : R) :
   ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z.
 Proof. exact: ball_triangle_subproof. Qed.
 
-Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num).
-Proof. by apply/nbhs_ballP; exists eps%:num => /=. Qed.
+Lemma nbhsx_ballx (x : M) (eps : R) : 0 < eps -> nbhs x (ball x eps).
+Proof. by move=> e0; apply/nbhs_ballP; exists eps. Qed.
 
 Lemma open_nbhs_ball (x : M) (eps : {posnum R}) : open_nbhs x ((ball x eps%:num)^°).
 Proof.
 split; first exact: open_interior.
-by apply: nbhs_singleton; apply: nbhs_interior; apply:nbhsx_ballx.
+by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhsx_ballx.
 Qed.
 
 Lemma le_ball (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2.
@@ -5054,8 +5054,7 @@ apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA].
 by exists (point, point); apply: sbeA; apply: ballxx.
 Qed.
 
-Lemma near_ball (y : M) (eps : {posnum R}) :
-   \forall y' \near y, ball y eps%:num y'.
+Lemma near_ball (y : M) (eps : R) : 0 < eps -> \forall y' \near y, ball y eps y'.
 Proof. exact: nbhsx_ballx. Qed.
 
 Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a).
@@ -5113,6 +5112,9 @@ End pseudoMetricType_numDomainType.
 #[global] Hint Resolve close_refl : core.
 Arguments close_cvg {T} F1 F2 {FF2} _.
 
+Arguments nbhsx_ballx {R M} x eps.
+Arguments near_ball {R M} y eps.
+
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `cvg_ball`")]
 Notation app_cvg_locally := cvg_ball (only parsing).
 
@@ -5707,10 +5709,10 @@ Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
 Proof.
 move=> x y clxy; apply/eqP; rewrite eq_le.
 apply/in_segment_addgt0Pr => _ /posnumP[e].
-rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos.
-have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he).
+rewrite in_itv /= -ler_distl; have he : 0 < (e%:num / 2) by [].
+have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x _ he) (nbhsx_ballx y _ he).
 have := ball_triangle yz_he (ball_sym zx_he).
-by rewrite -mulr2n -mulr_natr divfK // => /ltW.
+by rewrite -mulr2n -(mulr_natr (_ / _) 2) divfK// => /ltW.
 Qed.
 
 Section RestrictedUniformTopology.