[Merged by Bors] - chore(Analysis): rename closedUnitBall and closed_unit_ball to unitClosedBall

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -745,7 +745,7 @@ theorem integrable_of_continuousOn [CompleteSpace E] {I : Box ι} {f : ℝⁿ 
   · obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                         (I.isCompact_Icc.image_of_continuousOn hc).isBounded
     use ‖C‖, fun x hx ↦ by
-      simpa only [smul_closedUnitBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)
+      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)
   · refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)
     rw [mem_ae_iff, μ.restrict_apply] <;> simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]
 

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -630,7 +630,7 @@ instance instCStarRing : CStarRing 𝓜(𝕜, A) where
     On the other hand, for any `‖z‖ ≤ 1`, we may choose `x := star z` and `y := z` to get:
     `‖star (L (star x)) * L y‖ = ‖star (L z) * (L z)‖ = ‖L z‖ ^ 2`, and taking the supremum over
     all such `z` yields that the supremum is at least `‖L‖ ^ 2`. It is the latter part of the
-    argument where `DenselyNormedField 𝕜` is required (for `sSup_closed_unit_ball_eq_nnnorm`). -/
+    argument where `DenselyNormedField 𝕜` is required (for `sSup_unitClosedBall_eq_nnnorm`). -/
       have hball : (Metric.closedBall (0 : A) 1).Nonempty :=
         Metric.nonempty_closedBall.2 zero_le_one
       have key :
@@ -645,17 +645,17 @@ instance instCStarRing : CStarRing 𝓜(𝕜, A) where
               (a.fst.le_opNorm_of_le hy))
           _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
       rw [← nnnorm_snd]
-      simp only [mul_snd, ← sSup_closed_unit_ball_eq_nnnorm, star_snd, mul_apply]
+      simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply]
       simp only [← @opNNNorm_mul_apply 𝕜 _ A]
-      simp only [← sSup_closed_unit_ball_eq_nnnorm, mul_apply']
+      simp only [← sSup_unitClosedBall_eq_nnnorm, mul_apply']
       refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_
       · rintro - ⟨x, hx, rfl⟩
         refine csSup_le (hball.image _) ?_
         rintro - ⟨y, hy, rfl⟩
         exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)
       · simp only [Set.mem_image, Set.mem_setOf_eq, exists_prop, exists_exists_and_eq_and]
         have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt.2 hr
-        simp_rw [← nnnorm_fst, ← sSup_closed_unit_ball_eq_nnnorm] at hr'
+        simp_rw [← nnnorm_fst, ← sSup_unitClosedBall_eq_nnnorm] at hr'
         obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'
         have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx
         refine ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), ?_⟩

Mathlib/Analysis/CStarAlgebra/Unitization.lean

@@ -60,7 +60,7 @@ variable (E)
 instance CStarRing.instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where
   isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 E) fun a => NNReal.eq_iff.mp <|
     show ‖mul 𝕜 E a‖₊ = ‖a‖₊ by
-    rw [← sSup_closed_unit_ball_eq_nnnorm]
+    rw [← sSup_unitClosedBall_eq_nnnorm]
     refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_
     · exact (Metric.nonempty_closedBall.mpr zero_le_one).image _
     · rintro - ⟨x, hx, rfl⟩
@@ -87,12 +87,12 @@ variable {E}
 out so that declaring the `CStarRing` instance doesn't time out. -/
 theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
     ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤ ‖(Unitization.splitMul 𝕜 E (star x * x)).snd‖ := by
-  /- The key idea is that we can use `sSup_closed_unit_ball_eq_norm` to make this about
+  /- The key idea is that we can use `sSup_unitClosedBall_eq_norm` to make this about
   applying this linear map to elements of norm at most one. There is a bit of `sqrt` and `sq`
   shuffling that needs to occur, which is primarily just an annoyance. -/
   refine (Real.le_sqrt (norm_nonneg _) (norm_nonneg _)).mp ?_
   simp only [Unitization.splitMul_apply]
-  rw [← sSup_closed_unit_ball_eq_norm]
+  rw [← sSup_unitClosedBall_eq_norm]
   refine csSup_le ((Metric.nonempty_closedBall.2 zero_le_one).image _) ?_
   rintro - ⟨b, hb, rfl⟩
   simp only
@@ -101,7 +101,7 @@ theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
     ← CStarRing.norm_star_mul_self, ContinuousLinearMap.add_apply, star_add, mul_apply',
     Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply,
     ContinuousLinearMap.one_apply, star_mul, star_smul, add_mul, smul_mul_assoc, ← mul_smul_comm,
-    mul_assoc, ← mul_add, ← sSup_closed_unit_ball_eq_norm]
+    mul_assoc, ← mul_add, ← sSup_unitClosedBall_eq_norm]
   refine (norm_mul_le _ _).trans ?_
   calc
     _ ≤ ‖star x.fst • (x.fst • b + x.snd * b) + star x.snd * (x.fst • b + x.snd * b)‖ := by

Mathlib/Analysis/Convex/StrictConvexSpace.lean

@@ -35,7 +35,7 @@ In a strictly convex space, we prove
 
 We also provide several lemmas that can be used as alternative constructors for `StrictConvex ℝ E`:
 
-- `StrictConvexSpace.of_strictConvex_closed_unit_ball`: if `closed_ball (0 : E) 1` is strictly
+- `StrictConvexSpace.of_strictConvex_unitClosedBall`: if `closed_ball (0 : E) 1` is strictly
   convex, then `E` is a strictly convex space;
 
 - `StrictConvexSpace.of_norm_add`: if `‖x + y‖ = ‖x‖ + ‖y‖` implies `SameRay ℝ x y` for all
@@ -57,7 +57,7 @@ open Convex Pointwise Set Metric
 require balls of positive radius with center at the origin to be strictly convex in the definition,
 then prove that any closed ball is strictly convex in `strictConvex_closedBall` below.
 
-See also `StrictConvexSpace.of_strictConvex_closed_unit_ball`. -/
+See also `StrictConvexSpace.of_strictConvex_unitClosedBall`. -/
 class StrictConvexSpace (𝕜 E : Type*) [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] : Prop where
   strictConvex_closedBall : ∀ r : ℝ, 0 < r → StrictConvex 𝕜 (closedBall (0 : E) r)
@@ -76,9 +76,13 @@ theorem strictConvex_closedBall [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) :
 variable [NormedSpace ℝ E]
 
 /-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
-theorem StrictConvexSpace.of_strictConvex_closed_unit_ball [LinearMap.CompatibleSMul E E 𝕜 ℝ]
+theorem StrictConvexSpace.of_strictConvex_unitClosedBall [LinearMap.CompatibleSMul E E 𝕜 ℝ]
     (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E :=
-  ⟨fun r hr => by simpa only [smul_closedUnitBall_of_nonneg hr.le] using h.smul r⟩
+  ⟨fun r hr => by simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r⟩
+
+@[deprecated (since := "2024-12-01")]
+alias StrictConvexSpace.of_strictConvex_closed_unit_ball :=
+  StrictConvexSpace.of_strictConvex_unitClosedBall
 
 /-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`
 and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
@@ -87,7 +91,7 @@ theorem StrictConvexSpace.of_norm_combo_lt_one
     (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ‖a • x + b • y‖ < 1) :
     StrictConvexSpace ℝ E := by
   refine
-    StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
+    StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
       ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)
   rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
     mem_sphere_zero_iff_norm] at hx hy
@@ -101,7 +105,7 @@ theorem StrictConvexSpace.of_norm_combo_ne_one
       ∀ x y : E,
         ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) :
     StrictConvexSpace ℝ E := by
-  refine StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
+  refine StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
     ((convex_closedBall _ _).strictConvex ?_)
   simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise,
     frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]
@@ -164,8 +168,8 @@ theorem norm_add_lt_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x + y‖ < ‖x
   rw [← norm_pos_iff] at hx hy
   have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
   have :=
-    combo_mem_ball_of_ne (inv_norm_smul_mem_closed_unit_ball x)
-      (inv_norm_smul_mem_closed_unit_ball y) hne (div_pos hx hxy) (div_pos hy hxy)
+    combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x)
+      (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy) (div_pos hy hxy)
       (by rw [← add_div, div_self hxy.ne'])
   rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
     smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -758,10 +758,13 @@ lemma norm_le_one_of_discrete
   · simp
   · simp [norm_eq_one_iff_ne_zero_of_discrete.mpr hx]
 
-lemma discreteTopology_unit_closedBall_eq_univ : (Metric.closedBall 0 1 : Set 𝕜) = Set.univ := by
+lemma unitClosedBall_eq_univ_of_discrete : (Metric.closedBall 0 1 : Set 𝕜) = Set.univ := by
   ext
   simp
 
+@[deprecated (since := "2024-12-01")]
+alias discreteTopology_unit_closedBall_eq_univ := unitClosedBall_eq_univ_of_discrete
+
 end Discrete
 
 end NormedDivisionRing

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -429,7 +429,7 @@ lemma NormedField.completeSpace_iff_isComplete_closedBall {K : Type*} [NormedFie
   · exact Metric.isClosed_ball.isComplete
   rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _|⟨_, rfl⟩
   · rwa [completeSpace_iff_isComplete_univ,
-         ← NormedDivisionRing.discreteTopology_unit_closedBall_eq_univ]
+         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
   refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
   obtain ⟨k, hk⟩ := hu.norm_bddAbove
   have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))

Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

@@ -190,7 +190,7 @@ theorem sSup_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
     sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖ := by
   simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_unit_ball_eq_nnnorm
 
-theorem sSup_closed_unit_ball_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
+theorem sSup_unitClosedBall_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
     [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
     [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
     sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊ := by
@@ -202,12 +202,18 @@ theorem sSup_closed_unit_ball_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCom
   exact csSup_le_csSup ⟨‖f‖₊, hbdd⟩ ((nonempty_ball.2 zero_lt_one).image _)
     (Set.image_subset _ ball_subset_closedBall)
 
-theorem sSup_closed_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
+@[deprecated (since := "2024-12-01")]
+alias sSup_closed_unit_ball_eq_nnnorm := sSup_unitClosedBall_eq_nnnorm
+
+theorem sSup_unitClosedBall_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
     [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
     [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
     sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖ := by
   simpa only [NNReal.coe_sSup, Set.image_image] using
-    NNReal.coe_inj.2 f.sSup_closed_unit_ball_eq_nnnorm
+    NNReal.coe_inj.2 f.sSup_unitClosedBall_eq_nnnorm
+
+@[deprecated (since := "2024-12-01")]
+alias sSup_closed_unit_ball_eq_norm := sSup_unitClosedBall_eq_norm
 
 end Sup
 

Mathlib/Analysis/NormedSpace/Pointwise.lean

@@ -361,16 +361,21 @@ theorem smul_closedBall (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
   · simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]
   · exact smul_closedBall' hc x r
 
-theorem smul_closedUnitBall (c : 𝕜) : c • closedBall (0 : E) (1 : ℝ) = closedBall (0 : E) ‖c‖ := by
+theorem smul_unitClosedBall (c : 𝕜) : c • closedBall (0 : E) (1 : ℝ) = closedBall (0 : E) ‖c‖ := by
   rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]
 
+@[deprecated (since := "2024-12-01")] alias smul_closedUnitBall := smul_unitClosedBall
+
 variable [NormedSpace ℝ E]
 
 /-- In a real normed space, the image of the unit closed ball under multiplication by a nonnegative
 number `r` is the closed ball of radius `r` with center at the origin. -/
-theorem smul_closedUnitBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
+theorem smul_unitClosedBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
     r • closedBall (0 : E) 1 = closedBall (0 : E) r := by
-  rw [smul_closedUnitBall, Real.norm_of_nonneg hr]
+  rw [smul_unitClosedBall, Real.norm_of_nonneg hr]
+
+@[deprecated (since := "2024-12-01")]
+alias smul_closedUnitBall_of_nonneg := smul_unitClosedBall_of_nonneg
 
 /-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
 nonnegative. -/
@@ -400,6 +405,6 @@ theorem affinity_unitBall {r : ℝ} (hr : 0 < r) (x : E) : x +ᵥ r • ball (0
 `fun y ↦ x + r • y`. -/
 theorem affinity_unitClosedBall {r : ℝ} (hr : 0 ≤ r) (x : E) :
     x +ᵥ r • closedBall (0 : E) 1 = closedBall x r := by
-  rw [smul_closedUnitBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
+  rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
 
 end NormedAddCommGroup

Mathlib/Analysis/NormedSpace/Real.lean

@@ -35,11 +35,14 @@ section Seminormed
 
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E]
 
-theorem inv_norm_smul_mem_closed_unit_ball (x : E) :
+theorem inv_norm_smul_mem_unitClosedBall (x : E) :
     ‖x‖⁻¹ • x ∈ closedBall (0 : E) 1 := by
   simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
     div_self_le_one]
 
+@[deprecated (since := "2024-12-01")]
+alias inv_norm_smul_mem_closed_unit_ball := inv_norm_smul_mem_unitClosedBall
+
 theorem norm_smul_of_nonneg {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖ := by
   rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
 

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -461,7 +461,7 @@ theorem addHaar_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :
     μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1) := by
   rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]
 
-theorem addHaar_closed_unit_ball_eq_addHaar_unit_ball :
+theorem addHaar_unitClosedBall_eq_addHaar_unit_ball :
     μ (closedBall (0 : E) 1) = μ (ball 0 1) := by
   apply le_antisymm _ (measure_mono ball_subset_closedBall)
   have A : Tendsto
@@ -476,9 +476,12 @@ theorem addHaar_closed_unit_ball_eq_addHaar_unit_ball :
   rw [← addHaar_closedBall' μ (0 : E) hr.1.le]
   exact measure_mono (closedBall_subset_ball hr.2)
 
+@[deprecated (since := "2024-12-01")]
+alias addHaar_closed_unit_ball_eq_addHaar_unit_ball := addHaar_unitClosedBall_eq_addHaar_unit_ball
+
 theorem addHaar_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :
     μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by
-  rw [addHaar_closedBall' μ x hr, addHaar_closed_unit_ball_eq_addHaar_unit_ball]
+  rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unit_ball]
 
 theorem addHaar_closedBall_eq_addHaar_ball [Nontrivial E] (x : E) (r : ℝ) :
     μ (closedBall x r) = μ (ball x r) := by