mathlib documentation

analysis.locally_convex.polar

Polar set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

Main statements #

linear_map.polar_eq_Inter: The polar as an intersection.
linear_map.subset_bipolar: The polar is a subset of the bipolar.
linear_map.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 linear_map.polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) :

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 : E), x ∈ s → ‖⇑(⇑B x) y‖ ≤ 1}

theorem linear_map.polar_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) (y : F) :

y ∈ B.polar s ↔ ∀ (x : E), x ∈ s → ‖⇑(⇑B x) y‖ ≤ 1

theorem linear_map.polar_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) (y : F) (hy : y ∈ B.polar s) (x : E) (H : x ∈ s) :

‖⇑(⇑B x) y‖ ≤ 1

@[simp]

theorem linear_map.zero_mem_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) :

0 ∈ B.polar s

theorem linear_map.polar_eq_Inter {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s : set E} :

B.polar s = ⋂ (x : E) (H : x ∈ s), {y : F | ‖⇑(⇑B x) y‖ ≤ 1}

theorem linear_map.polar_gc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

galois_connection (⇑order_dual.to_dual ∘ B.polar) (B.flip.polar ∘ ⇑order_dual.of_dual)

The map B.polar : set E → set F forms an order-reversing Galois connection with B.flip.polar : set F → set E. We use order_dual.to_dual and order_dual.of_dual to express that polar is order-reversing.

@[simp]

theorem linear_map.polar_Union {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid 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 linear_map.polar_union {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s t : set E} :

B.polar (s ∪ t) = B.polar s ∩ B.polar t

theorem linear_map.polar_antitone {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

antitone B.polar

@[simp]

theorem linear_map.polar_empty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

B.polar ∅ = set.univ

@[simp]

theorem linear_map.polar_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

B.polar {0} = set.univ

theorem linear_map.subset_bipolar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) :

s ⊆ B.flip.polar (B.polar s)

@[simp]

theorem linear_map.tripolar_eq_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) :

B.polar (B.flip.polar (B.polar s)) = B.polar s

theorem linear_map.polar_weak_closed {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : set E) :

is_closed (B.polar s)

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

theorem linear_map.polar_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [nontrivially_normed_field 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (h : B.separating_right) :

B.polar set.univ = {0}