[Merged by Bors] - feat(Analysis/LocallyConvex/WithSeminorms): characterize continuous seminorms

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -51,7 +51,7 @@ seminorm, locally convex
 -/
 
 
-open NormedField Set Seminorm TopologicalSpace
+open NormedField Set Seminorm TopologicalSpace Filter
 
 open BigOperators NNReal Pointwise Topology
 
@@ -584,7 +584,8 @@ set_option linter.uppercaseLean3 false in
 
 end NontriviallyNormedField
 
-section ContinuousBounded
+-- TODO: the names in this section are not very predictable
+section continuous_of_bounded
 
 namespace Seminorm
 
@@ -660,7 +661,73 @@ theorem cont_normedSpace_to_withSeminorms (E) [SeminormedAddCommGroup E] [Normed
 
 end Seminorm
 
-end ContinuousBounded
+end continuous_of_bounded
+
+section bounded_of_continuous
+
+namespace Seminorm
+
+variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+  [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {p : SeminormFamily 𝕜 E ι}
+
+/-- In a semi-`NormedSpace`, a continuous seminorm is zero on elements of norm `0`. -/
+lemma map_eq_zero_of_norm_zero (q : Seminorm 𝕜 F)
+    (hq : Continuous q) {x : F} (hx : ‖x‖ = 0) : q x = 0 :=
+  (map_zero q) ▸
+    ((specializes_iff_mem_closure.mpr $ mem_closure_zero_iff_norm.mpr hx).map hq).eq.symm
+
+/-- Let `F` be a semi-`NormedSpace` over a `NontriviallyNormedField`, and let `q` be a
+seminorm on `F`. If `q` is continuous, then it is uniformly controlled by the norm, that is there
+is some `C > 0` such that `∀ x, q x ≤ C * ‖x‖`.
+The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
+norm is then used to rescale any element into an element of norm in `[ε/C, ε[`, thus with a
+controlled image by `q`. The control of `q` at the original element follows by rescaling. -/
+lemma bound_of_continuous_normedSpace (q : Seminorm 𝕜 F)
+    (hq : Continuous q) : ∃ C, 0 < C ∧ (∀ x : F, q x ≤ C * ‖x‖) := by
+  have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
+  rcases NormedAddCommGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' $ Iio_mem_nhds one_pos)
+    with ⟨ε, ε_pos, hε⟩
+  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
+  have : 0 < ‖c‖ / ε := by positivity
+  refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
+  by_cases hx : ‖x‖ = 0
+  . rw [hx, mul_zero]
+    exact le_of_eq (map_eq_zero_of_norm_zero q hq hx)
+  . refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
+    refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
+    rwa [← div_le_iff' this, one_div_div]
+
+/-- Let `E` be a topological vector space (over a `NontriviallyNormedField`) whose topology is
+generated by some family of seminorms `p`, and let `q` be a seminorm on `E`. If `q` is continuous,
+then it is uniformly controlled by *finitely many* seminorms of `p`, that is there
+is some finset `s` of the index set and some `C > 0` such that `q ≤ C • s.sup p`. -/
+lemma bound_of_continuous [Nonempty ι] [t : TopologicalSpace E] (hp : WithSeminorms p)
+    (q : Seminorm 𝕜 E) (hq : Continuous q) :
+    ∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p := by
+  -- The continuity of `q` gives us a finset `s` and a real `ε > 0`
+  -- such that `hε : (s.sup p).ball 0 ε ⊆ q.ball 0 1`.
+  rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩
+  rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩
+  -- Now forget that `E` already had a topology and view it as the (semi)normed space
+  -- `(E, s.sup p)`.
+  clear hp hq t
+  letI : SeminormedAddCommGroup E :=
+    (s.sup p).toAddGroupSeminorm.toSeminormedAddCommGroup
+  letI : NormedSpace 𝕜 E := { norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }
+  -- The inclusion `hε` tells us exactly that `q` is *still* continuous for this new topology
+  have : Continuous q :=
+    Seminorm.continuous one_pos (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) hε)
+  -- Hence we can conclude by applying `bound_of_continuous_normed_space`.
+  rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩
+  exact ⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩
+  -- Note that the key ingredient for this proof is that, by scaling arguments hidden in
+  -- `seminorm.continuous`, we only have to look at the `q`-ball of radius one, and the `s` we get
+  -- from that will automatically work for all other radii.
+
+end Seminorm
+
+end bounded_of_continuous
 
 section LocallyConvexSpace
 

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -260,44 +260,6 @@ instance Submodule.normedSpace {𝕜 R : Type _} [SMul 𝕜 R] [NormedField 𝕜
     (s : Submodule R E) : NormedSpace 𝕜 s where norm_smul_le c x := norm_smul_le c (x : E)
 #align submodule.normed_space Submodule.normedSpace
 
-/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
-moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
-the rescaling element that shows up in applications. -/
-theorem rescale_to_shell_semi_normed_zpow {c : α} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E}
-    (hx : ‖x‖ ≠ 0) :
-    ∃ n : ℤ, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ := by
-  have xεpos : 0 < ‖x‖ / ε := div_pos ((Ne.symm hx).le_iff_lt.1 (norm_nonneg x)) εpos
-  rcases exists_mem_Ico_zpow xεpos hc with ⟨n, hn⟩
-  have cpos : 0 < ‖c‖ := lt_trans (zero_lt_one : (0 : ℝ) < 1) hc
-  have cnpos : 0 < ‖c ^ (n + 1)‖ := by
-    rw [norm_zpow]
-    exact lt_trans xεpos hn.2
-  refine' ⟨-(n + 1), _, _, _, _⟩
-  show c ^ (-(n + 1)) ≠ 0; exact zpow_ne_zero _ (norm_pos_iff.1 cpos)
-  show ‖c ^ (-(n + 1)) • x‖ < ε
-  · rw [norm_smul, zpow_neg, norm_inv, ← _root_.div_eq_inv_mul, div_lt_iff cnpos, mul_comm,
-      norm_zpow]
-    exact (div_lt_iff εpos).1 hn.2
-  show ε / ‖c‖ ≤ ‖c ^ (-(n + 1)) • x‖
-  · rw [zpow_neg, div_le_iff cpos, norm_smul, norm_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos),
-      zpow_one, mul_inv_rev, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel (ne_of_gt cpos),
-      one_mul, ← _root_.div_eq_inv_mul, le_div_iff (zpow_pos_of_pos cpos _), mul_comm]
-    exact (le_div_iff εpos).1 hn.1
-  show ‖c ^ (-(n + 1))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
-  · rw [zpow_neg, norm_inv, inv_inv, norm_zpow, zpow_add₀ cpos.ne', zpow_one, mul_right_comm, ←
-      _root_.div_eq_inv_mul]
-    exact mul_le_mul_of_nonneg_right hn.1 (norm_nonneg _)
-#align rescale_to_shell_semi_normed_zpow rescale_to_shell_semi_normed_zpow
-
-/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
-moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
-the rescaling element that shows up in applications. -/
-theorem rescale_to_shell_semi_normed {c : α} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E}
-    (hx : ‖x‖ ≠ 0) : ∃ d : α, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ :=
-  let ⟨_, hn⟩ := rescale_to_shell_semi_normed_zpow hc εpos hx
-  ⟨_, hn⟩
-#align rescale_to_shell_semi_normed rescale_to_shell_semi_normed
-
 end SeminormedAddCommGroup
 
 /-- A linear map from a `Module` to a `NormedSpace` induces a `NormedSpace` structure on the
@@ -404,19 +366,6 @@ theorem frontier_sphere' [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) :
   rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
 #align frontier_sphere' frontier_sphere'
 
-theorem rescale_to_shell_zpow {c : α} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
-    ∃ n : ℤ, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ :=
-  rescale_to_shell_semi_normed_zpow hc εpos (mt norm_eq_zero.1 hx)
-#align rescale_to_shell_zpow rescale_to_shell_zpow
-
-/-- If there is a scalar `c` with `‖c‖>1`, then any element can be moved by scalar multiplication to
-any shell of width `‖c‖`. Also recap information on the norm of the rescaling element that shows
-up in applications. -/
-theorem rescale_to_shell {c : α} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
-    ∃ d : α, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ :=
-  rescale_to_shell_semi_normed hc εpos (mt norm_eq_zero.1 hx)
-#align rescale_to_shell rescale_to_shell
-
 end NormedAddCommGroup
 
 section NontriviallyNormedSpace

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -12,6 +12,7 @@ import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
 import Mathlib.Analysis.NormedSpace.LinearIsometry
+import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Topology.Algebra.Module.StrongTopology
 
 /-!
@@ -51,13 +52,8 @@ variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [Nontr
 /-- If `‖x‖ = 0` and `f` is continuous then `‖f x‖ = 0`. -/
 theorem norm_image_of_norm_zero [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous f) {x : E}
     (hx : ‖x‖ = 0) : ‖f x‖ = 0 := by
-  refine' le_antisymm (le_of_forall_pos_le_add fun ε hε => _) (norm_nonneg (f x))
-  rcases NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) ε hε with ⟨δ, δ_pos, hδ⟩
-  replace hδ := hδ x
-  rw [sub_zero, hx] at hδ
-  replace hδ := le_of_lt (hδ δ_pos)
-  rw [map_zero, sub_zero] at hδ
-  rwa [zero_add]
+  rw [← mem_closure_zero_iff_norm, ← specializes_iff_mem_closure, ← map_zero f] at *
+  exact hx.map hf
 #align norm_image_of_norm_zero norm_image_of_norm_zero
 
 section
@@ -67,29 +63,19 @@ variable [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃]
 theorem SemilinearMapClass.bound_of_shell_semi_normed [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕)
     {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
     (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) {x : E} (hx : ‖x‖ ≠ 0) :
-    ‖f x‖ ≤ C * ‖x‖ := by
-  rcases rescale_to_shell_semi_normed hc ε_pos hx with ⟨δ, hδ, δxle, leδx, _⟩
-  simpa only [map_smulₛₗ, norm_smul, mul_left_comm C, mul_le_mul_left (norm_pos_iff.2 hδ),
-    RingHomIsometric.is_iso] using hf (δ • x) leδx δxle
+    ‖f x‖ ≤ C * ‖x‖ :=
+  (normSeminorm 𝕜 E).bound_of_shell ((normSeminorm 𝕜₂ F).comp ⟨⟨f, map_add f⟩, map_smulₛₗ f⟩)
+    ε_pos hc hf hx
 #align semilinear_map_class.bound_of_shell_semi_normed SemilinearMapClass.bound_of_shell_semi_normed
 
 /-- A continuous linear map between seminormed spaces is bounded when the field is nontrivially
 normed. The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
 norm is then used to rescale any element into an element of norm in `[ε/C, ε]`, whose image has a
 controlled norm. The norm control for the original element follows by rescaling. -/
 theorem SemilinearMapClass.bound_of_continuous [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕)
-    (hf : Continuous f) : ∃ C, 0 < C ∧ ∀ x : E, ‖f x‖ ≤ C * ‖x‖ := by
-  rcases NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one with ⟨ε, ε_pos, hε⟩
-  simp only [sub_zero, map_zero] at hε
-  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-  have : 0 < ‖c‖ / ε := div_pos (zero_lt_one.trans hc) ε_pos
-  refine' ⟨‖c‖ / ε, this, fun x => _⟩
-  by_cases hx : ‖x‖ = 0
-  · rw [hx, MulZeroClass.mul_zero]
-    exact le_of_eq (norm_image_of_norm_zero f hf hx)
-  refine' SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc (fun x hle hlt => _) hx
-  refine' (hε _ hlt).le.trans _
-  rwa [← div_le_iff' this, one_div_div]
+    (hf : Continuous f) : ∃ C, 0 < C ∧ ∀ x : E, ‖f x‖ ≤ C * ‖x‖ :=
+  let φ : E →ₛₗ[σ₁₂] F := ⟨⟨f, map_add f⟩, map_smulₛₗ f⟩
+  ((normSeminorm 𝕜₂ F).comp φ).bound_of_continuous_normedSpace (continuous_norm.comp hf)
 #align semilinear_map_class.bound_of_continuous SemilinearMapClass.bound_of_continuous
 
 end

Mathlib/Analysis/NormedSpace/RieszLemma.lean

@@ -9,6 +9,7 @@ Authors: Jean Lo, Yury Kudryashov
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.NormedSpace.Basic
+import Mathlib.Analysis.Seminorm
 import Mathlib.Topology.MetricSpace.HausdorffDistance
 
 /-!