Polar sets in the strong dual of a normed space

In this file we study polar sets in the strong dual StrongDual of a normed space.

Main definitions

• polar 𝕜 s is the subset of StrongDual 𝕜 E consisting of those functionals x' for which ‖x' z‖ ≤ 1 for every z ∈ s.

References

• [Conway, John B., A course in functional analysis][conway1990]

Tags

strong dual, polar

theorem NormedSpace.isClosed_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : IsClosed (StrongDual.polar 𝕜 s)

@[simp]

theorem NormedSpace.polar_closure (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : StrongDual.polar 𝕜 (closure s) = StrongDual.polar 𝕜 s

theorem NormedSpace.smul_mem_polar {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x' : StrongDual 𝕜 E} {c : 𝕜} (hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖) : c⁻¹ • x' ∈ StrongDual.polar 𝕜 s

If x' is a StrongDual 𝕜 E element such that the norms ‖x' z‖ are bounded for z ∈ s, then a small scalar multiple of x' is in polar 𝕜 s.

theorem NormedSpace.polar_ball_subset_closedBall_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {r : ℝ} (hr : 0 < r) : StrongDual.polar 𝕜 (Metric.ball 0 r) ⊆ Metric.closedBall 0 (‖c‖ / r)

theorem NormedSpace.closedBall_inv_subset_polar_closedBall (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : Metric.closedBall 0 r⁻¹ ⊆ StrongDual.polar 𝕜 (Metric.closedBall 0 r)

theorem NormedSpace.polar_closedBall {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : StrongDual.polar 𝕜 (Metric.closedBall 0 r) = Metric.closedBall 0 r⁻¹

The polar of closed ball in a normed space E is the closed ball of the dual with inverse radius.

theorem NormedSpace.polar_ball {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : StrongDual.polar 𝕜 (Metric.ball 0 r) = Metric.closedBall 0 r⁻¹

theorem NormedSpace.isBounded_polar_of_mem_nhds_zero (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (s_nhds : s ∈ nhds 0) : Bornology.IsBounded (StrongDual.polar 𝕜 s)

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.

theorem NormedSpace.sInter_polar_eq_closedBall {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : ⋂₀ (StrongDual.polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ Metric.closedBall 0 r⁻¹}) = Metric.closedBall 0 r

theorem LinearMap.polar_AbsConvex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E) : AbsConvex 𝕜 (B.polar s)

@[deprecated SeparatingDual.eq_zero_of_forall_dual_eq_zero (since := "2026-03-18")]

theorem NormedSpace.eq_zero_of_forall_dual_eq_zero (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : ∀ (f : StrongDual 𝕜 E), f x = 0) : x = 0

@[deprecated SeparatingDual.eq_zero_iff_forall_dual_eq_zero (since := "2026-03-18")]

theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : x = 0 ↔ ∀ (g : StrongDual 𝕜 E), g x = 0

@[deprecated SeparatingDual.eq_iff_forall_dual_eq (since := "2026-03-18")]

theorem NormedSpace.eq_iff_forall_dual_eq (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x y : E} : x = y ↔ ∀ (g : StrongDual 𝕜 E), g x = g y