feature(Analysis/Normed/Module/Dual): Add a few polar lemmas (#16426)

Adds a few trivial polar lemmas. CC: @urkud Co-authored-by: Christopher Hoskin <[email protected]>
leanprover-community · Sep 23, 2024 · 8192b1a · 8192b1a
1 parent b978dc4
commit 8192b1a
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/Mathlib/Analysis/LocallyConvex/Polar.lean b/Mathlib/Analysis/LocallyConvex/Polar.lean
@@ -64,6 +64,10 @@ theorem polar_mem (s : Set E) (y : F) (hy : y ∈ B.polar s) : ∀ x ∈ s, ‖B
 theorem zero_mem_polar (s : Set E) : (0 : F) ∈ B.polar s := fun _ _ => by
   simp only [map_zero, norm_zero, zero_le_one]
 
+theorem polar_nonempty (s : Set E) : Set.Nonempty (B.polar s) := by
+  use 0
+  exact zero_mem_polar B s
+
 theorem polar_eq_iInter {s : Set E} : B.polar s = ⋂ x ∈ s, { y : F | ‖B x y‖ ≤ 1 } := by
   ext
   simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]

diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean
@@ -159,6 +159,13 @@ variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 theorem mem_polar_iff {x' : Dual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1 :=
   Iff.rfl
 
+@[simp]
+theorem zero_mem_polar (s : Set E) : (0 : Dual 𝕜 E) ∈ polar 𝕜 s :=
+  LinearMap.zero_mem_polar _ s
+
+theorem polar_nonempty (s : Set E) : Set.Nonempty (polar 𝕜 s) :=
+  LinearMap.polar_nonempty _ _
+
 @[simp]
 theorem polar_univ : polar 𝕜 (univ : Set E) = {(0 : Dual 𝕜 E)} :=
   (dualPairing 𝕜 E).flip.polar_univ
@@ -256,13 +263,20 @@ theorem isBounded_polar_of_mem_nhds_zero {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)
     (((dualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
       polar_ball_subset_closedBall_div ha r_pos)
 
+@[simp]
+theorem polar_empty : polar 𝕜 (∅ : Set E) = Set.univ :=
+  LinearMap.polar_empty _
+
 @[simp]
 theorem polar_singleton {a : E} : polar 𝕜 {a} = { x | ‖x a‖ ≤ 1 } := by
   simp only [polar, LinearMap.polar_singleton, LinearMap.flip_apply, dualPairing_apply]
 
 theorem mem_polar_singleton {a : E} (y : Dual 𝕜 E) : y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1 := by
   simp only [polar_singleton, mem_setOf_eq]
 
+theorem polar_zero : polar 𝕜 ({0} : Set E) = Set.univ :=
+  LinearMap.polar_zero _
+
 theorem sInter_polar_eq_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
     {r : ℝ} (hr : 0 < r) :
     ⋂₀ (polar 𝕜 '' { F | F.Finite ∧ F ⊆ closedBall (0 : E) r⁻¹ }) = closedBall 0 r := by