fixes #1471

CHANGELOG_UNRELEASED.md

@@ -155,6 +155,15 @@
 
 - in `normedtype.v`:
   + `cvg_at_right_filter`, `cvg_at_left_filter`
+- in `normedtype.v`
+  + lemma `open_subball`
+  + lemma `interval_unbounded_setT`
+
+- in `derive.v`:
+  + lemmas `decr_derive1_le0`, `incr_derive1_ge0`
+
+- in `lebesgue_measure.v`:
+  + definition `vitali_cover`, lemma `vitali_coverS`
 
 ### Deprecated
 

theories/derive.v

@@ -1755,7 +1755,7 @@ apply: (@ler0_derive1_nincrNy _ (- f)) => //.
   exact: subset_itvl.
 Qed.
 
-Lemma decr_derive1_le0 {R : realType} (f : R -> R) (D : set R) (x : R) :
+Lemma decr_derive1_le0 {R : realFieldType} (f : R -> R) (D : set R) (x : R) :
   {in D^° : set R, forall x, derivable f x 1%R} ->
   {in D &, {homo f : x y /~ x < y}} ->
   D^° x -> f^`() x <= 0.
@@ -1821,7 +1821,7 @@ apply: decr_derive1_le0 zNyb; first by rewrite interior_itv.
 by move=> x y /[!inE]/=; apply/decrf.
 Qed.
 
-Lemma incr_derive1_ge0 {R : realType} (f : R -> R)
+Lemma incr_derive1_ge0 {R : realFieldType} (f : R -> R)
    (D : set R) (x : R):
   {in D^° : set R, forall x : R, derivable f x 1%R} ->
   {in D &, {homo f : x y / (x < y)%R}} ->
@@ -1851,7 +1851,7 @@ Qed.
 Lemma incr_derive1_ge0_itvy {R : realType} (f : R -> R)
     (b0 : bool) (a : R) (z : R) :
   {in `]a, +oo[, forall x : R, derivable f x 1%R} ->
-  {in Interval (BSide b0 a) (BInfty _ false) &, {homo f : x y / (x < y)%R}} ->
+  {in Interval (BSide b0 a) +oo%O &, {homo f : x y / (x < y)%R}} ->
   z \in `]a, +oo[%R -> 0 <= f^`() z.
 Proof.
 move=> df incrf zay; rewrite -[leRHS]opprK oppr_ge0.

theories/lebesgue_measure.v

@@ -2751,7 +2751,7 @@ Qed.
 
 End lebesgue_regularity.
 
-Definition vitali_cover {R : realType} (E : set R) I
+Definition vitali_cover {R : numFieldType} (E : set R) I
     (B : I -> set R) (D : set I) :=
   (forall i, is_ball (B i)) /\
   forall x, E x -> forall e : R, 0 < e -> exists i,
@@ -3020,10 +3020,8 @@ Qed.
 
 End vitali_theorem.
 
-Section vitali_theorem_corollary.
-Context {R : realType} (A : set R) (B : nat -> set R).
-
-Lemma vitali_coverS (F : set nat) (O : set R) : open O -> A `<=` O ->
+Lemma vitali_coverS {R : realFieldType} (A : set R) (B : nat -> set R)
+    (F : set nat) (O : set R) : open O -> A `<=` O ->
   vitali_cover A B F -> vitali_cover A B (F `&` [set k | B k `<=` O]).
 Proof.
 move=> oO AO [Bball ABF]; split => // x Ax r r0.
@@ -3048,6 +3046,9 @@ rewrite distrC (lt_le_trans (is_ballP _ _))//.
 by rewrite (le_trans (ltW Bkd))// ge_min lexx orbT.
 Qed.
 
+Section vitali_theorem_corollary.
+Context {R : realType} (A : set R) (B : nat -> set R).
+
 Let vitali_cover_mclosure (F : set nat) k :
   vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)).
 Proof.

theories/normedtype.v

@@ -4756,10 +4756,7 @@ have : inf X <= inf X - f%:num by exact: inf_lbound.
 by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl.
 Qed.
 
-Section interval_realType.
-Variable R : realType.
-
-Lemma interval_unbounded_setT (X : set R) : is_interval X ->
+Lemma interval_unbounded_setT {R : realFieldType} (X : set R) : is_interval X ->
   ~ has_lbound X -> ~ has_ubound X -> X = setT.
 Proof.
 move=> iX lX uX; rewrite predeqE => x; split => // _.
@@ -4768,6 +4765,9 @@ move/has_ubPn : uX => /(_ x) [z Xz xz].
 by apply: (iX y z); rewrite ?ltW.
 Qed.
 
+Section interval_realType.
+Variable R : realType.
+
 Lemma interval_left_unbounded_interior (X : set R) : is_interval X ->
   ~ has_lbound X -> has_ubound X -> X^° = [set r | r < sup X].
 Proof.
@@ -5503,15 +5503,13 @@ Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V)
   (r : R) : ball x r `<=` closed_ball x r.
 Proof. exact: subset_closure. Qed.
 
-Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M)
+Lemma open_subball {R : numFieldType} {M : normedModType R} (A : set M)
   (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
 Proof.
-move=> aA Ax.
-have /(@nbhs_closedballP R M _ x)[r xrA]: nbhs x A by rewrite nbhsE/=; exists A.
-near=> e.
-apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //.
-by apply: le_ball; near: e; apply: nbhs_right_le.
-Unshelve. all: by end_near. Qed.
+move=> oA Ax; have /nbhsr0P/= : nbhs x A by exact/open_nbhs_nbhs.
+apply: filterS => e xeA y exy; apply: xeA.
+by rewrite -ball_normE/= in exy; exact: ltW.
+Qed.
 
 Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R}
     (K : set M) z : closed K -> ~ K z ->