convergence in norm/WeakSpace

Stream: new members

[Yoh Tanimoto]

Hello!
I would like to prove that a convergent sequence in normed space is convergent in the weak topology as well. Could someone help me state it in Lean?

I tried Tendsto (fun n ↦ (x n : (WeakSpace 𝕜 E))) atTop (nhds (p : (WeakSpace 𝕜 E))), thinking that I were casting x n to Weakspace 𝕜 E, but actually it remains in E:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

open NormedSpace Filter Set

theorem weak_convergence_of_norm_convergence
 (x : ℕ → E) (p : E) (hx : Tendsto x atTop (nhds p)) :
 Tendsto (fun n ↦ (x n : (WeakSpace 𝕜 E))) atTop (nhds (p : (WeakSpace 𝕜 E))) := by
 exact hx

[Yoh Tanimoto]

Let me ask in a different way.
For a variable p : E, is it possible to take a variable q : WeakSpace 𝕜 E such that p = q?

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

variable (p : E)
variable (q : WeakSpace 𝕜 E)
#check p = q  -- : Prop

[Kalle Kytölä]

I thought the coercions should work as you thought, too, with explicit type ascriptions...

Adding the id-trick, this seems to work:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
variable (p : E)

#check (p : WeakSpace 𝕜 E)   -- p : E -- :(
#check (id p : WeakSpace 𝕜 E)   -- id p : WeakSpace 𝕜 E -- :)

[Eric Wieser]

I think this is the wrong question; you should be asking if there is an equivalence such that p : E but e p : WeakSpace k E

[Eric Wieser]

I would expect to find one right next to docs#WeakSpace

[Eric Wieser]

... though it does look like it's missing

[Eric Wieser]

See docs#WithLp.equiv for an example of what I mean

[Yoh Tanimoto]

OK, so id with explicit type ascription works, thanks!

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]


open NormedSpace Filter Set

theorem norm_topology_le_weak_topology :
 (UniformSpace.toTopologicalSpace : TopologicalSpace E) ≤
  (WeakSpace.instTopologicalSpace : TopologicalSpace (WeakSpace 𝕜 E)) := by
  apply Continuous.le_induced
  refine continuous_pi ?h.h
  intro y
  simp
  have : (fun x => ((topDualPairing 𝕜 E) y) x) = (fun x => y x) := by
   ext x
   exact topDualPairing_apply y x
  rw [this]
  exact ContinuousLinearMap.continuous y

theorem weak_convergence_of_norm_convergence
 (x : ℕ → E) (p : E) (hx : Tendsto x atTop (nhds p)) :
 Tendsto (fun n ↦ (id (x n) : (WeakSpace 𝕜 E))) atTop (nhds (p : (WeakSpace 𝕜 E))) := by
 refine tendsto_atTop_nhds.mpr ?_
 intro U hpU hU
 have hUnorm : IsOpen (id U : Set E) := by
  exact norm_topology_le_weak_topology (id U : Set E) hU
 rw [tendsto_atTop_nhds] at hx
 exact hx (id U : Set E) hpU hUnorm

What is the convention of mathlib for different topologies on the same set?
Should there be a canonical map E → WeakSpace 𝕜 E as you say, or a coercion?
I see the notation IsOpen[s] at docs#TopologicalSpace.le_def but if I just write #check IsOpen[UniformSpace.toTopologicalSpace : TopologicalSpace E], I get an error.

[Yoh Tanimoto]

I made a PR #11472 (from a fork) proving some basic relations between the weak and the original topology. May I have a write access to non-master branches of the mathlib repo?

I am a mathematical physicist, here is my website https://www.mat.uniroma2.it/~tanimoto/
I organized a workshop on Lean in Rome in January https://www.mat.uniroma2.it/butterley/formalisation/

[Riccardo Brasca]

Invitation sent!

[Yoh Tanimoto]

thank you!

[Moritz Doll]

I would guess that we are missing something like this:

def foo : E →L[𝕜] WeakSpace 𝕜 E where
  toFun x := x
  map_add' := sorry
  map_smul' := sorry
  cont := by
    apply WeakBilin.continuous_of_continuous_eval
    exact ContinuousLinearMap.continuous

and the convergence statement should be a very easy consequence of this definition.

[Yoh Tanimoto]

I agree that it would be nice to have such functions! I asked above which was the convention of mathlib for different topologies on a set.

So should there be a canonical map for any combination of two topologies on the same set? Or is there a way to solve this by, say, coercion? I wanted to know this because in von Neumann algebras one puts 7 topologies on B(H)...

[Moritz Doll]

The convention is that we mainly use type synonyms such as WeakSpace k E and then have mappings such as WithLp.equiv or the one I sketched out above to go between the different types

[Yoh Tanimoto]

ok!

[Moritz Doll]

There might be quite a bit of API missing for WeakSpace, as far as I know nobody really used it