leanprover-community · mans0954 · Feb 15, 2025 · Feb 15, 2025 · Feb 15, 2025 · Feb 16, 2025
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1968,6 +1968,7 @@ public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
 public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 public import Mathlib.Analysis.LocallyConvex.Barrelled
 public import Mathlib.Analysis.LocallyConvex.Basic
+public import Mathlib.Analysis.LocallyConvex.Bipolar
 public import Mathlib.Analysis.LocallyConvex.Bounded
 public import Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
 public import Mathlib.Analysis.LocallyConvex.Montel
@@ -7246,6 +7247,7 @@ public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
 public import Mathlib.Topology.Algebra.Module.LinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMapPiProd
 public import Mathlib.Topology.Algebra.Module.LinearPMap
+public import Mathlib.Topology.Algebra.Module.LinearSpan
 public import Mathlib.Topology.Algebra.Module.LocallyConvex
 public import Mathlib.Topology.Algebra.Module.ModuleTopology
 public import Mathlib.Topology.Algebra.Module.Multilinear.Basic

diff --git a/Mathlib/Analysis/LocallyConvex/AbsConvex.lean b/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
@@ -182,6 +182,10 @@ theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {s : Set E} :
       (closure_subset_closedAbsConvexHull (𝕜 := 𝕜) (E := E))))
     ((closedAbsConvexHull 𝕜).monotone subset_closure)
 
+@[simp]
+theorem closedAbsConvexHull_empty : closedAbsConvexHull 𝕜 (∅ : Set E) = ∅ :=
+  subset_eq_empty (closedAbsConvexHull_min (fun _ a ↦ a) AbsConvex.empty isClosed_empty) rfl
+
 end AbsolutelyConvex
 
 section NormedField

diff --git a/Mathlib/Analysis/LocallyConvex/Bipolar.lean b/Mathlib/Analysis/LocallyConvex/Bipolar.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2025 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+module
+
+public import Mathlib.Analysis.LocallyConvex.Polar
+public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.Normed.Module.Convex
+public import Mathlib.Analysis.LocallyConvex.Separation
+
+/-!
+
+# Bipolar Theorem
+
+## Main statements
+
+- `LinearMap.flip_polar_polar_eq`: The Bipolar Theorem: The bipolar of a set coincides with its
+  closed absolutely convex hull.
+
+## References
+
+* [Conway, *A course in functional analysis*][conway1990]
+
+## Tags
+
+bipolar, locally convex space
+-/
+
+public section
+
+open scoped ComplexOrder
+
+variable {𝕜 E F : Type*}
+
+namespace LinearMap
+
+section
+
+variable [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F]
+variable [Module 𝕜 E] [Module 𝕜 F]
+
+variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E)
+
+/-
+When `B` is left-separating, the closure of the empty set is the singleton `{0}`. This is in
+contrast to the closed absolutely convex hull of the empty set, which is again the empty set.
+c.f. `closureOperator_polar_gc_nonempty` below.
+-/
+example (h : SeparatingLeft B) : B.polar_gc.closureOperator (∅ : Set E) = {0} := by
+  simp only [GaloisConnection.closureOperator_apply, Function.comp_apply, polar_empty,
+    OrderDual.ofDual_toDual, (B.flip.polar_univ h)]
+
+end
+
+
+section RCLike
+
+variable [RCLike 𝕜] [AddCommGroup E] [AddCommGroup F]
+variable [Module 𝕜 E] [Module 𝕜 F]
+
+variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}
+
+variable [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
+
+/-
+The Bipolar Theorem: The bipolar of a set coincides with its closed absolutely convex hull.
+[Conway, *A course in functional analysis*, Chapter V. 1.8][conway1990]
+-/
+open scoped ComplexConjugate
+theorem flip_polar_polar_eq {s : Set E} [Nonempty s] :
+    B.flip.polar (B.polar s) = closedAbsConvexHull (E := WeakBilin B) 𝕜 s := by
+  refine subset_antisymm ?_ <| closedAbsConvexHull_min (E := WeakBilin B)
+    (subset_bipolar B s) (absConvex_polar _) (polar_isClosed B.flip _)
+  rw [← Set.compl_subset_compl]
+  -- Let `x` be an element not in `(closedAbsConvexHull 𝕜) s`
+  intro x hx
+  -- Use the Geometric Hahn-Banach theorem to obtain a function `f` and a constant `u` separating
+  -- `(closedAbsConvexHull 𝕜) s` and `x`
+  obtain ⟨f, ⟨u, ⟨hf₁, hf₂⟩⟩⟩ :=
+    RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜) (E := WeakBilin B)
+      (by rw [← convex_RCLike_iff_convex_real (K := 𝕜)]; exact absConvex_convexClosedHull.2)
+      isClosed_closedAbsConvexHull hx
+  -- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive
+  have f_zero_lt_u : RCLike.re (f 0) < u :=
+    (hf₁ 0) (absConvexHull_subset_closedAbsConvexHull zero_mem_absConvexHull)
+  rw [map_zero, map_zero] at f_zero_lt_u
+  -- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`
+  set g := (1/u : ℝ) • f with fg
+  have u_smul_g_eq_f : u • g = f := by
+    rw [fg, one_div, ← smul_assoc, smul_eq_mul, mul_inv_cancel₀ (ne_of_lt f_zero_lt_u).symm,
+      one_smul]
+  have re_g_a_lt_one {a : _} (ha : a ∈ (closedAbsConvexHull (E := WeakBilin B) 𝕜) s) :
+    RCLike.re (g a) < 1 := by
+    rw [fg, ContinuousLinearMap.coe_smul', Pi.smul_apply, RCLike.smul_re, one_div,
+      ← (inv_mul_cancel₀ (lt_iff_le_and_ne.mp f_zero_lt_u).2.symm)]
+    exact mul_lt_mul_of_pos_left ((hf₁ _) ha) (inv_pos_of_pos f_zero_lt_u)
+  -- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`
+  obtain ⟨f₀, hf₀⟩ := B.dualEmbedding_surjective g
+  -- Then, by construction, `f₀` is in the polar of `s`
+  have mem_polar : f₀ ∈ (B.polar (E := WeakBilin B) s) := by
+    simp only [← hf₀, WeakBilin.eval, coe_mk, AddHom.coe_mk, ContinuousLinearMap.coe_mk']
+      at re_g_a_lt_one
+    intro x₂ hx₂
+    let l := conj (B x₂ f₀) / ‖B x₂ f₀‖
+    have lnorm : ‖l‖ ≤ 1 := by
+      rw [norm_div, RCLike.norm_conj, norm_algebraMap', norm_norm]
+      exact div_self_le_one _
+    have i1 : RCLike.re ((B.flip f₀) (l • x₂)) ≤ 1 := le_of_lt <| re_g_a_lt_one
+      <| balanced_iff_smul_mem.mp absConvex_convexClosedHull.1 lnorm
+        (subset_closedAbsConvexHull hx₂)
+    rwa [CompatibleSMul.map_smul, smul_eq_mul, mul_comm, ← mul_div_assoc, LinearMap.flip_apply,
+      RCLike.mul_conj, sq, mul_self_div_self, RCLike.ofReal_re] at i1
+  -- and `1 < Re (B x f₀)`
+  have one_lt_x_f₀ : 1 < RCLike.re (B x f₀) := by
+    rw [← one_lt_inv_mul₀ f_zero_lt_u] at hf₂
+    suffices u⁻¹ * RCLike.re (f x) = RCLike.re ((B x) f₀) by exact lt_of_lt_of_eq hf₂ this
+    rw [← RCLike.re_ofReal_mul]
+    congr
+    simp only [map_inv₀, ← u_smul_g_eq_f, ← hf₀, WeakBilin.eval, coe_mk, AddHom.coe_mk,
+      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_mk', Pi.smul_apply,
+      Algebra.mul_smul_comm]
+    rw [← smul_eq_mul, ← smul_assoc]
+    norm_cast
+    simp only [smul_eq_mul, mul_inv_cancel₀ (ne_of_lt f_zero_lt_u).symm, map_one, one_mul]
+    exact flip_apply (f := B) (n:= f₀) (m := x)
+  -- From which it follows that `x` can't be in the bipolar of `s`
+  exact fun hc ↦ ((lt_iff_le_not_ge.mp one_lt_x_f₀).2)
+    (Preorder.le_trans (RCLike.re ((B x) f₀)) ‖(B x) f₀‖ 1
+      (RCLike.re_le_norm ((B x) f₀)) (hc f₀ mem_polar))
+
+/-
+This fails when `s` is empty. Indeed, `closedAbsConvexHull (E := WeakBilin B) 𝕜 s` is the empty set,
+but `B.polar_gc.closureOperator s` equals `{0}` when `B` is left separating (see example above).
+-/
+lemma closureOperator_polar_gc_nonempty {s : Set E} [Nonempty s] :
+    B.polar_gc.closureOperator s = closedAbsConvexHull (E := WeakBilin B) 𝕜 s := by
+  simp [flip_polar_polar_eq]
+
+end RCLike
+
+end LinearMap
diff --git a/Mathlib/Analysis/LocallyConvex/Polar.lean b/Mathlib/Analysis/LocallyConvex/Polar.lean
@@ -6,8 +6,11 @@ Authors: Moritz Doll, Kalle Kytölä
 module
 
 public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.Analysis.RCLike.Lemmas
 public import Mathlib.LinearAlgebra.SesquilinearForm.Basic
 public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Analysis.LocallyConvex.AbsConvex
+public import Mathlib.Analysis.Normed.Module.Convex
 
 /-!
 # Polar set
@@ -261,3 +264,23 @@ theorem polar_univ : polar 𝕜 (univ : Set E) = {(0 : StrongDual 𝕜 E)} :=
 end
 
 end StrongDual
+
+namespace LinearMap
+
+section NormedField
+
+variable [RCLike 𝕜] [AddCommMonoid E] [AddCommMonoid F]
+variable [Module 𝕜 E] [Module 𝕜 F]
+
+variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E)
+
+open ComplexOrder in
+theorem absConvex_polar : AbsConvex 𝕜 (B.polar s) := by
+  rw [polar_eq_biInter_preimage]
+  exact AbsConvex.iInter₂ fun i hi =>
+    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
+      (convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩
+
+end NormedField
+
+end LinearMap
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import Mathlib.LinearAlgebra.Dual.Lemmas
 public import Mathlib.LinearAlgebra.Finsupp.Span
 public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Topology.Algebra.Module.LinearSpan
 
 /-!
 # Weak Dual in Topological Vector Spaces
@@ -39,7 +40,6 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 ## References
 
 * [Bourbaki, *Topological Vector Spaces*][bourbaki1987]
-* [Rudin, *Functional Analysis*][rudin1991]
 
 ## Tags
 
@@ -100,34 +100,6 @@ open scoped NNReal
 
 section
 
-section TopologicalRing
-
-variable [Finite ι] [Field 𝕜] [t𝕜 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
-  [AddCommGroup E] [Module 𝕜 E] [T0Space 𝕜]
-
-/- A linear functional `φ` can be expressed as a linear combination of linear functionals `f₁,…,fₙ`
-if and only if `φ` is continuous with respect to the topology induced by `f₁,…,fₙ`. See
-`LinearMap.mem_span_iff_continuous` for a result about arbitrary collections of linear functionals.
--/
-theorem mem_span_iff_continuous_of_finite {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
-    φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (f i) t𝕜, t𝕜] φ := by
-  let _ := ⨅ i, induced (f i) t𝕜
-  constructor
-  · exact Submodule.span_induction
-      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
-      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
-  · intro φ_cont
-    refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
-    simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
-    have : Inseparable x 0 := by
-      -- Maybe missing lemmas about `Inseparable`?
-      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-    simpa only [map_zero] using (this.map φ_cont).eq
-
-end TopologicalRing
-
-section NontriviallyNormedField
-
 variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
 
 /- A linear functional `φ` is in the span of a collection of linear functionals if and only if `φ`
@@ -200,8 +172,6 @@ weak topology. -/
 noncomputable def leftDualEquiv (hl : B.SeparatingLeft) : E ≃ₗ[𝕜] StrongDual 𝕜 (WeakBilin B.flip) :=
   rightDualEquiv _ (LinearMap.flip_separatingRight.mpr hl)
 
-end NontriviallyNormedField
-
 end
 
 end LinearMap

diff --git a/Mathlib/Topology/Algebra/Module/LinearSpan.lean b/Mathlib/Topology/Algebra/Module/LinearSpan.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2025 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+module
+
+public import Mathlib.LinearAlgebra.Dual.Lemmas
+public import Mathlib.Topology.Algebra.Ring.Basic
+public import Mathlib.Analysis.Normed.Field.Basic
+public import Mathlib.Analysis.Normed.Group.Uniform
+public import Mathlib.Topology.Algebra.MulAction
+public import Mathlib.Topology.Algebra.Monoid
+public import Mathlib.Analysis.Normed.Field.Lemmas
+public import Mathlib.LinearAlgebra.Finsupp.Span
+public import Mathlib.Analysis.LocallyConvex.WithSeminorms
+
+/-!
+# Linear Span
+
+## Main statements
+
+- `LinearMap.mem_span_iff_continuous_of_finite` A linear functional `φ` can be expressed as a linear
+  combination of finitely many linear functionals `f₁,…,fₙ` if and only if `φ` is continuous with
+  respect to the topology induced by `f₁,…,fₙ`.
+- `LinearMap.mem_span_iff_continuous` A linear functional `φ` is in the span of a collection of
+  linear functionals if and only if `φ` is continuous with respect to the topology induced by the
+  collection of linear functionals.
+
+## References
+
+* [Rudin, *Functional Analysis*][rudin1991]
+
+## Tags
+
+span, continuous
+
+-/
+
+public section
+
+open Topology TopologicalSpace
+
+namespace LinearMap
+
+variable {ι 𝕜 E F : Type*}
+
+section TopologicalRing
+
+variable [Finite ι] [Field 𝕜] [t𝕜 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [T0Space 𝕜]
+  [AddCommGroup E] [Module 𝕜 E]
+
+/- A linear functional `φ` can be expressed as a linear combination of finitely many linear
+functionals `f₁,…,fₙ` if and only if `φ` is continuous with respect to the topology induced by
+`f₁,…,fₙ`. See `LinearMap.mem_span_iff_continuous` for a result about arbitrary collections of
+linear functionals. -/
+theorem mem_span_iff_continuous_of_finite {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
+    φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous[⨅ i, induced (f i) t𝕜, t𝕜] φ := by
+  let _ := ⨅ i, induced (f i) t𝕜
+  refine ⟨Submodule.span_induction
+      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
+      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c), fun φ_cont ↦ ?_⟩
+  apply mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
+  simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
+  have : Inseparable x 0 := by
+    -- Maybe missing lemmas about `Inseparable`?
+    simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
+  simpa [map_zero] using (this.map φ_cont).eq
+
+end TopologicalRing
+
+section NontriviallyNormedField
+
+variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+
+/- A linear functional `φ` is in the span of a collection of linear functionals if and only if `φ`
+is continuous with respect to the topology induced by the collection of linear functionals. See
+`LinearMap.mem_span_iff_continuous_of_finite` for a result about finite collections of linear
+functionals. -/
+theorem mem_span_iff_continuous {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) :
+    φ ∈ Submodule.span 𝕜 (Set.range f) ↔
+    Continuous[⨅ i, induced (f i) inferInstance, inferInstance] φ := by
+  letI t𝕜 : TopologicalSpace 𝕜 := inferInstance
+  letI t₁ : TopologicalSpace E := ⨅ i, induced (f i) t𝕜
+  letI t₂ (s : Finset ι) : TopologicalSpace E := ⨅ i : s, induced (f i) t𝕜
+  suffices
+      Continuous[t₁, t𝕜] φ ↔ ∃ s : Finset ι, Continuous[t₂ s, t𝕜] φ by
+    simp only [Submodule.span_range_eq_iSup, this, ← mem_span_iff_continuous_of_finite,
+      iSup_subtype]
+    rw [Submodule.mem_iSup_iff_exists_finset]
+  have t₁_group : @IsTopologicalAddGroup E t₁ _ :=
+    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
+  have t₂_group (s : Finset ι) : @IsTopologicalAddGroup E (t₂ s) _ :=
+    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
+  have t₁_smul : @ContinuousSMul 𝕜 E _ _ t₁ :=
+    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
+  have t₂_smul (s : Finset ι) : @ContinuousSMul 𝕜 E _ _ (t₂ s) :=
+    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
+  simp only [Seminorm.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]
+  conv in Continuous _ => rw [Seminorm.continuous_iff one_pos, nhds_iInf]
+  conv in Continuous _ =>
+    rw [let _ := t₂ s; Seminorm.continuous_iff one_pos, nhds_iInf, iInf_subtype]
+  rw [Filter.mem_iInf_finite]
+
+end NontriviallyNormedField
+
+end LinearMap