Weak continuity implies strong continuity for a family of unitaries

This file proves the analytic core needed to upgrade weak continuity of an implementing unitary representation to strong continuity. It is the spacetime-agnostic ingredient behind the strong continuity of the GNS unitary U(L) attached to an invariant state: weak continuity of the matrix coefficients on the dense cyclic vectors yields strong continuity of L ↦ U(L)ψ for every vector ψ.

Main result

• Physicslib4.strongContinuous_of_weak: for a family U : X → (H ≃ₗᵢ[ℂ] H) of unitaries indexed by a topological space X, if the matrix coefficients x ↦ ⟪ξ, U x η⟫ are continuous for ξ, η ranging over a dense set D, then x ↦ U x ψ is continuous for every ψ : H.

The proof has three steps, each using only Hilbert-space analysis (no Stone theorem, no unbounded operators):

1. Extend weak continuity to an arbitrary first slot (second slot still in D) by uniform approximation, using ‖U x η‖ = ‖η‖.
2. For η ∈ D, the polarization identity ‖U x η - U x₀ η‖² = 2‖η‖² - 2 Re⟪U x₀ η, U x η⟫ plus step 1 give continuity of x ↦ U x η.
3. For arbitrary ψ, approximate by η ∈ D; since each U x is an isometry, ‖U x ψ - U x η‖ = ‖ψ - η‖ is constant in x, so uniform approximation by the (continuous) maps x ↦ U x η finishes the proof.

theorem Physicslib4.strongContinuous_of_weak {X : Type u_1} [TopologicalSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : X → H ≃ₗᵢ[ℂ] H) {D : Set H} (hD : Dense D) (hweak : ∀ ξ ∈ D, ∀ η ∈ D, Continuous fun (x : X) => inner ℂ ξ ((U x) η)) (ψ : H) : Continuous fun (x : X) => (U x) ψ

Weak continuity implies strong continuity for a family of unitaries.

If U : X → (H ≃ₗᵢ[ℂ] H) has continuous matrix coefficients x ↦ ⟪ξ, U x η⟫ for all ξ, η in a dense set D ⊆ H, then x ↦ U x ψ is continuous for every ψ : H.