refactor(analysis/seminorm): move topology induced by seminorms to it…

…s own file (#12826)

Besides the copy and paste I removed the namespace `seminorm` from most parts (it is still there for the boundedness definitions and statements) and updated the module docstrings. No real code has changed.

src/analysis/locally_convex/with_seminorms.lean

@@ -0,0 +1,387 @@
+/-
+Copyright (c) 2022 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Anatole Dedecker
+-/
+
+import analysis.seminorm
+
+/-!
+# Topology induced by a family of seminorms
+
+## Main definitions
+
+* `seminorm_basis_zero`: The set of open seminorm balls for a family of seminorms.
+* `seminorm_module_filter_basis`: A module filter basis formed by the open balls.
+* `seminorm.is_bounded`: A linear map `f : E →ₗ[𝕜] F` is bounded iff every seminorm in `F` can be
+bounded by a finite number of seminorms in `E`.
+
+## Main statements
+
+* `continuous_from_bounded`: A bounded linear map `f : E →ₗ[𝕜] F` is continuous.
+* `with_seminorms.to_locally_convex_space`: A space equipped with a family of seminorms is locally
+convex.
+
+## TODO
+
+Show that for any locally convex space there exist seminorms that induce the topology.
+
+## Tags
+
+seminorm, locally convex
+-/
+
+open normed_field set seminorm
+open_locale big_operators nnreal pointwise topological_space
+
+variables {𝕜 E F G ι ι' : Type*}
+
+section filter_basis
+
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
+
+/-- A filter basis for the neighborhood filter of 0. -/
+def seminorm_basis_zero (p : ι → seminorm 𝕜 E) : set (set E) :=
+⋃ (s : finset ι) r (hr : 0 < r), singleton $ ball (s.sup p) (0 : E) r
+
+lemma seminorm_basis_zero_iff (p : ι → seminorm 𝕜 E) (U : set E) :
+  U ∈ seminorm_basis_zero p ↔ ∃ (i : finset ι) r (hr : 0 < r), U = ball (i.sup p) 0 r :=
+by simp only [seminorm_basis_zero, mem_Union, mem_singleton_iff]
+
+lemma seminorm_basis_zero_mem (p : ι → seminorm 𝕜 E) (i : finset ι) {r : ℝ} (hr : 0 < r) :
+  (i.sup p).ball 0 r ∈ seminorm_basis_zero p :=
+(seminorm_basis_zero_iff _ _).mpr ⟨i,_,hr,rfl⟩
+
+lemma seminorm_basis_zero_singleton_mem (p : ι → seminorm 𝕜 E) (i : ι) {r : ℝ} (hr : 0 < r) :
+  (p i).ball 0 r ∈ seminorm_basis_zero p :=
+(seminorm_basis_zero_iff _ _).mpr ⟨{i},_,hr, by rw finset.sup_singleton⟩
+
+lemma seminorm_basis_zero_nonempty (p : ι → seminorm 𝕜 E) [nonempty ι] :
+  (seminorm_basis_zero p).nonempty :=
+begin
+  let i := classical.arbitrary ι,
+  refine set.nonempty_def.mpr ⟨ball (p i) 0 1, _⟩,
+  exact seminorm_basis_zero_singleton_mem _ i zero_lt_one,
+end
+
+lemma seminorm_basis_zero_intersect (p : ι → seminorm 𝕜 E)
+  (U V : set E) (hU : U ∈ seminorm_basis_zero p) (hV : V ∈ seminorm_basis_zero p) :
+  ∃ (z : set E) (H : z ∈ (seminorm_basis_zero p)), z ⊆ U ∩ V :=
+begin
+  classical,
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r₁, hr₁, hU⟩,
+  rcases (seminorm_basis_zero_iff p V).mp hV with ⟨t, r₂, hr₂, hV⟩,
+  use ((s ∪ t).sup p).ball 0 (min r₁ r₂),
+  refine ⟨seminorm_basis_zero_mem p (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), _⟩,
+  rw [hU, hV, ball_finset_sup_eq_Inter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
+    ball_finset_sup_eq_Inter _ _ _ hr₁, ball_finset_sup_eq_Inter _ _ _ hr₂],
+  exact set.subset_inter
+    (set.Inter₂_mono' $ λ i hi, ⟨i, finset.subset_union_left _ _ hi, ball_mono $ min_le_left _ _⟩)
+    (set.Inter₂_mono' $ λ i hi, ⟨i, finset.subset_union_right _ _ hi, ball_mono $
+    min_le_right _ _⟩),
+end
+
+lemma seminorm_basis_zero_zero (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
+  (0 : E) ∈ U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨ι', r, hr, hU⟩,
+  rw [hU, mem_ball_zero, (ι'.sup p).zero],
+  exact hr,
+end
+
+lemma seminorm_basis_zero_add (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
+  ∃ (V : set E) (H : V ∈ (seminorm_basis_zero p)), V + V ⊆ U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  use (s.sup p).ball 0 (r/2),
+  refine ⟨seminorm_basis_zero_mem p s (div_pos hr zero_lt_two), _⟩,
+  refine set.subset.trans (ball_add_ball_subset (s.sup p) (r/2) (r/2) 0 0) _,
+  rw [hU, add_zero, add_halves'],
+end
+
+lemma seminorm_basis_zero_neg (p : ι → seminorm 𝕜 E) (U) (hU' : U ∈ seminorm_basis_zero p) :
+  ∃ (V : set E) (H : V ∈ (seminorm_basis_zero p)), V ⊆ (λ (x : E), -x) ⁻¹' U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU' with ⟨s, r, hr, hU⟩,
+  rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero],
+  exact ⟨U, hU', eq.subset hU⟩,
+end
+
+/-- The `add_group_filter_basis` induced by the filter basis `seminorm_basis_zero`. -/
+def seminorm_add_group_filter_basis [nonempty ι]
+  (p : ι → seminorm 𝕜 E) : add_group_filter_basis E :=
+add_group_filter_basis_of_comm (seminorm_basis_zero p)
+  (seminorm_basis_zero_nonempty p)
+  (seminorm_basis_zero_intersect p)
+  (seminorm_basis_zero_zero p)
+  (seminorm_basis_zero_add p)
+  (seminorm_basis_zero_neg p)
+
+lemma seminorm_basis_zero_smul_right (p : ι → seminorm 𝕜 E) (v : E) (U : set E)
+  (hU : U ∈ seminorm_basis_zero p) : ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rw [hU, filter.eventually_iff],
+  simp_rw [(s.sup p).mem_ball_zero, (s.sup p).smul],
+  by_cases h : 0 < (s.sup p) v,
+  { simp_rw (lt_div_iff h).symm,
+    rw ←_root_.ball_zero_eq,
+    exact metric.ball_mem_nhds 0 (div_pos hr h) },
+  simp_rw [le_antisymm (not_lt.mp h) ((s.sup p).nonneg v), mul_zero, hr],
+  exact is_open.mem_nhds is_open_univ (mem_univ 0),
+end
+
+variables [nonempty ι]
+
+lemma seminorm_basis_zero_smul (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
+  ∃ (V : set 𝕜) (H : V ∈ 𝓝 (0 : 𝕜)) (W : set E)
+  (H : W ∈ (seminorm_add_group_filter_basis p).sets), V • W ⊆ U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  refine ⟨metric.ball 0 r.sqrt, metric.ball_mem_nhds 0 (real.sqrt_pos.mpr hr), _⟩,
+  refine ⟨(s.sup p).ball 0 r.sqrt, seminorm_basis_zero_mem p s (real.sqrt_pos.mpr hr), _⟩,
+  refine set.subset.trans (ball_smul_ball (s.sup p) r.sqrt r.sqrt) _,
+  rw [hU, real.mul_self_sqrt (le_of_lt hr)],
+end
+
+lemma seminorm_basis_zero_smul_left (p : ι → seminorm 𝕜 E) (x : 𝕜) (U : set E)
+  (hU : U ∈ seminorm_basis_zero p) : ∃ (V : set E)
+  (H : V ∈ (seminorm_add_group_filter_basis p).sets), V ⊆ (λ (y : E), x • y) ⁻¹' U :=
+begin
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rw hU,
+  by_cases h : x ≠ 0,
+  { rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero],
+    use (s.sup p).ball 0 (r / ∥x∥),
+    exact ⟨seminorm_basis_zero_mem p s (div_pos hr (norm_pos_iff.mpr h)), subset.rfl⟩ },
+  refine ⟨(s.sup p).ball 0 r, seminorm_basis_zero_mem p s hr, _⟩,
+  simp only [not_ne_iff.mp h, subset_def, mem_ball_zero, hr, mem_univ, seminorm.zero,
+    implies_true_iff, preimage_const_of_mem, zero_smul],
+end
+
+/-- The `module_filter_basis` induced by the filter basis `seminorm_basis_zero`. -/
+def seminorm_module_filter_basis (p : ι → seminorm 𝕜 E) : module_filter_basis 𝕜 E :=
+{ to_add_group_filter_basis := seminorm_add_group_filter_basis p,
+  smul' := seminorm_basis_zero_smul p,
+  smul_left' := seminorm_basis_zero_smul_left p,
+  smul_right' := seminorm_basis_zero_smul_right p }
+
+end filter_basis
+
+section bounded
+
+namespace seminorm
+
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F]
+
+/-- The proposition that a linear map is bounded between spaces with families of seminorms. -/
+def is_bounded (p : ι → seminorm 𝕜 E) (q : ι' → seminorm 𝕜 F) (f : E →ₗ[𝕜] F) : Prop :=
+  ∀ i, ∃ s : finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • s.sup p
+
+lemma is_bounded_const (ι' : Type*) [nonempty ι']
+  {p : ι → seminorm 𝕜 E} {q : seminorm 𝕜 F} (f : E →ₗ[𝕜] F) :
+  is_bounded p (λ _ : ι', q) f ↔ ∃ (s : finset ι) C : ℝ≥0, C ≠ 0 ∧ q.comp f ≤ C • s.sup p :=
+by simp only [is_bounded, forall_const]
+
+lemma const_is_bounded (ι : Type*) [nonempty ι]
+  {p : seminorm 𝕜 E} {q : ι' → seminorm 𝕜 F} (f : E →ₗ[𝕜] F) :
+  is_bounded (λ _ : ι, p) q f ↔ ∀ i, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • p :=
+begin
+  dunfold is_bounded,
+  split,
+  { intros h i,
+    rcases h i with ⟨s, C, hC, h⟩,
+    exact ⟨C, hC, le_trans h (smul_le_smul (finset.sup_le (λ _ _, le_rfl)) le_rfl)⟩ },
+  intros h i,
+  use [{classical.arbitrary ι}],
+  simp only [h, finset.sup_singleton],
+end
+
+lemma is_bounded_sup {p : ι → seminorm 𝕜 E} {q : ι' → seminorm 𝕜 F}
+  {f : E →ₗ[𝕜] F} (hf : is_bounded p q f) (s' : finset ι') :
+  ∃ (C : ℝ≥0) (s : finset ι), 0 < C ∧ (s'.sup q).comp f ≤ C • (s.sup p) :=
+begin
+  classical,
+  by_cases hs' : ¬s'.nonempty,
+  { refine ⟨1, ∅, zero_lt_one, _⟩,
+    rw [finset.not_nonempty_iff_eq_empty.mp hs', finset.sup_empty, seminorm.bot_eq_zero, zero_comp],
+    exact seminorm.nonneg _ },
+  rw not_not at hs',
+  choose fₛ fC hf using hf,
+  use [s'.card • s'.sup fC, finset.bUnion s' fₛ],
+  split,
+  { refine nsmul_pos _ (ne_of_gt (finset.nonempty.card_pos hs')),
+    cases finset.nonempty.bex hs' with j hj,
+    exact lt_of_lt_of_le (zero_lt_iff.mpr (and.elim_left (hf j))) (finset.le_sup hj) },
+  have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • ((finset.bUnion s' fₛ).sup p) :=
+  begin
+    intros i hi,
+    refine le_trans (and.elim_right (hf i)) (smul_le_smul _ (finset.le_sup hi)),
+    exact finset.sup_mono (finset.subset_bUnion_of_mem fₛ hi),
+  end,
+  refine le_trans (comp_mono f (finset_sup_le_sum q s')) _,
+  simp_rw [←pullback_apply, add_monoid_hom.map_sum, pullback_apply], --improve this
+  refine le_trans (finset.sum_le_sum hs) _,
+  rw [finset.sum_const, smul_assoc],
+  exact le_rfl,
+end
+
+end seminorm
+
+end bounded
+
+section topology
+
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι]
+
+/-- The proposition that the topology of `E` is induced by a family of seminorms `p`. -/
+class with_seminorms (p : ι → seminorm 𝕜 E) [t : topological_space E] : Prop :=
+(topology_eq_with_seminorms : t = (seminorm_module_filter_basis p).topology)
+
+lemma with_seminorms_eq (p : ι → seminorm 𝕜 E) [t : topological_space E] [with_seminorms p] :
+  t = ((seminorm_module_filter_basis p).topology) := with_seminorms.topology_eq_with_seminorms
+
+end topology
+
+section topological_add_group
+
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
+variables [topological_space E] [topological_add_group E]
+variables [nonempty ι]
+
+lemma with_seminorms_of_nhds (p : ι → seminorm 𝕜 E)
+  (h : 𝓝 (0 : E) = (seminorm_module_filter_basis p).to_filter_basis.filter) :
+  with_seminorms p :=
+begin
+  refine ⟨topological_add_group.ext (by apply_instance)
+    ((seminorm_add_group_filter_basis _).is_topological_add_group) _⟩,
+  rw add_group_filter_basis.nhds_zero_eq,
+  exact h,
+end
+
+lemma with_seminorms_of_has_basis (p : ι → seminorm 𝕜 E) (h : (𝓝 (0 : E)).has_basis
+  (λ (s : set E), s ∈ (seminorm_basis_zero p)) id) :
+  with_seminorms p :=
+with_seminorms_of_nhds p $ filter.has_basis.eq_of_same_basis h
+  ((seminorm_add_group_filter_basis p).to_filter_basis.has_basis)
+
+end topological_add_group
+
+section normed_space
+
+/-- The topology of a `normed_space 𝕜 E` is induced by the seminorm `norm_seminorm 𝕜 E`. -/
+instance norm_with_seminorms (𝕜 E) [normed_field 𝕜] [semi_normed_group E] [normed_space 𝕜 E] :
+  with_seminorms (λ (_ : fin 1), norm_seminorm 𝕜 E) :=
+begin
+  let p := λ _ : fin 1, norm_seminorm 𝕜 E,
+  refine ⟨topological_add_group.ext normed_top_group
+    ((seminorm_add_group_filter_basis _).is_topological_add_group) _⟩,
+  refine filter.has_basis.eq_of_same_basis metric.nhds_basis_ball _,
+  rw ←ball_norm_seminorm 𝕜 E,
+  refine filter.has_basis.to_has_basis (seminorm_add_group_filter_basis p).nhds_zero_has_basis _
+    (λ r hr, ⟨(norm_seminorm 𝕜 E).ball 0 r, seminorm_basis_zero_singleton_mem p 0 hr, rfl.subset⟩),
+  rintros U (hU : U ∈ seminorm_basis_zero p),
+  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  use [r, hr],
+  rw [hU, id.def],
+  by_cases h : s.nonempty,
+  { rw finset.sup_const h },
+  rw [finset.not_nonempty_iff_eq_empty.mp h, finset.sup_empty, ball_bot _ hr],
+  exact set.subset_univ _,
+end
+
+end normed_space
+
+section continuous_bounded
+
+namespace seminorm
+
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F]
+variables [nonempty ι] [nonempty ι']
+
+lemma continuous_from_bounded (p : ι → seminorm 𝕜 E) (q : ι' → seminorm 𝕜 F)
+  [uniform_space E] [uniform_add_group E] [with_seminorms p]
+  [uniform_space F] [uniform_add_group F] [with_seminorms q]
+  (f : E →ₗ[𝕜] F) (hf : seminorm.is_bounded p q f) : continuous f :=
+begin
+  refine uniform_continuous.continuous _,
+  refine add_monoid_hom.uniform_continuous_of_continuous_at_zero f.to_add_monoid_hom _,
+  rw [f.to_add_monoid_hom_coe, continuous_at_def, f.map_zero, with_seminorms_eq p],
+  intros U hU,
+  rw [with_seminorms_eq q, add_group_filter_basis.nhds_zero_eq, filter_basis.mem_filter_iff] at hU,
+  rcases hU with ⟨V, hV : V ∈ seminorm_basis_zero q, hU⟩,
+  rcases (seminorm_basis_zero_iff q V).mp hV with ⟨s₂, r, hr, hV⟩,
+  rw hV at hU,
+  rw [(seminorm_add_group_filter_basis p).nhds_zero_eq, filter_basis.mem_filter_iff],
+  rcases (seminorm.is_bounded_sup hf s₂) with ⟨C, s₁, hC, hf⟩,
+  refine ⟨(s₁.sup p).ball 0 (r/C),
+    seminorm_basis_zero_mem p _ (div_pos hr (nnreal.coe_pos.mpr hC)), _⟩,
+  refine subset.trans _ (preimage_mono hU),
+  simp_rw [←linear_map.map_zero f, ←ball_comp],
+  refine subset.trans _ (ball_antitone hf),
+  rw ball_smul (s₁.sup p) hC,
+end
+
+lemma cont_with_seminorms_normed_space (F) [semi_normed_group F] [normed_space 𝕜 F]
+  [uniform_space E] [uniform_add_group E]
+  (p : ι → seminorm 𝕜 E) [with_seminorms p] (f : E →ₗ[𝕜] F)
+  (hf : ∃ (s : finset ι) C : ℝ≥0, C ≠ 0 ∧ (norm_seminorm 𝕜 F).comp f ≤ C • s.sup p) :
+  continuous f :=
+begin
+  rw ←seminorm.is_bounded_const (fin 1) at hf,
+  exact continuous_from_bounded p (λ _ : fin 1, norm_seminorm 𝕜 F) f hf,
+end
+
+lemma cont_normed_space_to_with_seminorms (E) [semi_normed_group E] [normed_space 𝕜 E]
+  [uniform_space F] [uniform_add_group F]
+  (q : ι → seminorm 𝕜 F) [with_seminorms q] (f : E →ₗ[𝕜] F)
+  (hf : ∀ i : ι, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • (norm_seminorm 𝕜 E)) : continuous f :=
+begin
+  rw ←seminorm.const_is_bounded (fin 1) at hf,
+  exact continuous_from_bounded (λ _ : fin 1, norm_seminorm 𝕜 E) q f hf,
+end
+
+end seminorm
+
+end continuous_bounded
+
+section locally_convex_space
+
+open locally_convex_space
+
+variables [nonempty ι] [normed_field 𝕜] [normed_space ℝ 𝕜]
+  [add_comm_group E] [module 𝕜 E] [module ℝ E] [is_scalar_tower ℝ 𝕜 E] [topological_space E]
+  [topological_add_group E]
+
+lemma with_seminorms.to_locally_convex_space (p : ι → seminorm 𝕜 E) [with_seminorms p] :
+  locally_convex_space ℝ E :=
+begin
+  apply of_basis_zero ℝ E id (λ s, s ∈ seminorm_basis_zero p),
+  { rw [with_seminorms_eq p, add_group_filter_basis.nhds_eq _, add_group_filter_basis.N_zero],
+    exact filter_basis.has_basis _ },
+  { intros s hs,
+    change s ∈ set.Union _ at hs,
+    simp_rw [set.mem_Union, set.mem_singleton_iff] at hs,
+    rcases hs with ⟨I, r, hr, rfl⟩,
+    exact convex_ball _ _ _ }
+end
+
+end locally_convex_space
+
+section normed_space
+
+variables (𝕜) [normed_field 𝕜] [normed_space ℝ 𝕜] [semi_normed_group E]
+
+/-- Not an instance since `𝕜` can't be inferred. See `normed_space.to_locally_convex_space` for a
+slightly weaker instance version. -/
+lemma normed_space.to_locally_convex_space' [normed_space 𝕜 E] [module ℝ E]
+  [is_scalar_tower ℝ 𝕜 E] : locally_convex_space ℝ E :=
+with_seminorms.to_locally_convex_space (λ _ : fin 1, norm_seminorm 𝕜 E)
+
+/-- See `normed_space.to_locally_convex_space'` for a slightly stronger version which is not an
+instance. -/
+instance normed_space.to_locally_convex_space [normed_space ℝ E] :
+  locally_convex_space ℝ E :=
+normed_space.to_locally_convex_space' ℝ
+
+end normed_space