Physicslib4.Analysis.StrongContinuity

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) ψ

A family of unitaries whose matrix elements are continuous on a dense set of vectors is strongly continuous.

Let U(x), x ∈ X, be unitaries on H indexed by a topological space X, and D a dense subset of H. If x ↦ ⟨ξ, U(x)η⟩ is continuous for all ξ, η ∈ D, then x ↦ U(x)ψ is continuous in norm for every ψ ∈ H. Matrix elements are often all one can compute directly: for the unitaries implementing a symmetry in the GNS representation of an invariant state ω they are ω(a* γ_x(b)) on the dense set of vectors π(a)Ω. This lemma upgrades their continuity to the strong continuity that Stone's theorem requires; this is how GNS.exists_gns_unitary_of_invariant_strongContinuous uses it.

The proof has three steps. Because ‖U(x)η‖ = ‖η‖, approximating ξ by elements of D is uniform in x, so x ↦ ⟨ξ, U(x)η⟩ is continuous for every ξ ∈ H and η ∈ D. For η ∈ D, ‖U(x)η − U(x₀)η‖² = 2‖η‖² − 2 Re⟨U(x₀)η, U(x)η⟩, which tends to 0 as x → x₀. Finally, taking η ∈ D close to ψ, ‖U(x)ψ − U(x)η‖ = ‖ψ − η‖ for every x, so x ↦ U(x)ψ is a uniform limit of continuous maps.

Implementation note: unitaries are H ≃ₗᵢ[ℂ] H, and nothing is assumed about how U depends on x beyond the hypothesis: no group law and no completeness of H. The uniform limits use Mathlib's continuous_of_uniform_approx_of_continuous.

Blueprint: lmm:weak-continuity-implies-strong