Merge branch 'master' into markov

Author: dennj

Mathlib/Analysis/Normed/Module/Connected.lean

@@ -31,7 +31,8 @@ public section
 assert_not_exists Subgroup.index Nat.divisors
 -- TODO assert_not_exists Cardinal
 
-open Convex Set Metric
+open Set Metric
+open scoped Convex ENNReal
 
 section TopologicalVectorSpace
 
@@ -135,39 +136,70 @@ section Ball
 
 namespace Metric
 
-theorem ball_contractible {x : E} {r : ℝ} (hr : 0 < r) :
+theorem contractibleSpace_ball {x : E} {r : ℝ} (hr : 0 < r) :
     ContractibleSpace (ball x r) :=
-  Convex.contractibleSpace (convex_ball _ _) (by simpa)
-
-theorem eball_contractible {x : E} {r : ENNReal} (hr : 0 < r) :
-    ContractibleSpace (Metric.eball x r) := by
-  cases r with
-  | top =>
-    rw [eball_top_eq_univ, (Homeomorph.Set.univ E).contractibleSpace_iff]
-    exact RealTopologicalVectorSpace.contractibleSpace
-  | coe r =>
-    rw [Metric.eball_coe]
-    apply ball_contractible
-    simpa using hr
+  (convex_ball _ _).contractibleSpace (by simpa)
+
+@[deprecated (since := "2026-02-02")]
+alias ball_contractible := contractibleSpace_ball
+
+theorem contractibleSpace_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    ContractibleSpace (eball x r) :=
+  (convex_eball _ _).contractibleSpace ⟨x, by simpa⟩
+
+@[deprecated (since := "2026-02-02")]
+alias eball_contractible := contractibleSpace_eball
+
+theorem contractibleSpace_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) :
+    ContractibleSpace (closedBall x r) :=
+  (convex_closedBall _ _).contractibleSpace (by simpa)
+
+instance contractibleSpace_closedEBall {x : E} {r : ℝ≥0∞} :
+    ContractibleSpace (closedEBall x r) :=
+  (convex_closedEBall _ _).contractibleSpace ⟨x, by simp⟩
 
 theorem isPathConnected_ball {x : E} {r : ℝ} (hr : 0 < r) :
-    IsPathConnected (ball x r) := by
-  rw [isPathConnected_iff_pathConnectedSpace]
-  exact @ContractibleSpace.instPathConnectedSpace _ _ (ball_contractible hr)
+    IsPathConnected (ball x r) :=
+  convex_ball _ _ |>.isPathConnected <| by simpa
+
+theorem isPathConnected_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    IsPathConnected (eball x r) :=
+  convex_eball _ _ |>.isPathConnected ⟨x, by simpa⟩
+
+theorem isPathConnected_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) :
+    IsPathConnected (closedBall x r) :=
+  convex_closedBall _ _ |>.isPathConnected ⟨x, by simpa⟩
 
-theorem isPathConnected_eball {x : E} {r : ENNReal} (hr : 0 < r) :
-    IsPathConnected (Metric.eball x r) := by
-  rw [isPathConnected_iff_pathConnectedSpace]
-  exact @ContractibleSpace.instPathConnectedSpace _ _ (eball_contractible hr)
+theorem isPathConnected_closedEBall {x : E} {r : ℝ≥0∞} :
+    IsPathConnected (closedEBall x r) :=
+  isPathConnected_iff_pathConnectedSpace.mpr inferInstance
+
+theorem isPreconnected_ball {x : E} {r : ℝ} : IsPreconnected (ball x r) :=
+  (convex_ball _ _).isPreconnected
+
+theorem isPreconnected_eball {x : E} {r : ℝ≥0∞} : IsPreconnected (eball x r) :=
+  (convex_eball _ _).isPreconnected
+
+theorem isPreconnected_closedBall {x : E} {r : ℝ} : IsPreconnected (closedBall x r) :=
+  (convex_closedBall _ _).isPreconnected
+
+theorem isPreconnected_closedEBall {x : E} {r : ℝ≥0∞} : IsPreconnected (closedEBall x r) :=
+  (convex_closedEBall _ _).isPreconnected
 
 theorem isConnected_ball {x : E} {r : ℝ} (hr : 0 < r) :
     IsConnected (ball x r) :=
   (isPathConnected_ball hr).isConnected
 
-theorem isConnected_eball {x : E} {r : ENNReal} (hr : 0 < r) :
-    IsConnected (Metric.eball x r) :=
+theorem isConnected_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    IsConnected (eball x r) :=
   (isPathConnected_eball hr).isConnected
 
+theorem isConnected_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) : IsConnected (closedBall x r) :=
+  ⟨⟨x, by simpa⟩, isPreconnected_closedBall⟩
+
+theorem isConnected_closedEBall {x : E} {r : ℝ≥0∞} : IsConnected (closedEBall x r) :=
+  ⟨⟨x, mem_closedEBall_self⟩, isPreconnected_closedEBall⟩
+
 end Metric
 
 end Ball

Mathlib/Analysis/Normed/Module/Convex.lean

@@ -60,12 +60,22 @@ theorem convexOn_dist (z : E) (hs : Convex ℝ s) : ConvexOn ℝ s fun z' => dis
 theorem convexOn_univ_dist (z : E) : ConvexOn ℝ univ fun z' => dist z' z :=
   convexOn_dist z convex_univ
 
-theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (Metric.ball a r) := by
+theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (ball a r) := by
   simpa only [Metric.ball, sep_univ] using (convexOn_univ_dist a).convex_lt r
 
+theorem convex_eball (a : E) (r : ENNReal) : Convex ℝ (eball a r) := by
+  cases r with
+  | top => simp [convex_univ]
+  | coe r => simp [eball_coe, convex_ball]
+
 theorem convex_closedBall (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r) := by
   simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r
 
+theorem convex_closedEBall (a : E) (r : ENNReal) : Convex ℝ (closedEBall a r) := by
+  cases r with
+  | top => simp [convex_univ]
+  | coe r => simp [closedEBall_coe, convex_closedBall]
+
 open Pointwise in
 theorem convexHull_sphere_eq_closedBall {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
     [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) :