fixes #1131 (#1132)

* fixes #1131

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -14,7 +14,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

@@ -671,7 +671,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 linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /(_ 0); rewrite 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.
@@ -740,7 +740,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 linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /(_ 0); rewrite 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

@@ -1950,7 +1950,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.
@@ -2089,9 +2089,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.
@@ -2108,8 +2106,7 @@ have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E.
     - by apply: bigcap_measurable => ?.
   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

@@ -1857,7 +1857,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)).
@@ -4043,17 +4043,17 @@ 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; apply: (nbhsx_ballx _ 1%:pos).
+  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; apply: (nbhsx_ballx _ 1%:pos).
+  by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx.
 have abfin : edist (a, b) \is a fin_num.
   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]; apply: (nbhsx_ballx _ (_ / _)%:pos).
+       [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//.
@@ -4145,7 +4145,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.
@@ -5614,7 +5614,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

@@ -5154,13 +5154,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: PseudoMetric.ball_triangle. 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.
@@ -5175,8 +5175,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).
@@ -5234,6 +5233,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).
 
@@ -6252,10 +6254,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.