chore(Analysis/NormedSpace/HahnBanach): move and split files (#29447)

This moves or splits the files in `Analysis/NormedSpace/HahnBanach/` accordingly:

- `Separation` → `Analysis/LocallyConvex/Separation`
- `Extension` → `Analysis/Normed/Module/HahnBanach`
- `SeparatingDual`: split, mostly in `Analysis/LocallyConvex/SeparatingDual`, but a few completeness results are sent to `Analysis/Normed/Operator/CompleteCodomain`.

The split allows us to significantly reduce the imports of `SeparatingDual`, albeit with a new proof that a normed space over `RCLike 𝕜` has a separating dual. Here we use the geometric Hahn-Banach theorem instead of the analytic one.

This is part of #28698 to migrate the material in `Analysis/NormedSpace/` to other locations.

Author: j-loreaux

Counterexamples/Phillips.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
+import Mathlib.Analysis.Normed.Module.HahnBanach
 import Mathlib.MeasureTheory.Integral.Bochner.Set
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Mathlib.Topology.ContinuousMap.Bounded.Star

Mathlib.lean

@@ -1788,6 +1788,8 @@ import Mathlib.Analysis.LocallyConvex.Basic
 import Mathlib.Analysis.LocallyConvex.Bounded
 import Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
 import Mathlib.Analysis.LocallyConvex.Polar
+import Mathlib.Analysis.LocallyConvex.SeparatingDual
+import Mathlib.Analysis.LocallyConvex.Separation
 import Mathlib.Analysis.LocallyConvex.StrongTopology
 import Mathlib.Analysis.LocallyConvex.WeakDual
 import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
@@ -1884,6 +1886,7 @@ import Mathlib.Analysis.Normed.Module.Completion
 import Mathlib.Analysis.Normed.Module.Convex
 import Mathlib.Analysis.Normed.Module.Dual
 import Mathlib.Analysis.Normed.Module.FiniteDimension
+import Mathlib.Analysis.Normed.Module.HahnBanach
 import Mathlib.Analysis.Normed.Module.RCLike.Basic
 import Mathlib.Analysis.Normed.Module.RCLike.Extend
 import Mathlib.Analysis.Normed.Module.RCLike.Real
@@ -1898,6 +1901,7 @@ import Mathlib.Analysis.Normed.Operator.Basic
 import Mathlib.Analysis.Normed.Operator.Bilinear
 import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
 import Mathlib.Analysis.Normed.Operator.Compact
+import Mathlib.Analysis.Normed.Operator.CompleteCodomain
 import Mathlib.Analysis.Normed.Operator.Completeness
 import Mathlib.Analysis.Normed.Operator.Conformal
 import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
@@ -1940,9 +1944,6 @@ import Mathlib.Analysis.NormedSpace.ENormedSpace
 import Mathlib.Analysis.NormedSpace.Extend
 import Mathlib.Analysis.NormedSpace.Extr
 import Mathlib.Analysis.NormedSpace.FunctionSeries
-import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
-import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
-import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
 import Mathlib.Analysis.NormedSpace.HomeomorphBall
 import Mathlib.Analysis.NormedSpace.IndicatorFunction
 import Mathlib.Analysis.NormedSpace.Int

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean

@@ -5,8 +5,8 @@ Authors: Frédéric Dupuis, Anatole Dedecker
 -/
 
 import Mathlib.Analysis.Normed.Algebra.Spectrum
-import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
+import Mathlib.Analysis.RCLike.Lemmas
 import Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 

Mathlib/Analysis/Calculus/ParametricIntegral.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot
 import Mathlib.Analysis.Calculus.MeanValue
 import Mathlib.MeasureTheory.Integral.DominatedConvergence
 import Mathlib.MeasureTheory.Integral.Bochner.Set
-import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
+import Mathlib.Analysis.LocallyConvex.SeparatingDual
 
 /-!
 # Derivatives of integrals depending on parameters

Mathlib/Analysis/Convex/Cone/Dual.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Andrew Yang
 -/
 import Mathlib.Analysis.Convex.Cone.Basic
-import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+import Mathlib.Analysis.LocallyConvex.Separation
 import Mathlib.Geometry.Convex.Cone.Dual
 import Mathlib.Topology.Algebra.Module.PerfectPairing
 

Mathlib/Analysis/Convex/KreinMilman.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.Convex.Exposed
-import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+import Mathlib.Analysis.LocallyConvex.Separation
 import Mathlib.Topology.Algebra.ContinuousAffineMap
 
 /-!

Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean renamed to Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Filippo A. E. Nuccio
 -/
 import Mathlib.Algebra.Central.Defs
-import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
-import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
-import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+import Mathlib.Analysis.LocallyConvex.Separation
+import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.LinearAlgebra.Dual.Lemmas
 
 /-!
@@ -48,10 +47,12 @@ instance {E : Type*} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGrou
     exact ⟨f, hf.ne'⟩⟩
 
 instance {E 𝕜 : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : SeparatingDual 𝕜 E :=
-  ⟨fun x hx ↦ by
-    rcases exists_dual_vector 𝕜 x hx with ⟨f, -, hf⟩
-    refine ⟨f, ?_⟩
-    simpa [hf] using hx⟩
+  ⟨fun x hx ↦
+    let : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
+    let : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
+    have : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
+    have : LocallyConvexSpace ℝ E := NormedSpace.toLocallyConvexSpace' 𝕜
+    RCLike.geometric_hahn_banach_point_point hx |>.imp fun f hf hf' ↦ by simp [hf'] at hf⟩
 
 namespace SeparatingDual
 
@@ -183,64 +184,6 @@ theorem exists_continuousLinearEquiv_apply_eq [ContinuousSMul R V]
       continuous_id.add ((continuous_const.mul G.continuous).smul continuous_const) }
   exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩
 
-open Filter
-open scoped Topology
-
-section
-variable (𝕜 E F : Type*) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [SeparatingDual 𝕜 E] [Nontrivial E]
-
-/-- If a space of linear maps from `E` to `F` is complete, and `E` is nontrivial, then `F` is
-complete. -/
-lemma completeSpace_of_completeSpace_continuousLinearMap [CompleteSpace (E →L[𝕜] F)] :
-    CompleteSpace F := by
-  refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
-  obtain ⟨v, hv⟩ : ∃ (v : E), v ≠ 0 := exists_ne 0
-  obtain ⟨φ, hφ⟩ : ∃ φ : StrongDual 𝕜 E, φ v = 1 := exists_eq_one hv
-  let g : ℕ → (E →L[𝕜] F) := fun n ↦ ContinuousLinearMap.smulRightL 𝕜 E F φ (f n)
-  have : CauchySeq g := (ContinuousLinearMap.smulRightL 𝕜 E F φ).lipschitz.cauchySeq_comp hf
-  obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
-  refine ⟨a v, ?_⟩
-  have : Tendsto (fun n ↦ g n v) atTop (𝓝 (a v)) := by
-    have : Continuous (fun (i : E →L[𝕜] F) ↦ i v) := by fun_prop
-    exact (this.tendsto _).comp ha
-  simpa [g, ContinuousLinearMap.smulRightL, hφ]
-
-lemma completeSpace_continuousLinearMap_iff :
-    CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F :=
-  ⟨fun _h ↦ completeSpace_of_completeSpace_continuousLinearMap 𝕜 E F, fun _h ↦ inferInstance⟩
-
-open ContinuousMultilinearMap
-
-variable {ι : Type*} [Finite ι] {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)]
-  [∀ i, NormedSpace 𝕜 (M i)] [∀ i, SeparatingDual 𝕜 (M i)]
-
-/-- If a space of multilinear maps from `Π i, E i` to `F` is complete, and each `E i` has a nonzero
-element, then `F` is complete. -/
-lemma completeSpace_of_completeSpace_continuousMultilinearMap
-    [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)]
-    {m : ∀ i, M i} (hm : ∀ i, m i ≠ 0) : CompleteSpace F := by
-  refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
-  have : ∀ i, ∃ φ : StrongDual 𝕜 (M i), φ (m i) = 1 := fun i ↦ exists_eq_one (hm i)
-  choose φ hφ using this
-  cases nonempty_fintype ι
-  let g : ℕ → (ContinuousMultilinearMap 𝕜 M F) := fun n ↦
-    compContinuousLinearMapL φ
-    (ContinuousMultilinearMap.smulRightL 𝕜 _ F ((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))
-  have : CauchySeq g := by
-    refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_
-    exact (ContinuousLinearMap.lipschitz _).cauchySeq_comp hf
-  obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
-  refine ⟨a m, ?_⟩
-  have : Tendsto (fun n ↦ g n m) atTop (𝓝 (a m)) := ((continuous_eval_const _).tendsto _).comp ha
-  simpa [g, hφ]
-
-lemma completeSpace_continuousMultilinearMap_iff {m : ∀ i, M i} (hm : ∀ i, m i ≠ 0) :
-    CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F :=
-  ⟨fun _h ↦ completeSpace_of_completeSpace_continuousMultilinearMap 𝕜 F hm, fun _h ↦ inferInstance⟩
-
-end
-
 end Field
 
 end SeparatingDual

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean renamed to Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -5,7 +5,8 @@ Authors: Frédéric Dupuis
 -/
 
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
-import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
+import Mathlib.Analysis.LocallyConvex.SeparatingDual
+import Mathlib.Topology.Algebra.Module.StrongTopology
 
 /-!
 # The weak operator topology

Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+import Mathlib.Analysis.LocallyConvex.Separation
 import Mathlib.LinearAlgebra.Dual.Defs
 import Mathlib.Topology.Algebra.Module.WeakDual