feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to TVS (#13468)

Author: urkud

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -359,31 +359,43 @@ end Bornology
 
 section UniformAddGroup
 
-variable (𝕜) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+variable (𝕜) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
 variable [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E]
 
 theorem TotallyBounded.isVonNBounded {s : Set E} (hs : TotallyBounded s) :
     Bornology.IsVonNBounded 𝕜 s := by
-  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
-  intro U hU
-  have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 ((0 : E) + (0 : E))) :=
-    tendsto_add
-  rw [add_zero] at h
-  have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
-  simp_rw [← nhds_prod_eq, id] at h'
-  rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
-  rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
-  refine Absorbs.mono_right ?_ hs
-  rw [ht.absorbs_biUnion]
-  have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
-    h'' <| mk_mem_prod hz1 hz2
-  refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
-  -- TODO: with dot notation, Lean timeouts on the next line. Why?
-  exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
+  if h : ∃ x : 𝕜, 1 < ‖x‖ then
+    letI : NontriviallyNormedField 𝕜 := ⟨h⟩
+    rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
+    intro U hU
+    have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
+      continuous_add.tendsto' _ _ (zero_add _)
+    have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
+    simp_rw [← nhds_prod_eq, id] at h'
+    rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
+    rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
+    refine Absorbs.mono_right ?_ hs
+    rw [ht.absorbs_biUnion]
+    have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
+      h'' <| mk_mem_prod hz1 hz2
+    refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
+    -- TODO: with dot notation, Lean timeouts on the next line. Why?
+    exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
+  else
+    haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
+    exact Bornology.IsVonNBounded.of_boundedSpace
 #align totally_bounded.is_vonN_bounded TotallyBounded.isVonNBounded
 
 end UniformAddGroup
 
+variable (𝕜) in
+theorem Filter.Tendsto.isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+    [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
+    {f : ℕ → E} {x : E} (hf : Tendsto f atTop (𝓝 x)) : Bornology.IsVonNBounded 𝕜 (range f) :=
+  letI := TopologicalAddGroup.toUniformSpace E
+  haveI := comm_topologicalAddGroup_is_uniform (G := E)
+  hf.cauchySeq.totallyBounded_range.isVonNBounded 𝕜
+
 section VonNBornologyEqMetric
 
 namespace NormedSpace

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -1434,82 +1434,6 @@ theorem nnnorm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
   NNReal.eq <| norm_ofSubsingleton_id _ _ _
 #align continuous_multilinear_map.nnnorm_of_subsingleton ContinuousMultilinearMap.nnnorm_ofSubsingleton_id
 
-variable {𝕜 G}
-
-open Topology Filter
-
-/-- If the target space is complete, the space of continuous multilinear maps with its norm is also
-complete. The proof is essentially the same as for the space of continuous linear maps (modulo the
-addition of `Finset.prod` where needed). The duplication could be avoided by deducing the linear
-case from the multilinear case via a currying isomorphism. However, this would mess up imports,
-and it is more satisfactory to have the simplest case as a standalone proof. -/
-instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearMap 𝕜 E G) := by
-  -- We show that every Cauchy sequence converges.
-  refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
-  -- We now expand out the definition of a Cauchy sequence,
-  rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩
-  -- and establish that the evaluation at any point `v : Π i, E i` is Cauchy.
-  have cau : ∀ v, CauchySeq fun n => f n v := by
-    intro v
-    apply cauchySeq_iff_le_tendsto_0.2 ⟨fun n => b n * ∏ i, ‖v i‖, _, _, _⟩
-    · intro n
-      have := b0 n
-      positivity
-    · intro n m N hn hm
-      rw [dist_eq_norm]
-      apply le_trans ((f n - f m).le_opNorm v) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m N hn hm) <| by positivity
-    · simpa using b_lim.mul tendsto_const_nhds
-  -- We assemble the limits points of those Cauchy sequences
-  -- (which exist as `G` is complete)
-  -- into a function which we call `F`.
-  choose F hF using fun v => cauchySeq_tendsto_of_complete (cau v)
-  -- Next, we show that this `F` is multilinear,
-  let Fmult : MultilinearMap 𝕜 E G :=
-    { toFun := F
-      map_add' := fun v i x y => by
-        have A := hF (Function.update v i (x + y))
-        have B := (hF (Function.update v i x)).add (hF (Function.update v i y))
-        simp? at A B says simp only [map_add] at A B
-        exact tendsto_nhds_unique A B
-      map_smul' := fun v i c x => by
-        have A := hF (Function.update v i (c • x))
-        have B := Filter.Tendsto.smul (tendsto_const_nhds (x := c)) (hF (Function.update v i x))
-        simp? at A B says simp only [map_smul] at A B
-        exact tendsto_nhds_unique A B }
-  -- and that `F` has norm at most `(b 0 + ‖f 0‖)`.
-  have Fnorm : ∀ v, ‖F v‖ ≤ (b 0 + ‖f 0‖) * ∏ i, ‖v i‖ := by
-    intro v
-    have A : ∀ n, ‖f n v‖ ≤ (b 0 + ‖f 0‖) * ∏ i, ‖v i‖ := by
-      intro n
-      apply le_trans ((f n).le_opNorm _) _
-      apply mul_le_mul_of_nonneg_right _ <| by positivity
-      calc
-        ‖f n‖ = ‖f n - f 0 + f 0‖ := by
-          congr 1
-          abel
-        _ ≤ ‖f n - f 0‖ + ‖f 0‖ := norm_add_le _ _
-        _ ≤ b 0 + ‖f 0‖ := by
-          apply add_le_add_right
-          simpa [dist_eq_norm] using b_bound n 0 0 (zero_le _) (zero_le _)
-    exact le_of_tendsto (hF v).norm (eventually_of_forall A)
-  -- Thus `F` is continuous, and we propose that as the limit point of our original Cauchy sequence.
-  let Fcont := Fmult.mkContinuous _ Fnorm
-  use Fcont
-  -- Our last task is to establish convergence to `F` in norm.
-  have : ∀ n, ‖f n - Fcont‖ ≤ b n := by
-    intro n
-    apply opNorm_le_bound _ (b0 n) fun v => ?_
-    have A : ∀ᶠ m in atTop, ‖(f n - f m) v‖ ≤ b n * ∏ i, ‖v i‖ := by
-      refine eventually_atTop.2 ⟨n, fun m hm => ?_⟩
-      apply le_trans ((f n - f m).le_opNorm _) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m n le_rfl hm) <| by positivity
-    have B : Tendsto (fun m => ‖(f n - f m) v‖) atTop (𝓝 ‖(f n - Fcont) v‖) :=
-      Tendsto.norm (tendsto_const_nhds.sub (hF v))
-    exact le_of_tendsto B A
-  rw [tendsto_iff_norm_sub_tendsto_zero]
-  exact squeeze_zero (fun n => norm_nonneg _) this b_lim
-
 end ContinuousMultilinearMap
 
 end Norm

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

@@ -14,7 +14,8 @@ on `ContinuousMultilinearMap 𝕜 E F`,
 where `E i` is a family of vector spaces over `𝕜` with topologies
 and `F` is a topological vector space.
 -/
-open Bornology Set
+
+open Bornology Function Set
 open scoped Topology UniformConvergence Filter
 
 namespace ContinuousMultilinearMap
@@ -29,6 +30,22 @@ def toUniformOnFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F)
     (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F :=
   UniformOnFun.ofFun _ f
 
+open UniformOnFun in
+lemma range_toUniformOnFun [DecidableEq ι] [TopologicalSpace F] :
+    range toUniformOnFun =
+      {f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F |
+        Continuous (toFun _ f) ∧
+        (∀ (m : Π i, E i) i x y,
+          toFun _ f (update m i (x + y)) = toFun _ f (update m i x) + toFun _ f (update m i y)) ∧
+        (∀ (m : Π i, E i) i (c : 𝕜) x,
+          toFun _ f (update m i (c • x)) = c • toFun _ f (update m i x))} := by
+  ext f
+  constructor
+  · rintro ⟨f, rfl⟩
+    exact ⟨f.cont, f.map_add, f.map_smul⟩
+  · rintro ⟨hcont, hadd, hsmul⟩
+    exact ⟨⟨⟨f, by intro; convert hadd, by intro; convert hsmul⟩, hcont⟩, rfl⟩
+
 @[simp]
 lemma toUniformOnFun_toFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
     UniformOnFun.toFun _ f.toUniformOnFun = f :=
@@ -76,6 +93,29 @@ instance instUniformContinuousConstSMul {M : Type*}
   haveI := uniformContinuousConstSMul_of_continuousConstSMul M F
   uniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl
 
+variable [∀ i, ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [T2Space F]
+
+open UniformOnFun in
+theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
+    CompleteSpace (ContinuousMultilinearMap 𝕜 E F) := by
+  classical
+  have H : ∀ {m : Π i, E i},
+      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
+    (uniformContinuous_eval (isVonNBounded_covers) _).continuous
+  rw [completeSpace_iff_isComplete_range uniformEmbedding_toUniformOnFun.toUniformInducing,
+    range_toUniformOnFun]
+  simp only [setOf_and, setOf_forall]
+  apply_rules [IsClosed.isComplete, IsClosed.inter]
+  · exact UniformOnFun.isClosed_setOf_continuous h
+  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
+      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
+  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
+      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)
+
+instance instCompleteSpace [∀ i, TopologicalAddGroup (E i)] [SequentialSpace (Π i, E i)] :
+    CompleteSpace (ContinuousMultilinearMap 𝕜 E F) :=
+  completeSpace <| .of_seq fun _u x hux ↦ (hux.isVonNBounded_range 𝕜).insert x
+
 end UniformAddGroup
 
 variable [TopologicalSpace F] [TopologicalAddGroup F]

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -861,6 +861,10 @@ theorem uniformContinuous_eval_of_mem_sUnion {x : α} (hx : x ∈ ⋃₀ 𝔖) :
 
 variable {β} {𝔖}
 
+theorem uniformContinuous_eval (h : ⋃₀ 𝔖 = univ) (x : α) :
+    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
+  uniformContinuous_eval_of_mem_sUnion _ _ <| h.symm ▸ mem_univ _
+
 /-- If `u` is a family of uniform structures on `γ`, then
 `𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)`. -/
 protected theorem iInf_eq {u : ι → UniformSpace γ} :
@@ -990,9 +994,7 @@ that of pointwise convergence. -/
 protected theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) :
     UniformContinuous (toFun 𝔖 : (α →ᵤ[𝔖] β) → α → β) := by
   rw [uniformContinuous_pi]
-  intro x
-  obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := sUnion_eq_univ_iff.mp h x
-  exact uniformContinuous_eval_of_mem β 𝔖 hxs hs
+  exact uniformContinuous_eval h
 #align uniform_on_fun.uniform_continuous_to_fun UniformOnFun.uniformContinuous_toFun
 
 /-- Convergence in the topology of `𝔖`-convergence means uniform convergence on `S` (in the sense