feat(Analysis/LocallyConvex): characterize dense submodules by annihilators

Mathlib/Analysis/LocallyConvex/Polar.lean

@@ -5,6 +5,7 @@ Authors: Moritz Doll, Kalle Kytölä
 -/
 module
 
+public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.LinearAlgebra.SesquilinearForm.Basic
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
 public import Mathlib.Analysis.Normed.Field.Lemmas
@@ -26,6 +27,8 @@ any bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, where `𝕜` is a no
 * `LinearMap.polar_eq_iInter`: The polar as an intersection.
 * `LinearMap.subset_bipolar`: The polar is a subset of the bipolar.
 * `LinearMap.polar_isClosed`: The polar is closed in the weak topology induced by `B.flip`.
+* `Submodule.dense_iff_polarSubmodule_eq_bot`: A real submodule of a locally convex space is dense
+  if and only if its polar submodule is trivial.
 
 ## References
 
@@ -260,3 +263,17 @@ theorem polar_univ : polar 𝕜 (univ : Set E) = {(0 : StrongDual 𝕜 E)} :=
 end
 
 end StrongDual
+
+namespace Submodule
+
+variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E]
+  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
+
+/-- A real submodule of a locally convex space is dense if and only if its polar submodule is
+trivial. -/
+theorem dense_iff_polarSubmodule_eq_bot (s : Submodule ℝ E) :
+    Dense (s : Set E) ↔ StrongDual.polarSubmodule ℝ s = ⊥ := by
+  simp only [dense_iff_forall_dual_eq_zero, Submodule.eq_bot_iff,
+    StrongDual.mem_polarSubmodule]
+
+end Submodule

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -35,6 +35,9 @@ We provide many variations to stricten the result under more assumptions on the
 * `geometric_hahn_banach_point_closed`, `geometric_hahn_banach_closed_point`: One set is closed, the
   other one is a singleton. Strict separation.
 * `geometric_hahn_banach_point_point`: Both sets are singletons. Strict separation.
+
+As an application, `Submodule.dense_iff_forall_dual_eq_zero` characterizes dense real submodules
+by the vanishing of their continuous dual annihilators.
 -/
 
 public section
@@ -251,6 +254,40 @@ theorem iInter_halfSpaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
   obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point hs₁ hs₂ h
   obtain ⟨y, hy, hxy⟩ := hx l
   exact ((hxy.trans_lt (hlA y hy)).trans hl).not_ge le_rfl
+
+namespace Submodule
+
+variable (s : Submodule ℝ E)
+
+/-- A real submodule of a locally convex space is dense if and only if every continuous linear
+functional vanishing on it is zero. -/
+theorem dense_iff_forall_dual_eq_zero :
+    Dense (s : Set E) ↔ ∀ f : StrongDual ℝ E, (∀ x ∈ s, f x = 0) → f = 0 := by
+  constructor
+  · intro hs f hf
+    exact ContinuousLinearMap.ext_on (by simpa using hs) hf
+  · intro h
+    rw [Submodule.dense_iff_topologicalClosure_eq_top]
+    apply top_unique
+    intro x _
+    by_contra hxc
+    obtain ⟨f, u, hfc, hfx⟩ := geometric_hahn_banach_closed_point s.topologicalClosure.convex
+      s.isClosed_topologicalClosure hxc
+    have hrestr : f.toLinearMap.comp s.subtype = 0 := by
+      by_contra hf
+      obtain ⟨y, hy⟩ := (f.toLinearMap.comp s.subtype).surjective hf u
+      exact (hfc y (s.le_topologicalClosure y.property)).ne hy
+    have hf : f = 0 := h f fun y hy ↦ DFunLike.congr_fun hrestr ⟨y, hy⟩
+    simpa [hf] using (hfc 0 s.topologicalClosure.zero_mem).trans hfx
+
+/-- A nondense real submodule of a locally convex space admits a nonzero continuous linear
+functional vanishing on it. -/
+theorem exists_dual_annihilator_of_not_dense (hs : ¬ Dense (s : Set E)) :
+    ∃ f : StrongDual ℝ E, f ≠ 0 ∧ ∀ x ∈ s, f x = 0 := by
+  simpa only [dense_iff_forall_dual_eq_zero, not_forall, exists_prop, and_comm] using hs
+
+end Submodule
+
 end
 
 namespace RCLike