refactor(Analysis/LocallyConvex/AbsConvexOpen): Break out AbsConvexOpenSets into its own file (#21928)

Break out `AbsConvexOpenSets` into its own file.

This allows `Mathlib.Analysis.LocallyConvex.AbsConvex` to be imported without also pulling in `Mathlib.Analysis.LocallyConvex.WithSeminorms` and `Mathlib.Analysis.Convex.Gauge`.

Author: mans0954

Mathlib.lean

@@ -1456,6 +1456,7 @@ import Mathlib.Analysis.InnerProductSpace.TwoDim
 import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
 import Mathlib.Analysis.InnerProductSpace.l2Space
 import Mathlib.Analysis.LocallyConvex.AbsConvex
+import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 import Mathlib.Analysis.LocallyConvex.Barrelled
 import Mathlib.Analysis.LocallyConvex.Basic

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
-import Mathlib.Analysis.LocallyConvex.WithSeminorms
-import Mathlib.Analysis.Convex.Gauge
 import Mathlib.Analysis.Convex.TotallyBounded
 
 /-!
@@ -21,8 +19,6 @@ topological vector space has a basis consisting of absolutely convex sets.
   containing `s`;
 * `closedAbsConvexHull`: the closed absolutely convex hull of a set `s` is the smallest absolutely
   convex set containing `s`;
-* `gaugeSeminormFamily`: the seminorm family induced by all open absolutely convex neighborhoods
-  of zero.
 
 ## Main statements
 
@@ -32,8 +28,6 @@ topological vector space has a basis consisting of absolutely convex sets.
   of `s`;
 * `closedAbsConvexHull_closure_eq_closedAbsConvexHull` : the closed absolutely convex hull of the
   closure of `s` equals the closed absolutely convex hull of `s`;
-* `with_gaugeSeminormFamily`: the topology of a locally convex space is induced by the family
-  `gaugeSeminormFamily`.
 
 ## Implementation notes
 
@@ -48,7 +42,6 @@ over a `SeminormedRing` `𝕜` and convex over `ℝ`, assuming `IsScalarTower 
 disks, convex, balanced
 -/
 
-
 open NormedField Set
 
 open NNReal Pointwise Topology
@@ -311,90 +304,3 @@ theorem totallyBounded_absConvexHull (hs : TotallyBounded s) :
   exact ⟨hs, totallyBounded_neg hs⟩
 
 end
-
-section AbsolutelyConvexSets
-
-variable [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜]
-variable [SMul 𝕜 E] [SMul ℝ E]
-variable (𝕜 E)
-
-/-- The type of absolutely convex open sets. -/
-def AbsConvexOpenSets :=
-  { s : Set E // (0 : E) ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s }
-
-noncomputable instance AbsConvexOpenSets.instCoeTC : CoeTC (AbsConvexOpenSets 𝕜 E) (Set E) :=
-  ⟨Subtype.val⟩
-
-namespace AbsConvexOpenSets
-
-variable {𝕜 E}
-
-theorem coe_zero_mem (s : AbsConvexOpenSets 𝕜 E) : (0 : E) ∈ (s : Set E) :=
-  s.2.1
-
-theorem coe_isOpen (s : AbsConvexOpenSets 𝕜 E) : IsOpen (s : Set E) :=
-  s.2.2.1
-
-theorem coe_nhds (s : AbsConvexOpenSets 𝕜 E) : (s : Set E) ∈ 𝓝 (0 : E) :=
-  s.coe_isOpen.mem_nhds s.coe_zero_mem
-
-theorem coe_balanced (s : AbsConvexOpenSets 𝕜 E) : Balanced 𝕜 (s : Set E) :=
-  s.2.2.2.1
-
-theorem coe_convex (s : AbsConvexOpenSets 𝕜 E) : Convex ℝ (s : Set E) :=
-  s.2.2.2.2
-
-end AbsConvexOpenSets
-
-instance AbsConvexOpenSets.instNonempty : Nonempty (AbsConvexOpenSets 𝕜 E) := by
-  rw [← exists_true_iff_nonempty]
-  dsimp only [AbsConvexOpenSets]
-  rw [Subtype.exists]
-  exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩
-
-end AbsolutelyConvexSets
-
-variable [RCLike 𝕜]
-variable [AddCommGroup E] [TopologicalSpace E]
-variable [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
-variable [ContinuousSMul ℝ E]
-variable (𝕜 E)
-
-/-- The family of seminorms defined by the gauges of absolute convex open sets. -/
-noncomputable def gaugeSeminormFamily : SeminormFamily 𝕜 E (AbsConvexOpenSets 𝕜 E) := fun s =>
-  gaugeSeminorm s.coe_balanced s.coe_convex (absorbent_nhds_zero s.coe_nhds)
-
-variable {𝕜 E}
-
-theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets 𝕜 E) :
-    (gaugeSeminormFamily 𝕜 E s).ball 0 1 = (s : Set E) := by
-  dsimp only [gaugeSeminormFamily]
-  rw [Seminorm.ball_zero_eq]
-  simp_rw [gaugeSeminorm_toFun]
-  exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_isOpen
-
-variable [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
-variable [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E]
-
-/-- The topology of a locally convex space is induced by the gauge seminorm family. -/
-theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) := by
-  refine SeminormFamily.withSeminorms_of_hasBasis _ ?_
-  refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_
-  · refine ⟨s, ⟨?_, rfl.subset⟩⟩
-    convert (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
-    rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
-  refine ⟨s, ⟨?_, rfl.subset⟩⟩
-  rw [SeminormFamily.basisSets_iff] at hs
-  rcases hs with ⟨t, r, hr, rfl⟩
-  rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
-  -- We have to show that the intersection contains zero, is open, balanced, and convex
-  refine
-    ⟨mem_iInter₂.mpr fun _ _ => by simp [Seminorm.mem_ball_zero, hr],
-      isOpen_biInter_finset fun S _ => ?_,
-      balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
-      convex_iInter₂ fun _ _ => Seminorm.convex_ball ..⟩
-  -- The only nontrivial part is to show that the ball is open
-  have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
-  have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
-  rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
-  exact S.coe_isOpen.smul₀ hr''

Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2022 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+import Mathlib.Analysis.LocallyConvex.AbsConvex
+import Mathlib.Analysis.LocallyConvex.WithSeminorms
+import Mathlib.Analysis.Convex.Gauge
+
+/-!
+# Absolutely convex open sets
+
+A set `s` in a commutative monoid `E` equipped with a topology is said to be an absolutely convex
+open set if it is absolutely convex and open. When `E` is a topological additive group, the topology
+coincides with the topology induced by the family of seminorms arising as gauges of absolutely
+convex open neighborhoods of zero.
+
+## Main definitions
+
+* `AbsConvexOpenSets`: sets which are absolutely convex and open
+* `gaugeSeminormFamily`: the seminorm family induced by all open absolutely convex neighborhoods
+  of zero.
+
+## Main statements
+
+* `with_gaugeSeminormFamily`: the topology of a locally convex space is induced by the family
+  `gaugeSeminormFamily`.
+
+-/
+
+open NormedField Set
+
+open NNReal Pointwise Topology
+
+variable {𝕜 E : Type*}
+
+section AbsolutelyConvexSets
+
+variable [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜]
+variable [SMul 𝕜 E] [SMul ℝ E]
+variable (𝕜 E)
+
+/-- The type of absolutely convex open sets. -/
+def AbsConvexOpenSets :=
+  { s : Set E // (0 : E) ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s }
+
+noncomputable instance AbsConvexOpenSets.instCoeTC : CoeTC (AbsConvexOpenSets 𝕜 E) (Set E) :=
+  ⟨Subtype.val⟩
+
+namespace AbsConvexOpenSets
+
+variable {𝕜 E}
+
+theorem coe_zero_mem (s : AbsConvexOpenSets 𝕜 E) : (0 : E) ∈ (s : Set E) :=
+  s.2.1
+
+theorem coe_isOpen (s : AbsConvexOpenSets 𝕜 E) : IsOpen (s : Set E) :=
+  s.2.2.1
+
+theorem coe_nhds (s : AbsConvexOpenSets 𝕜 E) : (s : Set E) ∈ 𝓝 (0 : E) :=
+  s.coe_isOpen.mem_nhds s.coe_zero_mem
+
+theorem coe_balanced (s : AbsConvexOpenSets 𝕜 E) : Balanced 𝕜 (s : Set E) :=
+  s.2.2.2.1
+
+theorem coe_convex (s : AbsConvexOpenSets 𝕜 E) : Convex ℝ (s : Set E) :=
+  s.2.2.2.2
+
+end AbsConvexOpenSets
+
+instance AbsConvexOpenSets.instNonempty : Nonempty (AbsConvexOpenSets 𝕜 E) := by
+  rw [← exists_true_iff_nonempty]
+  dsimp only [AbsConvexOpenSets]
+  rw [Subtype.exists]
+  exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩
+
+end AbsolutelyConvexSets
+
+variable [RCLike 𝕜]
+variable [AddCommGroup E] [TopologicalSpace E]
+variable [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
+variable [ContinuousSMul ℝ E]
+variable (𝕜 E)
+
+/-- The family of seminorms defined by the gauges of absolute convex open sets. -/
+noncomputable def gaugeSeminormFamily : SeminormFamily 𝕜 E (AbsConvexOpenSets 𝕜 E) := fun s =>
+  gaugeSeminorm s.coe_balanced s.coe_convex (absorbent_nhds_zero s.coe_nhds)
+
+variable {𝕜 E}
+
+theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets 𝕜 E) :
+    (gaugeSeminormFamily 𝕜 E s).ball 0 1 = (s : Set E) := by
+  dsimp only [gaugeSeminormFamily]
+  rw [Seminorm.ball_zero_eq]
+  simp_rw [gaugeSeminorm_toFun]
+  exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_isOpen
+
+variable [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
+variable [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E]
+
+/-- The topology of a locally convex space is induced by the gauge seminorm family. -/
+theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) := by
+  refine SeminormFamily.withSeminorms_of_hasBasis _ ?_
+  refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_
+  · refine ⟨s, ⟨?_, rfl.subset⟩⟩
+    convert (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
+    rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
+  refine ⟨s, ⟨?_, rfl.subset⟩⟩
+  rw [SeminormFamily.basisSets_iff] at hs
+  rcases hs with ⟨t, r, hr, rfl⟩
+  rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
+  -- We have to show that the intersection contains zero, is open, balanced, and convex
+  refine
+    ⟨mem_iInter₂.mpr fun _ _ => by simp [Seminorm.mem_ball_zero, hr],
+      isOpen_biInter_finset fun S _ => ?_,
+      balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
+      convex_iInter₂ fun _ _ => Seminorm.convex_ball ..⟩
+  -- The only nontrivial part is to show that the ball is open
+  have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
+  have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
+  rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
+  exact S.coe_isOpen.smul₀ hr''