From 8192b1aeed705058e2c7369599897104813e0ba0 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 23 Sep 2024 18:06:28 +0000 Subject: [PATCH] feature(Analysis/Normed/Module/Dual): Add a few polar lemmas (#16426) Adds a few trivial polar lemmas. CC: @urkud Co-authored-by: Christopher Hoskin --- Mathlib/Analysis/LocallyConvex/Polar.lean | 4 ++++ Mathlib/Analysis/Normed/Module/Dual.lean | 14 ++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/Mathlib/Analysis/LocallyConvex/Polar.lean b/Mathlib/Analysis/LocallyConvex/Polar.lean index c640565fce415..dba80d95bd857 100644 --- 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 index 91bfbe1dc1f82..2892b13b82927 100644 --- 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,6 +263,10 @@ 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] @@ -263,6 +274,9 @@ theorem polar_singleton {a : E} : polar 𝕜 {a} = { x | ‖x a‖ ≤ 1 } := by 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