feat(StrongTopology): generalize ContinuousLinearMap.restrictScalarsL (#15285)

Author: urkud

Mathlib/Algebra/Group/Action/Pi.lean

@@ -28,6 +28,10 @@ namespace Pi
 @[to_additive]
 instance smul' [∀ i, SMul (α i) (β i)] : SMul (∀ i, α i) (∀ i, β i) where smul s x i := s i • x i
 
+@[to_additive]
+lemma smul_def' [∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : s • x = fun i ↦ s i • x i :=
+  rfl
+
 @[to_additive (attr := simp)]
 lemma smul_apply' [∀ i, SMul (α i) (β i)] (s : ∀ i, α i) (x : ∀ i, β i) : (s • x) i = s i • x i :=
   rfl

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -93,9 +93,16 @@ theorem isVonNBounded_union {s t : Set E} :
 theorem IsVonNBounded.union {s₁ s₂ : Set E} (hs₁ : IsVonNBounded 𝕜 s₁) (hs₂ : IsVonNBounded 𝕜 s₂) :
     IsVonNBounded 𝕜 (s₁ ∪ s₂) := isVonNBounded_union.2 ⟨hs₁, hs₂⟩
 
+@[nontriviality]
 theorem IsVonNBounded.of_boundedSpace [BoundedSpace 𝕜] {s : Set E} : IsVonNBounded 𝕜 s := fun _ _ ↦
   .of_boundedSpace
 
+@[nontriviality]
+theorem IsVonNBounded.of_subsingleton [Subsingleton E] {s : Set E} : IsVonNBounded 𝕜 s :=
+  fun U hU ↦ eventually_of_forall fun c ↦ calc
+    s ⊆ univ := subset_univ s
+    _ = c • U := .symm <| Subsingleton.eq_univ_of_nonempty <| (Filter.nonempty_of_mem hU).image _
+
 @[simp]
 theorem isVonNBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set E} :
     IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ i, IsVonNBounded 𝕜 (s i) := by
@@ -237,6 +244,20 @@ theorem isVonNBounded_iff_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [
 
 end sequence
 
+/-- If a set is von Neumann bounded with respect to a smaller field,
+then it is also von Neumann bounded with respect to a larger field.
+See also `Bornology.IsVonNBounded.restrict_scalars` below. -/
+theorem IsVonNBounded.extend_scalars [NontriviallyNormedField 𝕜]
+    {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+    (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝]
+    [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E]
+    {s : Set E} (h : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕝 s := by
+  obtain ⟨ε, hε, hε₀⟩ : ∃ ε : ℕ → 𝕜, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ n in atTop, ε n ≠ 0 := by
+    simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))
+  refine isVonNBounded_of_smul_tendsto_zero (ε := (ε · • 1)) (by simpa) fun x hx ↦ ?_
+  have := h.smul_tendsto_zero (eventually_of_forall hx) hε
+  simpa only [Pi.smul_def', smul_one_smul]
+
 section NormedField
 
 variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
@@ -379,6 +400,31 @@ theorem Filter.Tendsto.isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [
   haveI := comm_topologicalAddGroup_is_uniform (G := E)
   hf.cauchySeq.totallyBounded_range.isVonNBounded 𝕜
 
+variable (𝕜) in
+protected theorem Bornology.IsVonNBounded.restrict_scalars_of_nontrivial
+    [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
+    [Zero E] [TopologicalSpace E]
+    [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
+    (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s := by
+  intro V hV
+  refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_
+  refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_
+  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
+    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
+
+variable (𝕜) in
+protected theorem Bornology.IsVonNBounded.restrict_scalars
+    [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜']
+    [Zero E] [TopologicalSpace E]
+    [SMul 𝕜 E] [MulActionWithZero 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
+    (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s :=
+  match subsingleton_or_nontrivial 𝕜' with
+  | .inl _ =>
+    have : Subsingleton E := MulActionWithZero.subsingleton 𝕜' E
+    IsVonNBounded.of_subsingleton
+  | .inr _ =>
+    h.restrict_scalars_of_nontrivial _
+
 section VonNBornologyEqMetric
 
 namespace NormedSpace

Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean

@@ -413,24 +413,6 @@ theorem restrictScalarsIsometry_toLinearMap :
     (restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toLinearMap = restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜'' :=
   rfl
 
-variable (𝕜'')
-
-
-/-- `ContinuousLinearMap.restrictScalars` as a `ContinuousLinearMap`. -/
-def restrictScalarsL : (E →L[𝕜] Fₗ) →L[𝕜''] E →L[𝕜'] Fₗ :=
-  (restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toContinuousLinearMap
-
-variable {𝕜 E Fₗ 𝕜' 𝕜''}
-
-@[simp]
-theorem coe_restrictScalarsL : (restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'' : (E →L[𝕜] Fₗ) →ₗ[𝕜''] E →L[𝕜'] Fₗ) =
-    restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜'' :=
-  rfl
-
-@[simp]
-theorem coe_restrict_scalarsL' : ⇑(restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = restrictScalars 𝕜' :=
-  rfl
-
 end RestrictScalars
 
 lemma norm_pi_le_of_le {ι : Type*} [Fintype ι]

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -275,6 +275,10 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F
       fun SV => { f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2 } :=
   ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets
 
+theorem uniformEmbedding_toUniformOnFun [UniformSpace F] [UniformAddGroup F] :
+    UniformEmbedding fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f :=
+  UniformConvergenceCLM.uniformEmbedding_coeFn ..
+
 instance uniformContinuousConstSMul
     {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] :
@@ -345,6 +349,66 @@ def toLinearMap₂ (L : E →L[𝕜] F →L[𝕜] G) : E →ₗ[𝕜] F →ₗ[
 
 end BilinearMaps
 
+section RestrictScalars
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {E : Type*} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E]
+  {F : Type*} [AddCommGroup F]
+
+section UniformSpace
+
+variable [UniformSpace F] [UniformAddGroup F] [Module 𝕜 F]
+  (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜]
+  [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F]
+
+theorem uniformEmbedding_restrictScalars :
+    UniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := by
+  rw [← uniformEmbedding_toUniformOnFun.of_comp_iff]
+  convert uniformEmbedding_toUniformOnFun using 4 with s
+  exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩
+
+theorem uniformContinuous_restrictScalars :
+    UniformContinuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
+  (uniformEmbedding_restrictScalars 𝕜').uniformContinuous
+
+end UniformSpace
+
+variable [TopologicalSpace F] [TopologicalAddGroup F] [Module 𝕜 F]
+  (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜]
+  [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F]
+
+theorem embedding_restrictScalars :
+    Embedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
+  letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
+  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+  (uniformEmbedding_restrictScalars _).embedding
+
+@[continuity, fun_prop]
+theorem continuous_restrictScalars :
+    Continuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
+   (embedding_restrictScalars _).continuous
+
+variable (𝕜 E F)
+variable (𝕜'' : Type*) [Ring 𝕜'']
+  [Module 𝕜'' F] [ContinuousConstSMul 𝕜'' F] [SMulCommClass 𝕜 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F]
+
+/-- `ContinuousLinearMap.restrictScalars` as a `ContinuousLinearMap`. -/
+def restrictScalarsL : (E →L[𝕜] F) →L[𝕜''] E →L[𝕜'] F :=
+  .mk <| restrictScalarsₗ 𝕜 E F 𝕜' 𝕜''
+
+variable {𝕜 E F 𝕜' 𝕜''}
+
+@[simp]
+theorem coe_restrictScalarsL : (restrictScalarsL 𝕜 E F 𝕜' 𝕜'' : (E →L[𝕜] F) →ₗ[𝕜''] E →L[𝕜'] F) =
+    restrictScalarsₗ 𝕜 E F 𝕜' 𝕜'' :=
+  rfl
+
+@[simp]
+theorem coe_restrict_scalarsL' : ⇑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = restrictScalars 𝕜' :=
+  rfl
+
+end RestrictScalars
+
 end ContinuousLinearMap
 
 open ContinuousLinearMap
@@ -357,8 +421,8 @@ section Semilinear
 
 variable {𝕜 : Type*} {𝕜₂ : Type*} {𝕜₃ : Type*} {𝕜₄ : Type*} {E : Type*} {F : Type*}
   {G : Type*} {H : Type*} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H]
-  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃]
-  [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H]
+  [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄]
+  [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H]
   [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H]
   [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G]
   [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
@@ -404,7 +468,7 @@ end Semilinear
 section Linear
 
 variable {𝕜 : Type*} {E : Type*} {F : Type*} {G : Type*} {H : Type*} [AddCommGroup E]
-  [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [Module 𝕜 E]
+  [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E]
   [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F]
   [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H]
   [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H]

Mathlib/Topology/Bornology/Absorbs.lean

@@ -244,3 +244,10 @@ lemma Absorbent.zero_mem [NeBot (cobounded G₀)] [AddMonoid E] [DistribMulActio
   absorbs_zero_iff.1 (hs 0)
 
 end GroupWithZero
+
+protected theorem Absorbs.restrict_scalars
+    {M N α : Type*} [Monoid N] [SMul M N] [SMul M α] [MulAction N α]
+    [IsScalarTower M N α] [Bornology M] [Bornology N] {s t : Set α} (h : Absorbs N s t)
+    (hbdd : Tendsto (· • 1 : M → N) (cobounded M) (cobounded N)) :
+    Absorbs M s t :=
+  (hbdd.eventually h).mono <| fun x hx ↦ by rwa [smul_one_smul N x s] at hx