Polar set

In this file we define the polar set. There are different notions of the polar, we will define the absolute polar. The advantage over the real polar is that we can define the absolute polar for any bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, where 𝕜 is a normed commutative ring and E and F are modules over 𝕜.

Main definitions

• LinearMap.polar: The polar of a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜.

Main statements

• LinearMap.polar_eq_iInter: The polar as an intersection.
• LinearMap.subset_bipolar: The polar is a subset of the bipolar.
• LinearMap.polar_weak_closed: The polar is closed in the weak topology induced by B.flip.

References

• H. H. Schaefer, Topological Vector Spaces

Tags

polar

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

The (absolute) polar of s : Set E is given by the set of all y : F such that ‖B x y‖ ≤ 1 for all x ∈ s.

Equations

• B.polar s = {y : F | ∀ x ∈ s, ‖(B x) y‖ ≤ 1}

theorem LinearMap.polar_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) (y : F) : y ∈ B.polar s ↔ ∀ x ∈ s, ‖(B x) y‖ ≤ 1

theorem LinearMap.polar_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) (y : F) (hy : y ∈ B.polar s) (x : E) : x ∈ s → ‖(B x) y‖ ≤ 1

theorem LinearMap.polar_eq_biInter_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : B.polar s = ⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1

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

@[simp]

theorem LinearMap.zero_mem_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : 0 ∈ B.polar s

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

theorem LinearMap.polar_eq_iInter {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s : Set E} : B.polar s = ⋂ x ∈ s, {y : F | ‖(B x) y‖ ≤ 1}

theorem LinearMap.polar_gc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : GaloisConnection (⇑OrderDual.toDual ∘ B.polar) (B.flip.polar ∘ ⇑OrderDual.ofDual)

The map B.polar : Set E → Set F forms an order-reversing Galois connection with B.flip.polar : Set F → Set E. We use OrderDual.toDual and OrderDual.ofDual to express that polar is order-reversing.

@[simp]

theorem LinearMap.polar_iUnion {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {ι : Sort u_4} {s : ι → Set E} : B.polar (⋃ (i : ι), s i) = ⋂ (i : ι), B.polar (s i)

@[simp]

theorem LinearMap.polar_union {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s t : Set E} : B.polar (s ∪ t) = B.polar s ∩ B.polar t

theorem LinearMap.polar_antitone {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Antitone B.polar

@[simp]

theorem LinearMap.polar_empty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : B.polar ∅ = Set.univ

@[simp]

theorem LinearMap.polar_singleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {a : E} : B.polar {a} = {y : F | ‖(B a) y‖ ≤ 1}

theorem LinearMap.mem_polar_singleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {x : E} (y : F) : y ∈ B.polar {x} ↔ ‖(B x) y‖ ≤ 1

theorem LinearMap.polar_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : B.polar {0} = Set.univ

theorem LinearMap.subset_bipolar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : s ⊆ B.flip.polar (B.polar s)

@[simp]

theorem LinearMap.tripolar_eq_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : B.polar (B.flip.polar (B.polar s)) = B.polar s

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

The polar set is closed in the weak topology induced by B.flip.

theorem LinearMap.sInter_polar_finite_subset_eq_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) : ⋂₀ (B.polar '' {F : Set E | F.Finite ∧ F ⊆ s}) = B.polar s

theorem LinearMap.polar_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (h : B.SeparatingRight) : B.polar Set.univ = {0}

theorem LinearMap.polar_subMulAction {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {S : Type u_4} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : B.polar ↑m = {y : F | ∀ x ∈ m, (B x) y = 0}

def LinearMap.polarSubmodule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {S : Type u_4} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : Submodule 𝕜 F

The polar of a set closed under scalar multiplication as a submodule

Equations

• B.polarSubmodule m = (⨅ x ∈ m, LinearMap.ker (B x)).copy (B.polar ↑m) ⋯

theorem StrongDual.dualPairing_separatingLeft (R : Type u_4) (M : Type u_5) [SeminormedCommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] : (topDualPairing R M).SeparatingLeft

@[deprecated StrongDual.dualPairing_separatingLeft (since := "2025-08-3")]

theorem StrongDual.NormedSpace.dualPairing_separatingLeft (R : Type u_4) (M : Type u_5) [SeminormedCommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] : (topDualPairing R M).SeparatingLeft

Alias of StrongDual.dualPairing_separatingLeft.

def StrongDual.polar (R : Type u_4) [NormedCommRing R] {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : Set M → Set (StrongDual R M)

Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Equations

• StrongDual.polar R = (topDualPairing R M).flip.polar

@[deprecated StrongDual.polar (since := "2025-08-3")]

def NormedSpace.polar (R : Type u_4) [NormedCommRing R] {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : Set M → Set (StrongDual R M)

Alias of StrongDual.polar.

---

Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Equations

• NormedSpace.polar = StrongDual.polar

def StrongDual.polarSubmodule (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] {S : Type u_6} [SetLike S M] [SMulMemClass S 𝕜 M] (m : S) : Submodule 𝕜 (StrongDual 𝕜 M)

Given a subset s in a monoid M (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of StrongDual 𝕜 M consisting of those functionals which evaluate to zero at all points z ∈ s.

Equations

• StrongDual.polarSubmodule 𝕜 m = (topDualPairing 𝕜 M).flip.polarSubmodule m

@[deprecated StrongDual.polarSubmodule (since := "2025-08-3")]

def NormedSpace.polarSubmodule (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] {S : Type u_6} [SetLike S M] [SMulMemClass S 𝕜 M] (m : S) : Submodule 𝕜 (StrongDual 𝕜 M)

Alias of StrongDual.polarSubmodule.

---

Given a subset s in a monoid M (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of StrongDual 𝕜 M consisting of those functionals which evaluate to zero at all points z ∈ s.

Equations

• NormedSpace.polarSubmodule = StrongDual.polarSubmodule

theorem StrongDual.polarSubmodule_eq_polar (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (m : SubMulAction 𝕜 E) : ↑(polarSubmodule 𝕜 m) = polar 𝕜 ↑m

@[deprecated StrongDual.polarSubmodule_eq_polar (since := "2025-08-3")]

theorem NormedSpace.polarSubmodule_eq_polar (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (m : SubMulAction 𝕜 E) : ↑(StrongDual.polarSubmodule 𝕜 m) = StrongDual.polar 𝕜 ↑m

Alias of StrongDual.polarSubmodule_eq_polar.

theorem StrongDual.mem_polar_iff (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

@[deprecated StrongDual.mem_polar_iff (since := "2025-08-3")]

theorem NormedSpace.mem_polar_iff (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E) : x' ∈ StrongDual.polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

Alias of StrongDual.mem_polar_iff.

theorem StrongDual.polarSubmodule_eq_setOf (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_6} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : ↑(polarSubmodule 𝕜 m) = {y : StrongDual 𝕜 E | ∀ x ∈ m, y x = 0}

@[deprecated StrongDual.polarSubmodule_eq_setOf (since := "2025-08-3")]

theorem NormedSpace.polarSubmodule_eq_setOf (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_6} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : ↑(StrongDual.polarSubmodule 𝕜 m) = {y : StrongDual 𝕜 E | ∀ x ∈ m, y x = 0}

Alias of StrongDual.polarSubmodule_eq_setOf.

theorem StrongDual.mem_polarSubmodule (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_6} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : StrongDual 𝕜 E) : y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

@[deprecated StrongDual.mem_polarSubmodule (since := "2025-08-3")]

theorem NormedSpace.mem_polarSubmodule (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_6} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : StrongDual 𝕜 E) : y ∈ StrongDual.polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Alias of StrongDual.mem_polarSubmodule.

@[simp]

theorem StrongDual.zero_mem_polar (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : 0 ∈ polar 𝕜 s

@[deprecated StrongDual.zero_mem_polar (since := "2025-08-3")]

theorem NormedSpace.zero_mem_polar (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : 0 ∈ StrongDual.polar 𝕜 s

Alias of StrongDual.zero_mem_polar.

theorem StrongDual.polar_nonempty (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : (polar 𝕜 s).Nonempty

@[deprecated StrongDual.polar_nonempty (since := "2025-08-3")]

theorem NormedSpace.polar_nonempty (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : (StrongDual.polar 𝕜 s).Nonempty

Alias of StrongDual.polar_nonempty.

@[simp]

theorem StrongDual.polar_empty (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 ∅ = Set.univ

@[deprecated StrongDual.polar_empty (since := "2025-08-3")]

theorem NormedSpace.polar_empty (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 ∅ = Set.univ

Alias of StrongDual.polar_empty.

@[simp]

theorem StrongDual.polar_singleton (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} : polar 𝕜 {a} = {x : StrongDual 𝕜 E | ‖x a‖ ≤ 1}

@[deprecated StrongDual.polar_singleton (since := "2025-08-3")]

theorem NormedSpace.polar_singleton (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} : StrongDual.polar 𝕜 {a} = {x : StrongDual 𝕜 E | ‖x a‖ ≤ 1}

Alias of StrongDual.polar_singleton.

theorem StrongDual.mem_polar_singleton (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} (y : StrongDual 𝕜 E) : y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

@[deprecated StrongDual.mem_polar_singleton (since := "2025-08-3")]

theorem NormedSpace.mem_polar_singleton (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} (y : StrongDual 𝕜 E) : y ∈ StrongDual.polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

Alias of StrongDual.mem_polar_singleton.

theorem StrongDual.polar_zero (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 {0} = Set.univ

@[deprecated StrongDual.polar_zero (since := "2025-08-3")]

theorem NormedSpace.polar_zero (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 {0} = Set.univ

Alias of StrongDual.polar_zero.

@[simp]

theorem StrongDual.polar_univ (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 Set.univ = {0}

@[deprecated StrongDual.polar_univ (since := "2025-08-3")]

theorem NormedSpace.polar_univ (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 Set.univ = {0}

Alias of StrongDual.polar_univ.