Convergence in the weak topology

A family converges in WeakSpace 𝕜 E exactly when its values under every continuous linear functional converge (TauCeti.tendsto_toWeakSpace_iff_forall_eval_tendsto). This lets weak convergence be used without unfolding the definition of WeakSpace as a WeakBilin space. No injectivity of the duality pairing is needed, since the weak topology is induced by the evaluations.

When the weak topology is Hausdorff, weak convergence implies convergence in the original topology for families that eventually stay in a compact set (TauCeti.tendsto_of_tendsto_toWeakSpace_of_isCompact): on a compact set the two topologies agree.

theorem TauCeti.tendsto_toWeakSpace_iff_forall_eval_tendsto {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {α : Type u_3} {l : Filter α} {u : α → E} {x : E} : Filter.Tendsto (fun (n : α) => (toWeakSpace 𝕜 E) (u n)) l (nhds ((toWeakSpace 𝕜 E) x)) ↔ ∀ (f : StrongDual 𝕜 E), Filter.Tendsto (fun (n : α) => f (u n)) l (nhds (f x))

A family converges weakly exactly when its values under every continuous linear functional converge.

theorem TauCeti.tendsto_of_tendsto_toWeakSpace_of_isCompact {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space (WeakSpace 𝕜 E)] {α : Type u_3} {l : Filter α} {K : Set E} (hK : IsCompact K) {u : α → E} (hu : ∀ᶠ (n : α) in l, u n ∈ K) {a : E} (h : Filter.Tendsto (fun (n : α) => (toWeakSpace 𝕜 E) (u n)) l (nhds ((toWeakSpace 𝕜 E) a))) : Filter.Tendsto u l (nhds a)

If the weak topology is Hausdorff, a family that eventually stays in a compact set and converges weakly to a converges to a in the original topology.