feat(analysis/locally_convex): closed balanced sets are a basis of the topology (#12786)

We prove some topological properties of the balanced core.

Author: mcdoll

src/analysis/locally_convex/balanced_core_hull.lean

@@ -11,13 +11,13 @@ import order.closure
 
 ## Main definitions
 
-* `balanced_core`: the largest balanced subset of a set `s`.
-* `balanced_hull`: the smallest balanced superset of a set `s`.
+* `balanced_core`: The largest balanced subset of a set `s`.
+* `balanced_hull`: The smallest balanced superset of a set `s`.
 
 ## Main statements
 
 * `balanced_core_eq_Inter`: Characterization of the balanced core as an intersection over subsets.
-
+* `nhds_basis_closed_balanced`: The closed balanced sets form a basis of the neighborhood filter.
 
 ## Implementation details
 
@@ -39,7 +39,8 @@ balanced
 
 
 open set
-open_locale pointwise
+open_locale pointwise topological_space filter
+
 
 variables {𝕜 E ι : Type*}
 
@@ -71,6 +72,9 @@ begin
   exact ht.2,
 end
 
+lemma balanced_core_emptyset : balanced_core 𝕜 (∅ : set E) = ∅ :=
+set.eq_empty_of_subset_empty (balanced_core_subset _)
+
 lemma balanced_core_mem_iff {s : set E} {x : E} : x ∈ balanced_core 𝕜 s ↔
   ∃ t : set E, balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t :=
 by simp_rw [balanced_core, mem_sUnion, mem_set_of_eq, exists_prop, and_assoc]
@@ -241,6 +245,83 @@ begin
   refine mem_of_subset_of_mem balanced_core_subset_balanced_core_aux (balanced_core_zero_mem hs),
 end
 
+lemma subset_balanced_core {U V : set E} (hV' : (0 : E) ∈ V)
+  (hUV : ∀ (a : 𝕜) (ha : ∥a∥ ≤ 1), a • U ⊆ V) :
+  U ⊆ balanced_core 𝕜 V :=
+begin
+  rw balanced_core_eq_Inter hV',
+  refine set.subset_Inter₂ (λ a ha, _),
+  rw [←one_smul 𝕜 U, ←mul_inv_cancel (norm_pos_iff.mp (lt_of_lt_of_le zero_lt_one ha)),
+    ←smul_eq_mul, smul_assoc],
+  refine set.smul_set_mono (hUV a⁻¹ _),
+  rw [norm_inv],
+  exact inv_le_one ha,
+end
+
 end normed_field
 
 end balanced_hull
+
+/-! ### Topological properties -/
+
+section topology
+
+variables [nondiscrete_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E]
+  [has_continuous_smul 𝕜 E]
+
+lemma balanced_core_is_closed {U : set E} (hU : is_closed U) : is_closed (balanced_core 𝕜 U) :=
+begin
+  by_cases h : (0 : E) ∈ U,
+  { rw balanced_core_eq_Inter h,
+    refine is_closed_Inter (λ a, _),
+    refine is_closed_Inter (λ ha, _),
+    have ha' := lt_of_lt_of_le zero_lt_one ha,
+    rw norm_pos_iff at ha',
+    refine is_closed_map_smul_of_ne_zero ha' U hU },
+  convert is_closed_empty,
+  contrapose! h,
+  exact balanced_core_nonempty_iff.mp (set.ne_empty_iff_nonempty.mp h),
+end
+
+lemma balanced_core_mem_nhds_zero {U : set E} (hU : U ∈ 𝓝 (0 : E)) :
+  balanced_core 𝕜 U ∈ 𝓝 (0 : E) :=
+begin
+  -- Getting neighborhoods of the origin for `0 : 𝕜` and `0 : E`
+  have h : filter.tendsto (λ (x : 𝕜 × E), x.fst • x.snd) (𝓝 (0,0)) (𝓝 ((0 : 𝕜) • (0 : E))) :=
+  continuous_iff_continuous_at.mp has_continuous_smul.continuous_smul (0, 0),
+  rw [smul_zero] at h,
+  have h' := filter.has_basis.prod (@metric.nhds_basis_ball 𝕜 _ 0) (filter.basis_sets (𝓝 (0 : E))),
+  simp_rw [←nhds_prod_eq, id.def] at h',
+  have h'' := filter.tendsto.basis_left h h' U hU,
+  rcases h'' with ⟨x, hx, h''⟩,
+  cases normed_field.exists_norm_lt 𝕜 hx.left with y hy,
+  have hy' : y ≠ 0 := norm_pos_iff.mp hy.1,
+  let W := y • x.snd,
+  rw ←filter.exists_mem_subset_iff,
+  refine ⟨W, (set_smul_mem_nhds_zero_iff hy').mpr hx.2, _⟩,
+  -- It remains to show that `W ⊆ balanced_core 𝕜 U`
+  refine subset_balanced_core (mem_of_mem_nhds hU) (λ a ha, _),
+  refine set.subset.trans (λ z hz, _) (set.maps_to'.mp h''),
+  rw [set.image_prod, set.image2_smul],
+  rw set.mem_smul_set at hz,
+  rcases hz with ⟨z', hz', hz⟩,
+  rw [←hz, set.mem_smul],
+  refine ⟨a • y, y⁻¹ • z', _, _, _⟩,
+  { rw [algebra.id.smul_eq_mul, mem_ball_zero_iff, norm_mul, ←one_mul x.fst],
+    exact mul_lt_mul' ha hy.2 hy.1.le zero_lt_one },
+  { convert set.smul_mem_smul_set hz',
+    rw [←smul_assoc y⁻¹ y x.snd, smul_eq_mul, inv_mul_cancel hy', one_smul] },
+  rw [smul_assoc, ←smul_assoc y y⁻¹ z', smul_eq_mul, mul_inv_cancel hy', one_smul],
+end
+
+variables (𝕜)
+
+lemma nhds_basis_closed_balanced [regular_space E] : (𝓝 (0 : E)).has_basis
+  (λ (s : set E), s ∈ 𝓝 (0 : E) ∧ is_closed s ∧ balanced 𝕜 s) id :=
+begin
+  refine (closed_nhds_basis 0).to_has_basis (λ s hs, _) (λ s hs, ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩),
+  refine ⟨balanced_core 𝕜 s, ⟨balanced_core_mem_nhds_zero hs.1, _⟩, balanced_core_subset s⟩,
+  refine ⟨balanced_core_is_closed hs.2, balanced_core_balanced s⟩
+end
+
+end topology