closed_ball

Co-Auhored-By: Théo Vignon

Co-Authored-By: Cyril Cohen <[email protected]>

Co-Authored-By: Reynald Affeldt @affeldt-aist

Co-Authored-By: @pi8027

theories/normedtype.v

@@ -37,6 +37,7 @@ Require Import classical_sets posnum nngnum topology prodnormedzmodule.
 (*                           `|x| == the norm of x (notation from ssrnum).    *)
 (*                      ball_norm == balls defined by the norm.               *)
 (*                      nbhs_norm == neighborhoods defined by the norm.       *)
+(*                    closed_ball == closure of a ball.                       *)
 (*                                                                            *)
 (* * Domination notations:                                                    *)
 (*              dominated_by h k f F == `|f| <= k * `|h|, near F              *)
@@ -1017,6 +1018,12 @@ rewrite -subr_gt0 => /Fy; apply: filterS => y' yy'; apply: ltW.
 by rewrite -(@ltr_add2r _ (- `|y|)) (le_lt_trans (ler_sub_dist _ _))// distrC.
 Qed.
 
+Lemma normrZV (x : V) :
+  x != 0 -> `| `| x|^-1 *: x | = 1.
+Proof.
+by move=> x0; rewrite normmZ normfV normr_id mulVf // normr_eq0.
+Qed.
+
 End NormedModule_numFieldType.
 Arguments cvg_bounded {_ _ F FF}.
 Hint Extern 0 (hausdorff _) => solve[apply: norm_hausdorff] : core.
@@ -2845,3 +2852,101 @@ rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
 rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Grab Existential Variables. all: end_near. Qed.
+
+
+Section Closed_Ball.
+
+Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R)
+  (x : V) (e : R) := [set y | norm (x - y) <= e ].
+
+Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R)
+  (x : V) (e : R) : closed (closed_ball_ normr x e).
+Proof.
+rewrite /closed_ball_ -/((normr \o (fun y => x - y)) @^-1` [set x | x <= e]).
+apply: (closed_comp _ (@closed_le _ _)) => y _.
+apply: (continuous_comp _ (@norm_continuous _ _ _)).
+exact: (continuousB (@cst_continuous _ _ _ _)).
+Qed.
+
+Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
+  (x : V) (e : R) := closure (ball x e).
+
+Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V)
+  (e : R) : 0 < e -> closed_ball x e x.
+Proof. by move=> ?; exact/subset_closure/ballxx. Qed.
+
+Lemma closed_ballE (R : realFieldType) (V : normedModType R) (x : V)
+  (e : {posnum R}) : closed_ball x e%:num = closed_ball_ normr x e%:num.
+Proof.
+rewrite eqEsubset; split => y.
+  rewrite /closed_ball closureE; apply; split; first exact: closed_closed_ball_.
+  by move=> z; rewrite -ball_normE; exact: ltW.
+have [/eqP -> _|xy] := boolP (x == y); first exact: closed_ballxx.
+rewrite /closed_ball closureE -ball_normE.
+rewrite /closed_ball_ /= le_eqVlt => /orP [/eqP xye B [Bc Be]|xye _ [_ /(_ _ xye)]//].
+apply: Bc => B0 /nbhs_ballP[s s0] B0y.
+have [es|se] := leP s e%:num; last first.
+  exists x; split; first by apply: Be; rewrite ball_normE; apply: ballxx.
+  by apply: B0y; rewrite -ball_normE /ball_ /= distrC xye.
+exists (y + (s / 2) *: (`|x - y|^-1 *: (x - y))); split; [apply: Be|apply: B0y].
+  rewrite /= opprD addrA -[X in `|X - _|](scale1r (x - y)) scalerA -scalerBl.
+  rewrite -[X in X - _](@divrr _ `|x - y|) ?unitfE ?normr_eq0 ?subr_eq0//.
+  rewrite -mulrBl -scalerA normmZ normrZV ?subr_eq0// mulr1.
+  rewrite gtr0_norm; first by rewrite ltr_subl_addl xye ltr_addr mulr_gt0.
+  by rewrite subr_gt0 xye ltr_pdivr_mulr // mulr_natr mulr2n ltr_spaddl.
+rewrite -ball_normE /ball_ /= opprD addrA addrN add0r normrN normmZ.
+rewrite normrZV ?subr_eq0// mulr1 normrM (gtr0_norm s0) gtr0_norm //.
+by rewrite ltr_pdivr_mulr // ltr_pmulr // ltr1n.
+Qed.
+
+Lemma closed_ball_closed (R : realFieldType) (V : normedModType R) (x : V)
+  (e : {posnum R}) : closed (closed_ball x e%:num).
+Proof. by rewrite closed_ballE //; exact: closed_closed_ball_. Qed.
+
+
+Lemma sub_ball_closed (R : numDomainType) (V : pseudoMetricType R) (x : V)
+  (r : R) : exists e, ball x e `<=` closed_ball x r.
+Proof. by exists r; exact: subset_closure. Qed.
+
+Lemma sub_closed_ball (R : realFieldType) (M : normedModType R) (x : M)
+  (r0 r1 : R) : 0 < r0 -> r0 < r1 -> closed_ball x r0 `<=` ball x r1.
+Proof.
+move=> r00 r01; rewrite (_ : r0 = (PosNum r00)%:num) // closed_ballE.
+by move=> m xm; rewrite -ball_normE /ball_ /= (le_lt_trans _ r01).
+Qed.
+
+Lemma nbhs_closedballP (R : realFieldType) (M : normedModType R) (B : set M)
+  (x : M) : nbhs x B <-> exists (r : {posnum R}), closed_ball x r%:num `<=` B.
+Proof.
+split=> [/nbhs_ballP[r r0 xrB]|[e xeB]]; last first.
+  apply/nbhs_ballP; exists e%:num => //.
+  exact: (subset_trans (@subset_closure _ _) xeB).
+have r20 : 0 < r / 2 by apply divr_gt0.
+exists (PosNum r20); apply: (subset_trans (sub_closed_ball _ _) xrB) => //=.
+by rewrite lter_pdivr_mulr // ltr_pmulr // ltr1n.
+Qed.
+
+
+Lemma closed_neigh_ball (R : realFieldType) (V : normedModType R) (x : V)
+  (r : {posnum R}) : open_nbhs x (closed_ball x r%:num)^°.
+Proof.
+split; first exact: open_interior.
+apply: nbhs_singleton; apply/nbhs_interior/nbhs_ballP.
+by exists r%:num => //; exact: subset_closure.
+Qed.
+
+Lemma ball_open (R : realFieldType) (V : normedModType R) (x : V)
+      (r : R) : 0 <r -> open (ball x r).
+Proof. Admitted.
+
+Lemma closed_ball_int (R : realFieldType) (V : normedModType R) (x : V)
+  (r : R) : 0 < r -> (closed_ball x r)^° = ball x r.
+Proof.
+Admitted.
+
+Lemma closed_neigh_ball (R : realFieldType) (V : normedModType R) (x : V)
+      (r: R) : 0<r -> open_nbhs x (closed_ball x r)^°.
+Admitted.
+
+
+End Closed_Ball.