Theorem 2.28 — a C-real symmetric operator has equal defect indices

Proved

TeschlQM.SelfAdjoint.defect_indices_eq_of_cReal

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

defect-indicesfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1symmetric-operators

Let $A$ be a symmetric operator on a complex Hilbert space $\mathfrak{H}$ and let $C$ be a conjugation on $\mathfrak{H}$ such that $A$ is $C$ -real, i.e. $C\mathfrak{D}(A) \subseteq \mathfrak{D}(A)$ and $AC\psi = CA\psi$ for $\psi \in \mathfrak{D}(A)$ . Then the defect indices of $A$ are equal:

d_+(A) = d_-(A).

Combined with Theorem 2.26 this shows that $C$ -real symmetric operators, such as real differential operators, always have self-adjoint extensions.

Formalization Note. A conjugation is a conjugate-linear C : H →ₗ⋆[ℂ] H with $C^2 = \mathbb{I}$ and $\langle C\psi, C\varphi\rangle = \langle\varphi,\psi\rangle$ (antiunitary reading of the book's definition). Equality of defect indices is the existence of a unitary from $K_+ = \operatorname{Ran}(A+\mathrm{i})^\perp$ onto $K_- = \operatorname{Ran}(A-\mathrm{i})^\perp$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_SelfAdjoint_defectSpace
import Definitions.Def_TeschlQM_SelfAdjoint_IsCReal

Formal statement

namespace TeschlQM.SelfAdjoint

/-- Teschl, Theorem 2.28 (p. 83): if the symmetric operator `A` is `C`-real for a conjugation
`C`, then its defect indices are equal. -/
theorem defect_indices_eq_of_cReal {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : TeschlQM.Shared.IsSymmetric A) (C : H →ₗ⋆[ℂ] H) (hC : IsConjugation C)
    (hAC : IsCReal A C) :
    HasEqualDefectIndices A := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 83, Theorem 2.28

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $H$ be a complex Hilbert space: a complete complex inner product space. Let $A$ be a partial $\mathbb C$ -linear operator on $H$ . Let $C:H\to H$ be a conjugate-linear map: additive, with $C(a\psi)=\bar a\,C\psi$ . Assume:

$\mathrm{IsSymmetric}(A)$ ;
$\mathrm{IsConjugation}(C)$ ;
$\mathrm{IsCReal}(A,C)$ .

Conclusion: $\mathrm{HasEqualDefectIndices}(A)$ .

All four predicates are imported definitions whose code is not shown here. The statement asserts only that these three hypotheses together imply the conclusion predicate.

Degenerate cases:

If $H=\{0\}$ , the conclusion depends on how the unseen HasEqualDefectIndices treats that case.
If the three hypotheses cannot hold together, the statement is vacuous. The same applies to the case $H=\{0\}$ if they cannot all hold there.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph