OS descent and adjoint compatibility for densely defined operators

Proved

QAlgorithms.Papers.Independent.Intakethird100.P92.operator_descent

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

prove2quantum

Let $(E,E_+,\theta)$ be a reflection-positive complex Hilbert space with canonical quotient $q:E_+\to\widehat E$ . Let $D\subseteq E_+$ be a linear subspace with $q(D)$ dense in $\widehat E$ . Suppose $T,U:D\to E_+$ are linear and satisfy

\langle\theta Tv,w\rangle=\langle\theta v,Uw\rangle\quad(v,w\in D).

Both maps preserve $N\cap D$ , where $N=\ker q$ , and induce linear operators $\widehat T,\widehat U$ on the common domain $q(D)$ with $\widehat T(qv)=q(Tv)$ and $\widehat U(qv)=q(Uv)$ . They satisfy $\widehat U\subseteq\widehat T^*$ , equivalently the adjoint pairing identity on this dense domain. If $T=U$ , then $\widehat T$ is symmetric. If additionally $D=E_+$ and $T$ is bounded, its induced operator has a continuous extension to $\widehat E$ satisfying $\|\widehat T\|\leq\|T\|$ .

This result supplies descent, symmetry, and the norm estimate; none of them is assumed as input.

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}

/-- Lemma 2.2, PDF pp. 8--9, all four clauses. The adjoint inclusion is stated
by its defining pairing identity on the dense common domain q(D), so it does not
incorrectly treat unbounded adjoints as everywhere-defined bounded operators.
The printed Eplus domain in (i) is D, as explicitly used in equation (5). -/
theorem operator_descent [hHilbert : CompleteSpace E] (r : ReflectionData E) (D : Submodule ℂ r.plus)
    (hDense : Dense ((D.map (osQ r) : Submodule ℂ (OS r)) : Set (OS r)))
    (T U : D →ₗ[ℂ] r.plus)
    (hPair : ∀ v w : D,
      inner ℂ (r.theta (T v : E)) (w : E) =
        inner ℂ (r.theta (v : E)) (U w : E)) :
    (∀ v : D, osQ r v = 0 → osQ r (T v) = 0 ∧ osQ r (U v) = 0) ∧
    ∃ Tq Uq : D.map (osQ r) →ₗ[ℂ] OS r,
      (∀ v, Tq (domainQ r D v) = osQ r (T v)) ∧
      (∀ v, Uq (domainQ r D v) = osQ r (U v)) ∧
      (∀ v w : D.map (osQ r),
        inner ℂ (Tq v) (w : OS r) = inner ℂ (v : OS r) (Uq w)) ∧
      (T = U → ∀ v w : D.map (osQ r),
        inner ℂ (Tq v) (w : OS r) = inner ℂ (v : OS r) (Tq w)) ∧
      (∀ B : r.plus →L[ℂ] r.plus, (∀ v : D, B v = T v) → D = ⊤ → T = U →
        (∀ v : r.plus, osExtension r B.toLinearMap (osQ r v) = osQ r (B v)) ∧
        (∀ v : D.map (osQ r), osExtension r B.toLinearMap v = Tq v) ∧
        ‖osExtension r B.toLinearMap‖ ≤ ‖B‖) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 8, Lemma 2.2

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_+$ for the form $[v,w]=\langle\theta v,w\rangle$ and seminorm $\sqrt{\operatorname{Re}\langle\theta v,v\rangle}$ , and let $q:H_+\to\mathcal H_r$ be its canonical complex linear map. Let $D$ be a complex linear subspace of $H_+$ such that its image $q(D)$ is dense in $\mathcal H_r$ , and let $T,U:D\to H_+$ be complex linear maps satisfying

\langle\theta(Tv),w\rangle=\langle\theta v,Uw\rangle \quad\text{for every }v,w\in D.

Then every $v\in D$ with $q(v)=0$ satisfies both $q(Tv)=0$ and $q(Uv)=0$ , and there exist complex linear maps $T_q,U_q:q(D)\to\mathcal H_r$ such that, for every $v\in D$ , $T_q(q(v))=q(Tv)$ and $U_q(q(v))=q(Uv)$ , where $q(v)$ is regarded as an element of $q(D)$ ; for every $a,b\in q(D)$ ,

\langle T_qa,b\rangle_{\mathcal H_r} =\langle a,U_qb\rangle_{\mathcal H_r};

and if $T=U$ , then $\langle T_qa,b\rangle_{\mathcal H_r}=\langle a,T_qb\rangle_{\mathcal H_r}$ for all $a,b\in q(D)$ . These same chosen maps also satisfy the following conditional statement: for every continuous complex linear map $B:H_+\to H_+$ , if $Bv=Tv$ for every $v\in D$ , $D=H_+$ , and $T=U$ , then

\mathcal E_B(qv)=q(Bv)\quad(v\in H_+),\qquad \mathcal E_B(a)=T_q(a)\quad(a\in q(D)),\qquad \|\mathcal E_B\|\leq\|B\|.

Here $H_+$ carries its norm inherited from $E$ when defining $\|B\|$ , and $\mathcal E_B$ means a chosen continuous complex linear operator on $\mathcal H_r$ satisfying $\mathcal E_B(qv)=q(Bv)$ for all $v\in H_+$ , if any such operator exists, and the zero operator otherwise.

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