Prove2Me

The induced hermitian contraction semigroup

Open
QAlgorithms.Papers.Independent.Intakethird100.P92.quantized_semigroup

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

prove2quantum

Let (E,E+,θ)(E,E_+,\theta) be reflection positive and let (Ut)t∈R(U_t)_{t\in\mathbb R} be a strongly continuous unitary one-parameter group satisfying UtE+⊆E+U_tE_+\subseteq E_+ for t>0t>0 and θUtθ=U−t\theta U_t\theta=U_{-t}. For each t≥0t\geq0, the canonical quotient extension U^t\widehat U_t exists and is a hermitian contraction. It satisfies

U^tq(v)=q(Utv),U^0=1,U^s+t=U^sU^t,∥U^t∥≤1.\widehat U_tq(v)=q(U_tv),\qquad \widehat U_0=1,\qquad \widehat U_{s+t}=\widehat U_s\widehat U_t,\qquad\|\widehat U_t\|\leq1.

For every x∈E^x\in\widehat E, the map t↦U^txt\mapsto\widehat U_tx is continuous on [0,∞)[0,\infty).

This is the strongly continuous version specified by Definition 3.1; cyclicity is not required. The operators are defined by their continuous extensions from the canonical quotient, not supplied independently.

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 3.2, PDF p. 10: quotient descent produces a strongly continuous
semigroup of hermitian contractions, including the identity at time zero. -/
theorem quantized_semigroup [hHilbert : CompleteSpace E] (r : ReflectionData E) (U : ReflectionGroup r) :
    (∀ t v, quantized r U t (osQ r v) = osQ r (positiveRestriction r U t v)) ∧
    quantized r U 0 = ContinuousLinearMap.id ℂ (OS r) ∧
    (∀ s t, quantized r U (s + t) = (quantized r U s).comp (quantized r U t)) ∧
    (∀ t, ‖quantized r U t‖ ≤ 1 ∧
      ∀ x y, inner ℂ (quantized r U t x) y = inner ℂ x (quantized r U t y)) ∧
    (∀ x, Continuous (fun t : ℝ≥0 => quantized r U t x)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end
Source
Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 10, Proposition 3.2
Read-back

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

Let EE be a complete complex inner product space, and let rr consist of a closed complex linear subspace H+H_+ and a complex linear surjective isometry θ\theta satisfying θ2=I\theta^2=I and Re⁡⟨θv,v⟩≥0\operatorname{Re}\langle\theta v,v\rangle\geq0 for every v∈H+v\in H_+. Let Hr\mathcal H_r be the separated completion of H+H_+ with form [v,w]=⟨θv,w⟩[v,w]=\langle\theta v,w\rangle and seminorm Re⁡⟨θv,v⟩\sqrt{\operatorname{Re}\langle\theta v,v\rangle}, with canonical complex linear map q:H+→Hrq:H_+\to\mathcal H_r. Let UtU_t, t∈Rt\in\mathbb R, be complex linear surjective isometries satisfying U0=IU_0=I, Us+t=UsUtU_{s+t}=U_sU_t, continuity of every orbit, preservation of H+H_+ for every nonnegative time, and θUtθ=U−t\theta U_t\theta=U_{-t}. For each t≥0t\geq0, define QtQ_t as a chosen continuous complex linear operator on Hr\mathcal H_r satisfying Qt(qv)=q(Utv)Q_t(qv)=q(U_tv) for every v∈H+v\in H_+, if one exists, and as the zero operator otherwise. The theorem asserts simultaneously that

Qt(qv)=q(Utv)(t≥0, v∈H+),Q0=I,Qs+t=Qs∘Qt(s,t≥0);Q_t(qv)=q(U_tv)\quad(t\geq0,\ v\in H_+),\qquad Q_0=I,\qquad Q_{s+t}=Q_s\circ Q_t\quad(s,t\geq0);

that for every t≥0t\geq0, ∥Qt∥≤1\|Q_t\|\leq1 and ⟨Qtx,y⟩Hr=⟨x,Qty⟩Hr\langle Q_tx,y\rangle_{\mathcal H_r}=\langle x,Q_ty\rangle_{\mathcal H_r} for all x,y∈Hrx,y\in\mathcal H_r; and that for every x∈Hrx\in\mathcal H_r, the map t↦Qtxt\mapsto Q_tx is continuous on the nonnegative real numbers, including at zero.

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