test with cpoint and radius

theories/lebesgue_measure.v

@@ -928,31 +928,30 @@ Proof. by rewrite ball_itv; exact: measurable_itv. Qed.
 Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R ->
   lebesgue_measure (ball x r) = (r *+ 2)%:E.
 Proof.
-rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite ball0 measure0 mul0rn.
+rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite ball0// measure0 mul0rn.
 rewrite ball_itv lebesgue_measure_itv hlength_itv/=.
 rewrite lte_fin ltr_subl_addr -addrA ltr_addl addr_gt0 //.
 by rewrite -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
 Qed.
 
-Lemma measurable_closed_ball (x : R) r : 0 <= r -> measurable (closed_ball x r).
+Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r).
 Proof.
-rewrite le_eqVlt => /predU1P[<-|]; first by rewrite closed_ball0.
-by move=> r0; rewrite closed_ball_itv.
+have [r0|r0] := leP r 0; first by rewrite closed_ball0.
+by rewrite closed_ball_itv.
 Qed.
 
 Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r ->
   lebesgue_measure (closed_ball x r) = (r *+ 2)%:E.
 Proof.
-rewrite le_eqVlt => /predU1P[<-|r0].
-  by rewrite mul0rn closed_ball0 measure0.
+rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0.
 rewrite closed_ball_itv// lebesgue_measure_itv hlength_itv/=.
 rewrite lte_fin -ltr_subl_addl addrAC subrr add0r gtr_opp// ?mulr_gt0//.
 rewrite -EFinD; congr (_%:E).
 by rewrite opprB addrAC addrCA subrr addr0 -mulr2n.
 Qed.
 
-Lemma measurable_scale_cball (k : R) c : 0 <= k -> measurable (scale_cball k c).
-Proof. by move=> k0; apply: measurable_closed_ball; rewrite mulr_ge0. Qed.
+Lemma measurable_scale_cball (k : R) c : measurable (scale_cball k c).
+Proof. exact: measurable_closed_ball. Qed.
 
 End measurable_ball.
 

theories/normedtype.v

@@ -5779,9 +5779,10 @@ End continuous.
 Section ball_realFieldType.
 Variables (R : realFieldType).
 
-Lemma ball0 (x : R) : ball x 0 = set0.
+Lemma ball0 (a r : R) : r <= 0 -> ball a r = set0.
 Proof.
-by apply/seteqP; split => // y; rewrite /ball/= ltNge normr_ge0.
+move=> r0; apply/seteqP; split => // y; rewrite /ball/=.
+by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0.
 Qed.
 
 Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R.
@@ -5816,9 +5817,10 @@ Qed.
 Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
   (x : V) (e : R) := closure (ball x e).
 
-Lemma closed_ball0 (R : realFieldType) (x : R) : closed_ball x 0 = set0.
+Lemma closed_ball0 (R : realFieldType) (a r : R) :
+  r <= 0 -> closed_ball a r = set0.
 Proof.
-by apply/seteqP; split => // y; rewrite /closed_ball ball0 closure0.
+by move=> r0; apply/seteqP; split => // y; rewrite /closed_ball ball0 ?closure0.
 Qed.
 
 Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V)
@@ -6155,19 +6157,170 @@ Notation linear_continuous0 := __deprecated__linear_continuous0.
   note="generalized to `bounded_linear_continuous`")]
 Notation linear_bounded0 := __deprecated__linear_bounded0.
 
-Section vitali_lemma_finite.
+(* NB: work in progress *)
+Section center_radius.
+Context {R : numDomainType} {M : pseudoMetricType R}.
+
+(* NB: the identifier center is already taken! *)
+Definition cpoint (A : set M) : M :=
+  get [set c | exists r : R, A = ball c r].
+
+Definition radius (A : set M) : {nonneg R} :=
+  xget 0%:nng [set r | A = ball (cpoint A) r%:num].
+
+Definition is_ball (A : set M) : bool := A == ball (cpoint A) (radius A)%:num.
+
+(* scale ball *)
+Definition sball (k : R) (A : set M) : set M :=
+  if is_ball A then ball (cpoint A) (k * (radius A)%:num) else set0.
+
+End center_radius.
+
+(* TODO: replace ball0 with that *)
+Lemma ball0_new (R : realFieldType) (a : R) (r : R) : ball a r = set0 <-> r <= 0.
+Proof.
+split; last exact: ball0.
+move=> /seteqP[+ _] => H; rewrite leNgt; apply/negP => r0.
+by have /(_ (ballxx _ r0)) := H a.
+Qed.
+
+Section center_radius_numDomainType.
+Context {R : numDomainType} {M : pseudoMetricType R}.
+
+Lemma sub_sball (A : set M) k l : k <= l -> sball k A `<=` sball l A.
+Proof.
+move=> kl; rewrite /sball; case: ifPn=> [Aball|_]; last exact: subset_refl.
+by apply: le_ball; rewrite ler_wpmul2r.
+Qed.
+
+Lemma sball1 (A : set M) : is_ball A -> sball 1 A = A.
+ by move=> Aball; rewrite /sball Aball mul1r; move/eqP in Aball. Qed.
+
+End center_radius_numDomainType.
+
+Section center_radius_realFieldType.
+Context {R : realFieldType}.
+
+Let ball_inj_radius_gt0 (x y r s : R) : 0 < r -> ball x r = ball y s -> 0 < s.
+Proof.
+move=> r0 xrys; rewrite ltNge; apply/negP => s0; move: xrys.
+by rewrite (ball0 _ s0) => /seteqP[+ _] => /(_ x); apply; exact: ballxx.
+Qed.
+
+Let ball_inj_center (x y r s : R) : 0 < r -> ball x r = ball y s -> x = y.
+Proof.
+move=> r0 xrys; have s0 := ball_inj_radius_gt0 r0 xrys.
+apply/eqP/negPn/negP => xy.
+wlog : x y r s xrys r0 s0 xy / x < y.
+  move: xy; rewrite neq_lt => /orP[xy|yx].
+    by move/(_ _ _ _ _ xrys); apply => //; rewrite lt_eqF.
+  by move/esym in xrys; move/(_ _ _ _ _ xrys); apply => //; rewrite lt_eqF.
+move=> {}xy.
+have [rs|sr] := ltP r s.
+- pose p := y + r; have : ~ ball x r p.
+    rewrite /ball/= ltr_distlC => /andP[_].
+    by rewrite /p ltr_add2r ltNge (ltW xy).
+  apply.
+  by rewrite xrys /ball/= ltr_distlC /p !ltr_add2l -ltr_norml gtr0_norm.
+- pose p := x - r + minr ((y - x)/2) r; have : ~ ball y s p.
+    rewrite {}/p.
+    have [H|H] := ltP ((y - x) / 2) r.
+      rewrite /ball/= ltr_distlC => /andP[+ _].
+      rewrite -(@ltr_pmul2l _ 2)// !mulrDr mulrCA divff// mulr1 ltNge.
+      move=> /negP; apply.
+      rewrite addrAC !addrA (addrC _ y) mulr_natl mulr2n addrA addrK.
+      rewrite (mulr_natl y) mulr2n -!addrA ler_add2l (ler_add (ltW _))//.
+      by rewrite ler_wpmul2l// ler_oppl opprK.
+    rewrite subrK /ball/= ltr_distlC => /andP[].
+    rewrite ltr_subl_addl addrC -ltr_subl_addl -(@ltr_pmul2r _ (2^-1))//.
+    move=> /le_lt_trans => /(_ _ H) /le_lt_trans => /(_ _ sr).
+    by rewrite ltr_pmulr// invf_gt1// ltNge ler1n.
+  apply.
+  rewrite -xrys /ball/= ltr_distlC; apply/andP; split.
+    by rewrite /p ltr_addl lt_minr divr_gt0// subr_gt0.
+  rewrite /p addrAC ltr_subl_addl addrCA ler_lt_add//.
+  by rewrite lt_minl ltr_addl r0 orbT.
+Qed.
+
+Let ball_inj_radius (x y r s : R) : 0 < r -> ball x r = ball y s -> r = s.
+Proof.
+move=> r0 xrys; have s0 := ball_inj_radius_gt0 r0 xrys.
+have xy := ball_inj_center r0 xrys.
+rewrite {}xy in xrys.
+apply/eqP/negPn/negP; rewrite neq_lt => /orP[rs|sr].
+- set p := y + r.
+  have : ball y s p.
+    rewrite /ball/= ltr_distlC /p !ltr_add2l rs andbT (lt_trans _ r0)//.
+    by rewrite ltr_oppl oppr0 (lt_trans r0).
+  by rewrite -xrys /ball/= ltr_distlC /p ltxx andbF.
+- set p := y + s.
+  have : ball y r p.
+    rewrite /ball/= ltr_distlC /p !ltr_add2l sr andbT (lt_trans _ s0)//.
+    by rewrite ltr_oppl oppr0 (lt_trans s0).
+  by rewrite xrys /ball/= ltr_distlC /p ltxx andbF.
+Qed.
+
+Lemma ball_inj (x y r s : R) : 0 < r -> ball x r = ball y s -> x = y /\ r = s.
+Proof.
+by move=> r0 xrys; split; [exact: (ball_inj_center r0 xrys)|
+                           exact: (ball_inj_radius r0 xrys)].
+Qed.
+
+Lemma radius0 : radius (@set0 R) = 0%:nng :> {nonneg R}.
+Proof.
+rewrite /radius/=; case: xgetP => [r _ /= /esym/ball0_new r0|]/=.
+  by apply/val_inj/eqP; rewrite /= eq_le r0/=.
+by move/(_ 0%:nng) => /=; rewrite ball0.
+Qed.
+
+Lemma is_ball0 : is_ball (@set0 R).
+Proof.
+rewrite /is_ball; apply/eqP/seteqP; split => // x.
+by rewrite radius0/= ball0.
+Qed.
+
+Lemma cpoint_ball (x r : R) : 0 < r -> cpoint (ball x r) = x.
+Proof.
+move=> r0; rewrite /cpoint; case: xgetP => [y _ [s] /ball_inj|].
+  by move=> /(_ r0)[].
+by move/(_ x) => /forallNP/(_ r).
+Qed.
+
+Lemma radius_ball (x r : R) : 0 <= r -> (radius (ball x r))%:num = r.
+Proof.
+rewrite le_eqVlt => /orP[/eqP r0|r0].
+  by rewrite ball0// ?radius0// -r0.
+rewrite /radius; case: xgetP => [y _ /ball_inj|].
+  by move=> /(_ r0)[].
+by move=> /(_ (NngNum (ltW r0)))/=; rewrite cpoint_ball.
+Qed.
+
+Lemma radius_ball' (x r : R) (r0 : 0 <= r) : radius (ball x r) = NngNum r0.
+Proof. by apply/val_inj => //=; rewrite radius_ball. Qed.
+
+Lemma is_ball_ball (x r : R) : is_ball (ball x r).
+Proof.
+have [r0|r0] := ltP 0 r; last by rewrite ball0// is_ball0.
+by apply/eqP; rewrite cpoint_ball// (radius_ball _ (ltW r0)).
+Qed.
+
+End center_radius_realFieldType.
+
+Section vitali_lemma_finite_new.
 Context {R : realType} {I : eqType}.
-Variable (B : I -> R * {posnum R}).
+Variable (B : I -> set R).
+Hypothesis is_ballB : forall i, is_ball (B i).
+Hypothesis B_set0 : forall i, B i !=set0.
 
-Lemma vitali_lemma_finite (s : seq I) :
+Lemma vitali_lemma_finite_new (s : seq I) :
   { D : seq I | [/\
-    {subset D <= s}, trivIset [set` D] (scale_ball 1 \o B) &
+    {subset D <= s}, trivIset [set` D] B &
     forall i, i \in s -> exists j, [/\ j \in D,
-      scale_ball 1 (B i) `&` scale_ball 1 (B j) !=set0,
-      (B j).2 >= (B i).2 &
-      scale_ball 1 (B i) `<=` scale_ball 3%:R (B j)] ] }.
+      B i `&` B j !=set0,
+      radius (B j) >= radius (B i) &
+      B i `<=` sball 3%:R (B j)] ] }.
 Proof.
-pose LE x y := (B x).2 <= (B y).2.
+pose LE x y := radius (B x) <= radius (B y).
 have LE_trans : transitive LE by move=> x y z; exact: le_trans.
 wlog : s / sorted LE s.
   have : sorted LE (sort LE s) by apply: sort_sorted => x y; exact: le_total.
@@ -6177,42 +6330,99 @@ wlog : s / sorted LE s.
 elim: s => [_|i [/= _ _|j t]]; first by exists nil.
   exists [:: i]; split => //; first by rewrite set_cons1; exact: trivIset1.
   move=> _ /[1!inE] /eqP ->; exists i; split => //; first by rewrite mem_head.
-  - by rewrite setIid; exact: scale_ball_neq0.
-  - by apply: sub_scale_ball; rewrite ler1n.
+  - by rewrite setIid; exact: B_set0.
+  - rewrite -[X in X `<=` _](sball1 (is_ballB i)); apply: sub_sball.
+    by rewrite ler1n.
 rewrite /= => + /andP[ij jt] => /(_ jt)[u [ujt trivIset_uB H]].
 have [K|] := pselect (forall j, j \in u ->
-    scale_ball 1 (B j) `&` scale_ball 1 (B i) = set0).
+    B j `&` B i = set0).
   exists (i :: u); split => //.
   - move=> x /[1!inE] /predU1P[->|]; first by rewrite mem_head.
     by move/ujt => xjt; rewrite in_cons xjt orbT.
   - move=> k l /= /[1!inE] /predU1P[->{k}|ku].
       by move=> /predU1P[->{j}//|js] /set0P; rewrite setIC K// eqxx.
     by move=> /predU1P[->{l} /set0P|lu]; [rewrite K// eqxx|exact: trivIset_uB].
   - move=> k /[1!inE] /predU1P[->{k}|].
-      exists i; split => //; first by rewrite mem_head.
-      by rewrite setIid; exact: scale_ball_neq0.
-      by apply: sub_scale_ball; rewrite ler1n.
+      exists i; split; [by rewrite mem_head| |exact: lexx|].
+        by rewrite setIid; exact: B_set0.
+      rewrite -[X in X `<=` _](sball1 (is_ballB i)); apply: sub_sball.
+      by rewrite ler1n.
     by move/H => [l [lu lk0 kl k3l]]; exists l; split => //; rewrite inE lu orbT.
 move/existsNP/cid => [k /not_implyP[ku /eqP/set0P ki0]].
 exists u; split => //.
   by move=> l /ujt /[!inE] /predU1P[->|->]; rewrite ?eqxx ?orbT.
-move=> _ /[1!inE] /predU1P[->|/H//]; exists k; split => //.
+move=> _ /[1!inE] /predU1P[->|/H//]; exists k; split; [exact: ku| | |].
 - by rewrite setIC.
-- rewrite (le_trans ij)//; move/ujt : ku => /[1!inE] /predU1P[<-//|kt].
-  by have /allP := order_path_min LE_trans jt; exact.
-- case: ki0 => x [Bkx Bix] y; rewrite scale_ball1 /ball /= => iy.
-  rewrite /scale_ball /ball /= -(subrK x y) -(addrC x) opprD addrA opprB.
+- apply: (le_trans ij); move/ujt : ku => /[1!inE] /predU1P[<-|kt].
+    exact: lexx.
+  by have /allP := order_path_min LE_trans jt; apply; exact: kt.
+- case: ki0 => x [Bkx Bix] y => iy.
+  rewrite /sball is_ballB// /ball/= -(subrK x y) -(addrC x) opprD addrA opprB.
   rewrite (le_lt_trans (ler_norm_add _ _))// (_ : 3%:R = 1 + 2%:R)//.
-  rewrite mulrDl mul1r mulr_natl ltr_add//.
-    by move: Bkx; rewrite scale_ball1.
-  rewrite -(subrK (B i).1 y) -(addrC (B i).1) opprD addrA opprB.
+  rewrite mulrDl mul1r mulr_natl; apply: ltr_add.
+    move: Bkx.
+    have := is_ballB k.
+    by rewrite /is_ball => /eqP => {1}->.
+  rewrite -(subrK (cpoint (B i)) y) -(addrC (cpoint (B i))) opprD addrA opprB.
   rewrite (le_lt_trans (ler_norm_add _ _))//.
-  rewrite (@lt_le_trans _ _ ((B j).2%:num *+ 2))//; last first.
-    rewrite ler_wmuln2r//; move/ujt : ku; rewrite inE => /predU1P[<-//|kt].
-    by have /allP := order_path_min LE_trans jt; exact.
+  apply (@lt_le_trans _ _ ((radius (B j))%:num *+ 2)); last first.
+    apply: ler_wmuln2r; move/ujt : ku; rewrite inE => /predU1P[<-|kt].
+      exact: lexx.
+    by have /allP := order_path_min LE_trans jt; apply; exact: kt.
   rewrite mulr2n ltr_add//.
-    by move: Bix; rewrite scale_ball1 /ball /= distrC => /lt_le_trans; apply.
-  by move: iy => /lt_le_trans; apply.
+    move: Bix.
+    have := is_ballB i.
+    rewrite /is_ball => /eqP => {1}->.
+    by rewrite /ball/= distrC => /lt_le_trans; apply.
+  move: iy.
+  have := is_ballB i.
+  by rewrite /is_ball => /eqP => {1}-> => /lt_le_trans; exact.
+Qed.
+
+End vitali_lemma_finite_new.
+
+(* TODO: replace with vitali_lemma_finite_new *)
+Section vitali_lemma_finite.
+Context {R : realType} {I : eqType}.
+Variable (B : I -> R * {posnum R}).
+
+Lemma vitali_lemma_finite (s : seq I) :
+  { D : seq I | [/\
+    {subset D <= s}, trivIset [set` D] (scale_ball 1 \o B) &
+    forall i, i \in s -> exists j, [/\ j \in D,
+      scale_ball 1 (B i) `&` scale_ball 1 (B j) !=set0,
+      (B j).2 >= (B i).2 &
+      scale_ball 1 (B i) `<=` scale_ball 3%:R (B j)] ] }.
+Proof.
+pose B_ := fun i => ball (B i).1 (B i).2%:num.
+have B_1 (i : I) : is_ball (B_ i) by rewrite /B_; exact: is_ball_ball.
+have B_2 (i : I) : B_ i !=set0 by exists (B i).1 => /=; exact: ballxx.
+have [D [Ds tB H]] := vitali_lemma_finite_new B_1 B_2 s.
+have B_E : scale_ball 1 \o B = B_.
+  apply/funext => i/=.
+  rewrite /scale_ball/=.
+  have /eqP := B_1 i.
+  rewrite /is_ball.
+  by rewrite cpoint_ball// mul1r radius_ball.
+have sB_E : scale_ball 3 \o B = sball 3 \o B_.
+  apply/funext => i/=.
+  rewrite /scale_ball/=.
+  have /eqP := B_1 i.
+  rewrite cpoint_ball// radius_ball// => ->.
+  by rewrite /sball/= is_ball_ball cpoint_ball// radius_ball.
+exists D; split => //.
+- by rewrite B_E.
+- move=> i si.
+  have [j [jD ij radiusij i3j]] := H _ si.
+  exists j; split => //.
+  + rewrite -![scale_ball 1 (B _)]/((scale_ball 1 \o B) _).
+    by rewrite B_E.
+  + move: radiusij.
+    by rewrite /B_ !radius_ball'.
+  + rewrite -[scale_ball 1 (B _)]/((scale_ball 1 \o B) _).
+    rewrite B_E.
+    rewrite -[scale_ball 3 (B _)]/((scale_ball 3 \o B) _).
+    by rewrite sB_E.
 Qed.
 
 Lemma vitali_lemma_finite_cover (s : seq I) :