A commuting group action descends to a continuous unitary representation

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.commuting_group_quantization

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $(E,E_+,\theta)$ be a reflection-positive complex Hilbert space and let $U$ be a strongly continuous unitary representation of a topological group $G$ on $E$ . Assume $U(g)E_+\subseteq E_+$ and $U(g)\theta=\theta U(g)$ for every $g\in G$ . There is a strongly continuous unitary representation $\widehat U$ on the canonical OS space such that

\widehat U(g)q(v)=q(U(g)v)\quad(g\in G,\ v\in E_+).

The induced operators satisfy the identity and multiplication laws. This is the OS quantization of the given representation, characterized on the dense canonical quotient image.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P92

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P92

open scoped ComplexConjugate BigOperators NNReal ENNReal

open MeasureTheory

attribute [local instance] Classical.propDecidable

universe u v

variable (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {E}

/-- Proposition 2.5, PDF p. 9, for an arbitrary topological group. The induced
unitary representation is required to agree with the canonical quotient on every
input, so it is the OS representation, rather than an unrelated representation. -/
theorem commuting_group_quantization [hHilbert : CompleteSpace E] (r : ReflectionData E)
    (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : G → E ≃ₗᵢ[ℂ] E)
    (hOne : ∀ x, U 1 x = x)
    (hMul : ∀ g h x, U (g * h) x = U g (U h x))
    (hContinuous : ∀ x, Continuous (fun g => U g x))
    (hPlus : ∀ g, ∀ x ∈ r.plus, U g x ∈ r.plus)
    (hTheta : ∀ g x, U g (r.theta x) = r.theta (U g x)) :
    ∃ V : G → OS r ≃ₗᵢ[ℂ] OS r,
      (∀ x, V 1 x = x) ∧
      (∀ g h x, V (g * h) x = V g (V h x)) ∧
      (∀ x, Continuous (fun g => V g x)) ∧
      (∀ g v, V g (osQ r v) = osQ r ⟨U g v, hPlus g v v.property⟩) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 9, Proposition 2.5

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $E$ be a complete complex inner product space, and let $r$ consist of a closed complex linear subspace $H_+$ and a complex linear surjective isometry $\theta$ satisfying $\theta^2=I$ and $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for all $v\in H_+$ . Let $\mathcal H_r$ be the separated completion of $H_+$ with form $[v,w]=\langle\theta v,w\rangle$ and seminorm $\sqrt{\operatorname{Re}\langle\theta v,v\rangle}$ , with canonical complex linear map $q:H_+\to\mathcal H_r$ . Let $G$ be any group equipped with a topology making it a topological group, and let $g\mapsto U_g$ assign a complex linear surjective isometry of $E$ to every $g\in G$ . Assume $U_1x=x$ and $U_{gh}x=U_g(U_hx)$ for all $g,h\in G$ and $x\in E$ ; assume $g\mapsto U_gx$ is continuous for each $x\in E$ ; assume $U_gx\in H_+$ for every $g\in G$ and $x\in H_+$ ; and assume $U_g(\theta x)=\theta(U_gx)$ for every $g\in G$ and $x\in E$ . Then there exists an assignment $g\mapsto V_g$ of complex linear surjective isometries of $\mathcal H_r$ such that $V_1a=a$ and $V_{gh}a=V_g(V_ha)$ for all $g,h\in G$ and $a\in\mathcal H_r$ , the map $g\mapsto V_ga$ is continuous for every $a\in\mathcal H_r$ , and $V_g(qv)=q(U_gv)$ for every $g\in G$ and $v\in H_+$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph