[Merged by Bors] - feat(analysis/locally_convex): polar sets for dualities

src/analysis/locally_convex/polar.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2022 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Kalle Kytölä
+-/
+
+import analysis.normed.normed_field
+import analysis.convex.basic
+import linear_algebra.sesquilinear_form
+
+/-!
+# 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
+
+* `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.
+
+## References
+
+* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
+
+## Tags
+
+polar
+-/
+
+
+variables {𝕜 E F : Type*}
+
+namespace linear_map
+
+section normed_ring
+
+variables [normed_comm_ring 𝕜] [add_comm_monoid E] [add_comm_monoid F]
+variables [module 𝕜 E] [module 𝕜 F]
+variables (B : E →ₗ[𝕜] 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`.-/
+def polar (s : set E) : set F :=
+  {y : F | ∀ x ∈ s, ∥B x y∥ ≤ 1 }
+
+lemma polar_mem_iff (s : set E) (y : F) :
+  y ∈ B.polar s ↔ ∀ x ∈ s, ∥B x y∥ ≤ 1 := iff.rfl
+
+lemma polar_mem (s : set E) (y : F) (hy : y ∈ B.polar s) :
+  ∀ x ∈ s, ∥B x y∥ ≤ 1 := hy
+
+@[simp] lemma zero_mem_polar (s : set E) :
+  (0 : F) ∈ B.polar s :=
+λ _ _, by simp only [map_zero, norm_zero, zero_le_one]
+
+lemma polar_eq_Inter {s : set E} :
+  B.polar s = ⋂ x ∈ s, {y : F | ∥B x y∥ ≤ 1} :=
+by { ext, simp only [polar_mem_iff, set.mem_Inter, set.mem_set_of_eq] }
+
+/-- 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. -/
+lemma polar_gc : galois_connection (order_dual.to_dual ∘ B.polar)
+  (B.flip.polar ∘ order_dual.of_dual) :=
+λ s t, ⟨λ h _ hx _ hy, h hy _ hx, λ h _ hx _ hy, h hy _ hx⟩
+
+@[simp] lemma polar_Union {ι} {s : ι → set E} : B.polar (⋃ i, s i) = ⋂ i, B.polar (s i) :=
+B.polar_gc.l_supr
+
+@[simp] lemma polar_union {s t : set E} : B.polar (s ∪ t) = B.polar s ∩ B.polar t :=
+B.polar_gc.l_sup
+
+lemma polar_antitone : antitone (B.polar : set E → set F) := B.polar_gc.monotone_l
+
+@[simp] lemma polar_empty : B.polar ∅ = set.univ := B.polar_gc.l_bot
+
+@[simp] lemma polar_zero : B.polar ({0} : set E) = set.univ :=
+begin
+  refine set.eq_univ_iff_forall.mpr (λ y x hx, _),
+  rw [set.mem_singleton_iff.mp hx, map_zero, linear_map.zero_apply, norm_zero],
+  exact zero_le_one,
+end
+
+lemma subset_bipolar (s : set E) : s ⊆ B.flip.polar (B.polar s) :=
+λ x hx y hy, by { rw B.flip_apply, exact hy x hx }
+
+@[simp] lemma tripolar_eq_polar (s : set E) : B.polar (B.flip.polar (B.polar s)) = B.polar s :=
+begin
+  refine (B.polar_antitone (B.subset_bipolar s)).antisymm _,
+  convert subset_bipolar B.flip (B.polar s),
+  exact B.flip_flip.symm,
+end
+
+end normed_ring
+
+section nondiscrete_normed_field
+
+variables [nondiscrete_normed_field 𝕜] [add_comm_monoid E] [add_comm_monoid F]
+variables [module 𝕜 E] [module 𝕜 F]
+variables (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
+
+lemma polar_univ (h : separating_right B) :
+  B.polar set.univ = {(0 : F)} :=
+begin
+  rw set.eq_singleton_iff_unique_mem,
+  refine ⟨by simp only [zero_mem_polar], λ y hy, h _ (λ x, _)⟩,
+  refine norm_le_zero_iff.mp (le_of_forall_le_of_dense $ λ ε hε, _),
+  rcases normed_field.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩,
+  calc ∥B x y∥ = ∥c∥ * ∥B (c⁻¹ • x) y∥ :
+    by rw [B.map_smul, linear_map.smul_apply, algebra.id.smul_eq_mul, norm_mul, norm_inv,
+      mul_inv_cancel_left₀ hc.ne']
+  ... ≤ ε * 1 : mul_le_mul hcε.le (hy _ trivial) (norm_nonneg _) hε.le
+  ... = ε : mul_one _
+end
+
+end nondiscrete_normed_field
+
+end linear_map

src/analysis/normed_space/dual.lean

@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 import analysis.normed_space.hahn_banach
 import analysis.normed_space.is_R_or_C
+import analysis.locally_convex.polar
 
 /-!
 # The topological dual of a normed space
@@ -72,6 +73,11 @@ by { rw inclusion_in_double_dual_norm_eq, exact continuous_linear_map.norm_id_le
 lemma double_dual_bound (x : E) : ∥(inclusion_in_double_dual 𝕜 E) x∥ ≤ ∥x∥ :=
 by simpa using continuous_linear_map.le_of_op_norm_le _ (inclusion_in_double_dual_norm_le 𝕜 E) x
 
+/-- The dual pairing as a bilinear form. -/
+def dual_pairing : (dual 𝕜 E) →ₗ[𝕜] E →ₗ[𝕜] 𝕜 := continuous_linear_map.coe_lm 𝕜
+
+@[simp] lemma dual_pairing_apply {v : dual 𝕜 E} {x : E} : dual_pairing 𝕜 E v x = v x := rfl
+
 end general
 
 section bidual_isometry
@@ -122,8 +128,6 @@ def inclusion_in_double_dual_li : E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)) :=
 
 end bidual_isometry
 
-end normed_space
-
 section polar_sets
 
 open metric set normed_space
@@ -132,23 +136,17 @@ open metric set normed_space
 `polar 𝕜 s` is the subset of `dual 𝕜 E` consisting of those functionals which
 evaluate to something of norm at most one at all points `z ∈ s`. -/
 def polar (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E] (s : set E) : set (dual 𝕜 E) :=
-{x' : dual 𝕜 E | ∀ z ∈ s, ∥ x' z ∥ ≤ 1}
+  {E : Type*} [normed_group E] [normed_space 𝕜 E] : set E → set (dual 𝕜 E) :=
+(dual_pairing 𝕜 E).flip.polar
 
 variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
 variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
 
-@[simp] lemma zero_mem_polar (s : set E) :
-  (0 : dual 𝕜 E) ∈ polar 𝕜 s :=
-λ _ _, by simp only [zero_le_one, continuous_linear_map.zero_apply, norm_zero]
-
-lemma polar_eq_Inter (s : set E) :
-  polar 𝕜 s = ⋂ z ∈ s, {x' : dual 𝕜 E | ∥x' z∥ ≤ 1} :=
-by simp only [polar, set_of_forall]
+lemma mem_polar_iff {x' : dual 𝕜 E} (s : set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ∥x' z∥ ≤ 1 := iff.rfl
 
 @[simp] lemma polar_univ : polar 𝕜 (univ : set E) = {(0 : dual 𝕜 E)} :=
 begin
-  refine eq_singleton_iff_unique_mem.2 ⟨zero_mem_polar _ _, λ x' hx', _⟩,
+  refine eq_singleton_iff_unique_mem.2 ⟨linear_map.zero_mem_polar _ _, λ x' hx', _⟩,
   ext x,
   refine norm_le_zero_iff.1 (le_of_forall_le_of_dense $ λ ε hε, _),
   rcases normed_field.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩,
@@ -161,41 +159,16 @@ end
 
 lemma is_closed_polar (s : set E) : is_closed (polar 𝕜 s) :=
 begin
-  simp only [polar_eq_Inter, ← continuous_linear_map.apply_apply _ (_ : dual 𝕜 E)],
+  dunfold normed_space.polar,
+  simp only [linear_map.polar_eq_Inter, linear_map.flip_apply],
   refine is_closed_bInter (λ z hz, _),
   exact is_closed_Iic.preimage (continuous_linear_map.apply 𝕜 𝕜 z).continuous.norm
 end
 
-variable (E)
-
-/-- `polar 𝕜 : set E → set (normed_space.dual 𝕜 E)` forms an order-reversing Galois connection with
-a similarly defined map `set (normed_space.dual 𝕜 E) → set E`. We use `order_dual.to_dual` and
-`order_dual.of_dual` to express that `polar` is order-reversing. Instead of defining the dual
-operation `unpolar s := {x : E | ∀ x' ∈ s, ∥x' x∥ ≤ 1}` we apply `polar 𝕜` again, then pull the set
-from the double dual space to the original space using `normed_space.inclusion_in_double_dual`. -/
-lemma polar_gc :
-  galois_connection (order_dual.to_dual ∘ polar 𝕜)
-    (λ s, inclusion_in_double_dual 𝕜 E ⁻¹' (polar 𝕜 $ order_dual.of_dual s)) :=
-λ s t, ⟨λ H x hx x' hx', H hx' x hx, λ H x' hx' x hx, H hx x' hx'⟩
-
-variable {E}
-
-@[simp] lemma polar_Union {ι} (s : ι → set E) : polar 𝕜 (⋃ i, s i) = ⋂ i, polar 𝕜 (s i) :=
-(polar_gc 𝕜 E).l_supr
-
-@[simp] lemma polar_union (s t : set E) : polar 𝕜 (s ∪ t) = polar 𝕜 s ∩ polar 𝕜 t :=
-(polar_gc 𝕜 E).l_sup
-
-lemma polar_antitone : antitone (polar 𝕜 : set E → set (dual 𝕜 E)) := (polar_gc 𝕜 E).monotone_l
-
-@[simp] lemma polar_empty : polar 𝕜 (∅ : set E) = univ := (polar_gc 𝕜 E).l_bot
-
-@[simp] lemma polar_zero : polar 𝕜 ({0} : set E) = univ :=
-eq_univ_of_forall $ λ x', forall_eq.2 $ by { rw [map_zero, norm_zero], exact zero_le_one }
-
 @[simp] lemma polar_closure (s : set E) : polar 𝕜 (closure s) = polar 𝕜 s :=
-(polar_antitone 𝕜 subset_closure).antisymm $ (polar_gc 𝕜 E).l_le $
-  closure_minimal ((polar_gc 𝕜 E).le_u_l s) $
+((dual_pairing 𝕜 E).flip.polar_antitone subset_closure).antisymm $
+  (dual_pairing 𝕜 E).flip.polar_gc.l_le $
+  closure_minimal ((dual_pairing 𝕜 E).flip.polar_gc.le_u_l s) $
   (is_closed_polar _ _).preimage (inclusion_in_double_dual 𝕜 E).continuous
 
 variables {𝕜}
@@ -205,7 +178,8 @@ small scalar multiple of `x'` is in `polar 𝕜 s`. -/
 lemma smul_mem_polar {s : set E} {x' : dual 𝕜 E} {c : 𝕜}
   (hc : ∀ z, z ∈ s → ∥ x' z ∥ ≤ ∥c∥) : c⁻¹ • x' ∈ polar 𝕜 s :=
 begin
-  by_cases c_zero : c = 0, { simp [c_zero] },
+  by_cases c_zero : c = 0, { simp only [c_zero, inv_zero, zero_smul],
+    exact (dual_pairing 𝕜 E).flip.zero_mem_polar _ },
   have eq : ∀ z, ∥ c⁻¹ • (x' z) ∥ = ∥ c⁻¹ ∥ * ∥ x' z ∥ := λ z, norm_smul c⁻¹ _,
   have le : ∀ z, z ∈ s → ∥ c⁻¹ • (x' z) ∥ ≤ ∥ c⁻¹ ∥ * ∥ c ∥,
   { intros z hzs,
@@ -221,6 +195,7 @@ lemma polar_ball_subset_closed_ball_div {c : 𝕜} (hc : 1 < ∥c∥) {r : ℝ}
   polar 𝕜 (ball (0 : E) r) ⊆ closed_ball (0 : dual 𝕜 E) (∥c∥ / r) :=
 begin
   intros x' hx',
+  rw mem_polar_iff at hx',
   simp only [polar, mem_set_of_eq, mem_closed_ball_zero_iff, mem_ball_zero_iff] at *,
   have hcr : 0 < ∥c∥ / r, from div_pos (zero_lt_one.trans hc) hr,
   refine continuous_linear_map.op_norm_le_of_shell hr hcr.le hc (λ x h₁ h₂, _),
@@ -261,8 +236,10 @@ begin
   obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ∥a∥ := normed_field.exists_one_lt_norm 𝕜,
   obtain ⟨r, r_pos, r_ball⟩ : ∃ (r : ℝ) (hr : 0 < r), ball 0 r ⊆ s :=
     metric.mem_nhds_iff.1 s_nhd,
-  exact bounded_closed_ball.mono ((polar_antitone 𝕜 r_ball).trans $
+  exact bounded_closed_ball.mono (((dual_pairing 𝕜 E).flip.polar_antitone r_ball).trans $
     polar_ball_subset_closed_ball_div ha r_pos)
 end
 
 end polar_sets
+
+end normed_space

src/analysis/normed_space/weak_dual.lean

@@ -72,7 +72,6 @@ noncomputable theory
 open filter
 open_locale topological_space
 
-section weak_star_topology_for_duals_of_normed_spaces
 /-!
 ### Weak star topology on duals of normed spaces
 In this section, we prove properties about the weak-* topology on duals of normed spaces.
@@ -149,36 +148,4 @@ begin
   exact set.preimage_set_of_eq,
 end
 
-variables (𝕜)
-
-/-- The polar set `polar 𝕜 s` of `s : set E` seen as a subset of the dual of `E` with the
-weak-star topology is `weak_dual.polar 𝕜 s`. -/
-def polar (s : set E) : set (weak_dual 𝕜 E) := to_normed_dual ⁻¹' (polar 𝕜 s)
-
 end weak_dual
-
-end weak_star_topology_for_duals_of_normed_spaces
-
-section polar_sets_in_weak_dual
-
-open metric set normed_space
-
-variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
-
-/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
-is used, i.e., when `polar 𝕜 s` is interpreted as a subset of `weak_dual 𝕜 E`. -/
-lemma weak_dual.is_closed_polar (s : set E) : is_closed (weak_dual.polar 𝕜 s) :=
-begin
-  rw [weak_dual.polar, polar_eq_Inter, preimage_Inter₂],
-  apply is_closed_bInter,
-  intros z hz,
-  rw set.preimage_set_of_eq,
-  have eq : {x' : weak_dual 𝕜 E | ∥weak_dual.to_normed_dual x' z∥ ≤ 1}
-    = (λ (x' : weak_dual 𝕜 E), ∥x' z∥)⁻¹' (Iic 1) := by refl,
-  rw eq,
-  refine is_closed.preimage _ (is_closed_Iic),
-  apply continuous.comp continuous_norm (eval_continuous (top_dual_pairing _ _) z),
-end
-
-end polar_sets_in_weak_dual