From 1836731964d3799f4e0c4eb63ec2049e7dd01649 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 15 Jan 2024 10:21:36 +0000 Subject: [PATCH 1/4] chore(Analysis): rename `closedUnitBall` and `closed_unit_ball` to `unit_closedBall` Since `closedBall` is a function name, it should appear as an unbroken token in the lemma name --- Mathlib/Analysis/BoxIntegral/Basic.lean | 2 +- Mathlib/Analysis/CStarAlgebra/Multiplier.lean | 8 ++++---- Mathlib/Analysis/CStarAlgebra/Unitization.lean | 8 ++++---- Mathlib/Analysis/Convex/StrictConvexSpace.lean | 16 ++++++++-------- Mathlib/Analysis/Normed/Field/Basic.lean | 2 +- Mathlib/Analysis/Normed/Field/Lemmas.lean | 2 +- .../NormedSpace/OperatorNorm/NNNorm.lean | 6 +++--- Mathlib/Analysis/NormedSpace/Pointwise.lean | 8 ++++---- Mathlib/Analysis/NormedSpace/Real.lean | 2 +- .../MeasureTheory/Measure/Lebesgue/EqHaar.lean | 4 ++-- 10 files changed, 29 insertions(+), 29 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index 44c6028cdd79d..b4a22b6102a0b 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/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] diff --git a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean b/Mathlib/Analysis/CStarAlgebra/Multiplier.lean index 8f62eac684540..900b2eb10e19f 100644 --- a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean +++ b/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,9 +645,9 @@ 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 _) ?_ @@ -655,7 +655,7 @@ instance instCStarRing : CStarRing 𝓜(𝕜, A) where 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'), ?_⟩ diff --git a/Mathlib/Analysis/CStarAlgebra/Unitization.lean b/Mathlib/Analysis/CStarAlgebra/Unitization.lean index 94c73b1a5216b..8771d6ba22cae 100644 --- a/Mathlib/Analysis/CStarAlgebra/Unitization.lean +++ b/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 diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean index 32a1cef9cd3a9..5ed62a2c5dffa 100644 --- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean +++ b/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,9 @@ 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⟩ /-- 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 +87,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 +101,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 +164,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, ← diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index 00424d49f8973..ee45d33514e65 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -758,7 +758,7 @@ 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 discreteTopology_unitClosedBall_eq_univ : (Metric.closedBall 0 1 : Set 𝕜) = Set.univ := by ext simp diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean index 2943b39e7e097..95bdaa29109b3 100644 --- a/Mathlib/Analysis/Normed/Field/Lemmas.lean +++ b/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.discreteTopology_unitClosedBall_eq_univ] 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)) diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean index 020de596c8f44..88537a64dd3cb 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean +++ b/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,12 @@ 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] +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 end Sup diff --git a/Mathlib/Analysis/NormedSpace/Pointwise.lean b/Mathlib/Analysis/NormedSpace/Pointwise.lean index 866ca33561073..05f912b750bd2 100644 --- a/Mathlib/Analysis/NormedSpace/Pointwise.lean +++ b/Mathlib/Analysis/NormedSpace/Pointwise.lean @@ -361,16 +361,16 @@ 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] 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] /-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is nonnegative. -/ @@ -400,6 +400,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 diff --git a/Mathlib/Analysis/NormedSpace/Real.lean b/Mathlib/Analysis/NormedSpace/Real.lean index 09c0aa69993d6..062bf811a4319 100644 --- a/Mathlib/Analysis/NormedSpace/Real.lean +++ b/Mathlib/Analysis/NormedSpace/Real.lean @@ -35,7 +35,7 @@ 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] diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index 8a0f8da0ef7ad..afef644f648a1 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/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 @@ -478,7 +478,7 @@ theorem addHaar_closed_unit_ball_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 From 4fa01ee00517e375118e3770a18756b0cae77168 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 1 Dec 2024 22:18:11 +0000 Subject: [PATCH 2/4] deprecated aliases --- Mathlib/Analysis/Convex/StrictConvexSpace.lean | 4 ++++ Mathlib/Analysis/Normed/Field/Basic.lean | 3 +++ Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean | 6 ++++++ Mathlib/Analysis/NormedSpace/Pointwise.lean | 5 +++++ Mathlib/Analysis/NormedSpace/Real.lean | 3 +++ Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean | 3 +++ 6 files changed, 24 insertions(+) diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean index 5ed62a2c5dffa..9e50330e7e3d1 100644 --- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean +++ b/Mathlib/Analysis/Convex/StrictConvexSpace.lean @@ -80,6 +80,10 @@ theorem StrictConvexSpace.of_strictConvex_unitClosedBall [LinearMap.CompatibleSM (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E := ⟨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 check this for points of norm one and some `a`, `b` such that `a + b = 1`. -/ diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index ee45d33514e65..f4aec9fb16673 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -762,6 +762,9 @@ lemma discreteTopology_unitClosedBall_eq_univ : (Metric.closedBall 0 1 : Set ext simp +@[deprecated (since := "2024-12-01")] +alias discreteTopology_unit_closedBall_eq_univ := discreteTopology_unitClosedBall_eq_univ + end Discrete end NormedDivisionRing diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean index 88537a64dd3cb..51f3b1705bfc9 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean @@ -202,6 +202,9 @@ theorem sSup_unitClosedBall_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommG exact csSup_le_csSup ⟨‖f‖₊, hbdd⟩ ((nonempty_ball.2 zero_lt_one).image _) (Set.image_subset _ ball_subset_closedBall) +@[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) : @@ -209,6 +212,9 @@ theorem sSup_unitClosedBall_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGro simpa only [NNReal.coe_sSup, Set.image_image] using 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 end OpNorm diff --git a/Mathlib/Analysis/NormedSpace/Pointwise.lean b/Mathlib/Analysis/NormedSpace/Pointwise.lean index 05f912b750bd2..fb81f7ab0111d 100644 --- a/Mathlib/Analysis/NormedSpace/Pointwise.lean +++ b/Mathlib/Analysis/NormedSpace/Pointwise.lean @@ -364,6 +364,8 @@ theorem smul_closedBall (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) : 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 @@ -372,6 +374,9 @@ theorem smul_unitClosedBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r • closedBall (0 : E) 1 = closedBall (0 : E) r := by 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. -/ @[simp] diff --git a/Mathlib/Analysis/NormedSpace/Real.lean b/Mathlib/Analysis/NormedSpace/Real.lean index 062bf811a4319..aed2117e262d0 100644 --- a/Mathlib/Analysis/NormedSpace/Real.lean +++ b/Mathlib/Analysis/NormedSpace/Real.lean @@ -40,6 +40,9 @@ theorem inv_norm_smul_mem_unitClosedBall (x : E) : 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] diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index afef644f648a1..d0f3276996786 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -476,6 +476,9 @@ theorem addHaar_unitClosedBall_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_unitClosedBall_eq_addHaar_unit_ball] From 4a6a183014696979d285457fe9e2a7f12a632129 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 2 Dec 2024 10:27:57 +0000 Subject: [PATCH 3/4] rename to `unitClosedBall_eq_univ_of_discrete` --- Mathlib/Analysis/Normed/Field/Basic.lean | 4 ++-- Mathlib/Analysis/Normed/Field/Lemmas.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index f4aec9fb16673..4b60173455528 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -758,12 +758,12 @@ lemma norm_le_one_of_discrete · simp · simp [norm_eq_one_iff_ne_zero_of_discrete.mpr hx] -lemma discreteTopology_unitClosedBall_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 := discreteTopology_unitClosedBall_eq_univ +alias discreteTopology_unit_closedBall_eq_univ := unitClosedBall_eq_univ_of_discrete end Discrete diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean index 95bdaa29109b3..37916052cd845 100644 --- a/Mathlib/Analysis/Normed/Field/Lemmas.lean +++ b/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_unitClosedBall_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)) From 6e4fd228de08d8dbd763ceb915a618a7d5bfddd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 18 Dec 2024 12:49:55 +0000 Subject: [PATCH 4/4] rename once more --- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index d0f3276996786..d0e675c84de16 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/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_unitClosedBall_eq_addHaar_unit_ball : +theorem addHaar_unitClosedBall_eq_addHaar_unitBall : μ (closedBall (0 : E) 1) = μ (ball 0 1) := by apply le_antisymm _ (measure_mono ball_subset_closedBall) have A : Tendsto @@ -477,11 +477,11 @@ theorem addHaar_unitClosedBall_eq_addHaar_unit_ball : 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 +alias addHaar_closed_unit_ball_eq_addHaar_unit_ball := addHaar_unitClosedBall_eq_addHaar_unitBall 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_unitClosedBall_eq_addHaar_unit_ball] + rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall] theorem addHaar_closedBall_eq_addHaar_ball [Nontrivial E] (x : E) (r : ℝ) : μ (closedBall x r) = μ (ball x r) := by