Some theorems about weak topology in real Hilbert Space

Stream: mathlib4

[Yifan Bai]

Hi,

Here's Yifan Bai

I have formalized several results about the weak topology on a real Hilbert space H with my collaborator Yantao Li, and we are considering contributing them to mathlib. Our results are mainly based on the existing definitions WeakSpace and WeakDual defined in Mathlib/Topology/Algebra/Module/WeakDual.lean.

Currently we have:
(1) weak convergence defined by

def WeakConverge (x : ℕ → H) (p : H) :=
Tendsto ((toWeakSpace ℝ H) ∘ x) atTop (nhds ((toWeakSpace ℝ H) p))

and we proved its equivalent inner product definition in many text books:

theorem weakConverge_iff_inner_converge [CompleteSpace H] (x : ℕ → H) (p : H) : WeakConverge x p ↔ ∀ y : H, Tendsto (fun n ↦ ⟪x n, y⟫) atTop (nhds ⟪p, y⟫) := by

in finite-dimensional spaces weak convergence ↔ strong convergence:

theorem finite_weak_converge_iff_converge [FiniteDimensional ℝ H] (x : ℕ → H) (p : H) (h : WeakConverge x p) : Tendsto x atTop (nhds p) := by

and some other lemmas about the relationship between weak and strong convergence.
(2) WeakSpace ℝ H is a T2 space.
(3) Closed convex sets are weakly closed, where weakly closed is defined by

def IsWeaklyClosed (s : Set H) := IsClosed ((toWeakSpace ℝ H) '' s)

(4) A homeomorphism between WeakSpace ℝ H and WeakDual ℝ H , based on this I proved a Banach–Alaoglu-style corollary: closedBall x r is weakly compact, with weakly compact defined by

def IsWeaklyCompact (s : Set H) : Prop := IsCompact ((toWeakSpace ℝ H) '' s)

(5) In separable H, every bounded sequence has a weakly convergent subsequence (This is not a general result, so I guess this one is currently not needed in mathlib).

We’re not sure which of these results would be useful for mathlib and worth upstreaming. If contributions are welcome, could you advise:

• where these results should live (which files/directories)?
• whether any of them (or close variants) already exist in mathlib?
  If so, maybe we can start with a small PR focusing on (1), i.e. basic results about weak convergence.

Also, this would be our first time contributing to mathlib, so we may be unfamiliar with the usual contribution workflow—thanks in advance for your patience and guidance.

[Yongxi Lin (Aaron)]

We have more general results: WeakDual.instT2Space, ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image.

(5) should follow from WeakDual.isSeqCompact_closedBall and (3) should follow from Convex.toWeakSpace_closure.

[Yifan Bai]

Yongxi Lin (Aaron) said:

We have more general results: WeakDual.instT2Space, ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image.

(5) should follow from WeakDual.isSeqCompact_closedBall and (3) should follow from Convex.toWeakSpace_closure.

Thank you for your comments :face_holding_back_tears:
While most theorems in mathlib are proved in WeakDual, we mainly focus on the properties in the WeakSpace, since we aim to formalize some weak convergence results of several fix point iteration methods.
For the closed convex theorem (3), thank you for Convex.toWeakSpace_closure, we haven't noticed the theorems in the Locally Convex space, since all the normed space is locally convex, what we proved is exactly this theorem.

For the weak convergence (1), ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto is considered in the WOT topology, which cannot be applied directly in the WeakSpace. I think a theorem in the WeakSpace may be more convenient, and that's what we did. We also proved the relationship between strong and weak convergence in finite (mentioned before) and infinite dimensional space. For infinite dimensional space, we show

theorem strong_converge_iff_weak_norm_converge [CompleteSpace H] (x : ℕ → H) (p : H) : Tendsto x atTop (nhds p) ↔ WeakConverge x p ∧ Tendsto (fun n => ‖x n‖) atTop (nhds ‖p‖) := by

(2) In general, WeakDual over a topological space is T2 which is WeakDual.instT2Space, but WeakSpace is generally not (I think it may hold for normed space?), and we proved this instance in Hilbert space.

(4) and (5), to use WeakDual.isSeqCompact_closedBal proved in the WeakDual, we construct a homeomorphism between WeakDual and WeakSpace so that we can get the WeakSpace version.

Thank you for your patience.

[Yongxi Lin (Aaron)]

Let me just focus on (2) now. I think WeakSpace 𝕜 E is T2 whenever E is locally convex and 𝕜 = ℝ or ℂ because of Hahn Banach theorems (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Separation.html), and you should prove this more general version (instead of proving it just for normed or Hilbert space) if you want to contribute to mathlib. Something like this:

import Mathlib

instance {𝕜 E : Type*} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [RCLike 𝕜] [Module 𝕜 E]
    [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] :
    T2Space (WeakSpace 𝕜 E) := by
  sorry

and I believe this is worth adding to mathlib.

Potentially a more general theorem can be proved. WeakDual.instT2Space is proved for any 𝕜 that is Hausdorff, and we can probably do sth similar for WeakSpace. However, I am not familiar with topological modules over rings other than ℝ or ℂ. Hopefully somebody with more experiences and knowledge than me can notice this post and give you some advice.

[Sébastien Gouëzel]

Deleted -- I didn't see it was WeakSpace and not WeakDual.

[Jireh Loreaux]

@Yifan Bai a few questions:

1. Did you only do this for real Hilbert spaces (not docs#RCLike ones)? Why?
2. For (4) do you have not just the homeomorphism, but the docs#ContinuousLinearEquiv ? This is the thing that sounds most appealing to have in Mathlib from what you mentioned above.

[Yifan Bai]

Yongxi Lin (Aaron) said:

Let me just focus on (2) now. I think WeakSpace 𝕜 E is T2 whenever E is locally convex and 𝕜 = ℝ or ℂ because of Hahn Banach theorems (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Separation.html), and you should prove this more general version (instead of proving it just for normed or Hilbert space) if you want to contribute to mathlib. Something like this:

import Mathlib

instance {𝕜 E : Type*} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [RCLike 𝕜] [Module 𝕜 E]
    [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] :
    T2Space (WeakSpace 𝕜 E) := by
  sorry

and I believe this is worth adding to mathlib.

Potentially a more general theorem can be proved. WeakDual.instT2Space is proved for any 𝕜 that is Hausdorff, and we can probably do sth similar for WeakSpace. However, I am not familiar with topological modules over rings other than ℝ or ℂ. Hopefully somebody with more experience sand knowledge than me can notice this post and give you some advice.

Thank you very much for suggesting this more general statement :saluting_face: . So far we only have a proof for a special case; we’ll try to work towards proving a more general version.

[Yifan Bai]

Jireh Loreaux said:

Yifan Bai a few questions:

1. Did you only do this for real Hilbert spaces (not docs#RCLike ones)? Why?
2. For (4) do you have not just the homeomorphism, but the docs#ContinuousLinearEquiv ? This is the thing that sounds most appealing to have in Mathlib from what you mentioned above.

Thank you for the comments!

1. Yes—so far all of our results are stated for real Hilbert spaces. Our current goal is to formalize the convergence analysis of several algorithms, and for the moment we only need the real case. We’ll look into what can be generalized to more general settings (e.g. IsROrC Hilbert spaces) next.

2. I agree that a ContinuousLinearEquiv statement should also be possible here, not just a homeomorphism. I’ll try to formulate and prove the corresponding docs#ContinuousLinearEquiv version.

Thanks again for the valuable suggestions. :face_holding_back_tears:

[Jireh Loreaux]

I would hope that all your real Hilbert space stuff transfers easily. For future reference, I would start in the more general setting, and only specialize when necessary. This saves you reactoring your code later. (I'm not just saying this for the sake of Mathlib, I mean even for your own use.)

[Yifan Bai]

Jireh Loreaux said:

I would hope that all your real Hilbert space stuff transfers easily. For future reference, I would start in the more general setting, and only specialize when necessary. This saves you reactoring your code later. (I'm not just saying this for the sake of Mathlib, I mean even for your own use.)

Thank you for the suggestion. Our current workflow need some adjustment, and refactoring is indeed quite tedious. In the future I’ll start by considering the more general setting first.