From 948b83f4a806ef57cdc0e6ae548b860e56caafc7 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 09:49:38 +0800 Subject: [PATCH 1/2] refactor(Analysis): golf `Mathlib/Analysis/Normed/Module/Dual` --- Mathlib/Analysis/Normed/Module/Dual.lean | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean index 45de9937f53299..063417bde36ea3 100644 --- a/Mathlib/Analysis/Normed/Module/Dual.lean +++ b/Mathlib/Analysis/Normed/Module/Dual.lean @@ -117,20 +117,9 @@ theorem polar_closedBall {π•œ E : Type*} [RCLike π•œ] [NormedAddCommGroup E] [ theorem polar_ball {π•œ E : Type*} [RCLike π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] {r : ℝ} (hr : 0 < r) : StrongDual.polar π•œ (ball (0 : E) r) = closedBall (0 : StrongDual π•œ E) r⁻¹ := by - apply le_antisymm - Β· intro x hx - rw [mem_closedBall_zero_iff] - apply le_of_forall_gt_imp_ge_of_dense - intro a ha - rw [← mem_closedBall_zero_iff, ← (mul_div_cancel_leftβ‚€ a (Ne.symm (ne_of_lt hr)))] - rw [← RCLike.norm_of_nonneg (K := π•œ) (le_trans zero_le_one - (le_of_lt ((inv_lt_iff_one_lt_mulβ‚€' hr).mp ha)))] - apply polar_ball_subset_closedBall_div _ hr hx - rw [RCLike.norm_of_nonneg (K := π•œ) (le_trans zero_le_one - (le_of_lt ((inv_lt_iff_one_lt_mulβ‚€' hr).mp ha)))] - exact (inv_lt_iff_one_lt_mulβ‚€' hr).mp ha - Β· rw [← polar_closedBall hr] - exact LinearMap.polar_antitone _ ball_subset_closedBall + letI : NormedSpace ℝ E := .restrictScalars ℝ π•œ E + rw [← polar_closure (π•œ := π•œ) (s := ball (0 : E) r), closure_ball (0 : E) hr.ne', + polar_closedBall hr] /-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms of all elements of the polar `polar π•œ s` are bounded by a constant. -/ From a4e7598690630b4fbb681a28300ff62e3510de6c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 25 Apr 2026 16:19:28 +0800 Subject: [PATCH 2/2] Update Mathlib/Analysis/Normed/Module/Dual.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Normed/Module/Dual.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean index 063417bde36ea3..5cd5b6ac918616 100644 --- a/Mathlib/Analysis/Normed/Module/Dual.lean +++ b/Mathlib/Analysis/Normed/Module/Dual.lean @@ -118,8 +118,7 @@ theorem polar_closedBall {π•œ E : Type*} [RCLike π•œ] [NormedAddCommGroup E] [ theorem polar_ball {π•œ E : Type*} [RCLike π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] {r : ℝ} (hr : 0 < r) : StrongDual.polar π•œ (ball (0 : E) r) = closedBall (0 : StrongDual π•œ E) r⁻¹ := by letI : NormedSpace ℝ E := .restrictScalars ℝ π•œ E - rw [← polar_closure (π•œ := π•œ) (s := ball (0 : E) r), closure_ball (0 : E) hr.ne', - polar_closedBall hr] + rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure] /-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms of all elements of the polar `polar π•œ s` are bounded by a constant. -/