feat(analysis/normed_space/weak_dual): add polar sets in preparation …

…for Banach-Alaoglu theorem (#9836)

The first of two parts to add the Banach-Alaoglu theorem about the compactness of the closed unit ball (and more generally polar sets of neighborhoods of the origin) of the dual of a normed space in the weak-star topology.

This first half is about polar sets (for a set `s` in a normed space `E`, the `polar s` is the subset of `weak_dual _ E` consisting of the functionals that evaluate to something of norm at most one at all elements of `s`).



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/normed_space/dual.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import analysis.normed_space.hahn_banach
+import analysis.normed_space.is_R_or_C
 
 /-!
 # The topological dual of a normed space
@@ -19,6 +20,13 @@ isometric embedding, `E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E))`.
 Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the
 theory for `semi_normed_space` and we specialize to `normed_space` when needed.
 
+## Main definitions
+
+* `inclusion_in_double_dual` and `inclusion_in_double_dual_li` are the inclusion of a normed space
+  in its double dual, considered as a bounded linear map and as a linear isometry, respectively.
+* `polar 𝕜 s` is the subset of `dual 𝕜 E` consisting of those functionals `x'` for which
+  `∥x' z∥ ≤ 1` for every `z ∈ s`.
+
 ## Tags
 
 dual
@@ -115,3 +123,91 @@ def inclusion_in_double_dual_li : E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)) :=
 end bidual_isometry
 
 end normed_space
+
+section polar_sets
+
+open metric set normed_space
+
+/-- Given a subset `s` in a normed space `E` (over a field `𝕜`), the polar
+`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}
+
+open metric set normed_space
+open_locale topological_space
+
+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 { ext, simp only [polar, mem_bInter_iff, mem_set_of_eq], }
+
+@[simp] lemma polar_empty : polar 𝕜 (∅ : set E) = univ :=
+by simp only [polar, forall_false_left, mem_empty_eq, forall_const, set_of_true]
+
+variables {𝕜}
+
+/-- If `x'` is a dual element such that the norms `∥x' z∥` are bounded for `z ∈ s`, then a
+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] },
+  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,
+    rw eq z,
+    apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _), },
+  have cancel : ∥ c⁻¹ ∥ * ∥ c ∥ = 1,
+  by simp only [c_zero, norm_eq_zero, ne.def, not_false_iff,
+                inv_mul_cancel, normed_field.norm_inv],
+  rwa cancel at le,
+end
+
+variables (𝕜)
+
+/-- The `polar` of closed ball in a normed space `E` is the closed ball of the dual with
+inverse radius. -/
+lemma polar_closed_ball
+  {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {r : ℝ} (hr : 0 < r) :
+  polar 𝕜 (closed_ball (0 : E) r) = closed_ball (0 : dual 𝕜 E) (1/r) :=
+begin
+  ext x',
+  simp only [mem_closed_ball, mem_set_of_eq, dist_zero_right],
+  split,
+  { intros h,
+    apply continuous_linear_map.op_norm_le_of_ball hr (one_div_nonneg.mpr hr.le),
+    { exact λ z hz, linear_map.bound_of_ball_bound hr 1 x'.to_linear_map h z, },
+    { exact ring_hom_isometric.ids, }, },
+  { intros h z hz,
+    simp only [mem_closed_ball, dist_zero_right] at hz,
+    have key := (continuous_linear_map.le_op_norm x' z).trans
+      (mul_le_mul h hz (norm_nonneg _) (one_div_nonneg.mpr hr.le)),
+    rwa [one_div_mul_cancel hr.ne.symm] at key, },
+end
+
+/-- 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. -/
+lemma polar_bounded_of_nhds_zero {s : set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
+  ∃ (c : ℝ), ∀ x' ∈ polar 𝕜 s, ∥x'∥ ≤ c :=
+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,
+  refine ⟨∥a∥ / r, λ x' hx', _⟩,
+  have I : 0 ≤ ∥a∥ / r := div_nonneg (norm_nonneg _) r_pos.le,
+  refine continuous_linear_map.op_norm_le_of_shell r_pos I ha (λ x hx h'x, _),
+  have x_mem : x ∈ ball (0 : E) r, by simpa only [mem_ball_zero_iff] using h'x,
+  calc ∥x' x∥ ≤ 1 : hx' x (r_ball x_mem)
+  ... = (∥a∥ / r) * (r / ∥a∥) : by field_simp [r_pos.ne', (zero_lt_one.trans ha).ne']
+  ... ≤ (∥a∥ / r) * ∥x∥ : mul_le_mul_of_nonneg_left hx I
+end
+
+end polar_sets

src/analysis/normed_space/weak_dual.lean

@@ -137,4 +137,48 @@ end
 
 end normed_space.dual
 
+namespace weak_dual
+
+lemma to_normed_dual.preimage_closed_unit_ball :
+  (to_normed_dual ⁻¹' metric.closed_ball (0 : dual 𝕜 E) 1) =
+    {x' : weak_dual 𝕜 E | ∥ x'.to_normed_dual ∥ ≤ 1} :=
+begin
+  have eq : metric.closed_ball (0 : dual 𝕜 E) 1 = {x' : dual 𝕜 E | ∥ x' ∥ ≤ 1},
+  { ext x', simp only [dist_zero_right, metric.mem_closed_ball, set.mem_set_of_eq], },
+  rw eq,
+  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_bInter],
+  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 (weak_dual.eval_continuous _ _ z),
+end
+
+end polar_sets_in_weak_dual