§10.3 Unbounded Spectral Theorems (pp. 156–236)

123 declarations (items 164–288, together with Conventions 213 and 260), extending §10.2 to the Spectral Theorem for Unbounded, Self-Adjoint Operators (Theorem 285) and the functional calculus it supplies. The blueprint motivates this with the few genuinely unbounded self-adjoint operators that arise in AQFT, the momentum operator being the standard example. The section reuses §10.2 without restating it, follows the same Hall presentation, and builds up unbounded operators from scratch. Its single subsection, §10.3.1 Spectral Theorem: Unbounded Self-Adjoint Operators (p. 156), proceeds in six stages.

Unbounded operators (pp. 157–181, items 164–212). Unbounded operators (Definition 164), their adjoints (Definition 168, Propositions 169–170, Lemma 171), symmetric operators, extensions and self-adjointness (Definitions 172–173 and 175, Proposition 174), positive operators, with positivity agreeing with the bounded notion (Definition 176, Lemma 177), and closed and closable operators via the graph in \(\mathbf{H} \times \mathbf{H}\) (Definitions 178 and 181, Proposition 182), with the closure of a symmetric operator symmetric (Lemma 183) and essential self-adjointness defined (Definition 184). Elementary properties follow: symmetric operators are closable (Proposition 186), the adjoint of a closure (Proposition 187), uniqueness of the self-adjoint extension of an essentially self-adjoint operator (Proposition 190), and kernel and range, with the orthogonal complement of the range equal to the kernel of the adjoint (Definitions 191–192, Proposition 195). Next come the resolvent set and spectrum of an unbounded operator (Definition 199), which agree with the bounded notions (Lemma 201) and are real for self-adjoint operators (Theorem 203). The layer closes with criteria for essential self-adjointness: dense range (Theorem 204), and, through Hilbert direct sums and internal orthogonal decompositions (Definitions 205, 207 and 208, Lemmas 206 and 210), direct sums of bounded self-adjoint operators (Propositions 211–212).
Integration against a projection-valued measure (p. 182, items 213–240). Under standing hypotheses (Convention 213), and with sesquilinear and quadratic forms on subspaces (Definitions 216–217) and the needed measure theory (Theorems 220–221, Propositions 222–226, Definition 224), the integral of an unbounded measurable function against a projection-valued measure is constructed on its natural domain (Propositions 232 and 234). It coincides with the bounded integral of §10.2 (Proposition 235), ignores null sets (Lemma 236), is the limit of its truncations (Lemma 237), and is self-adjoint for real-valued functions (Proposition 240).
Bounded normal operators (p. 201, items 241–259). For normal operators (Definition 241) the norm equals the spectral radius (Proposition 246). Spectral subspaces (Definition 247, Propositions 248–249) and almost eigenvectors (Definition 251, Lemmas 250 and 252–256) lead to the two-variable spectral mapping theorem for polynomials in \(A\) and \(A^*\) (Theorem 257, Corollary 258), and hence to the continuous functional calculus for a normal operator (Theorem 259). Lemma 253 is stated with a constant uniform over all eigenvalues \(\lvert \lambda \rvert \le R\), which is what the proof of Theorem 257 consumes; the Lean proof of Theorem 257 itself takes a shorter route through Mathlib’s continuous functional calculus (cfc_map_spectrum), as a formalization note in the blueprint records, while the almost-eigenvector lemmas are formalised in their own right.
From a continuous functional calculus to a projection-valued measure (p. 215, items 260–274). Under standing hypotheses (Convention 260), an abstract continuous functional calculus (Definition 261) is extended, through its associated measures (Definition 263), to bounded measurable functions (Definition 266). The extension is linear, multiplicative and compatible with conjugation (Lemmas 267 and 271, Proposition 270), and it yields a projection-valued measure (Theorem 272). Combined with the previous stage, this gives the Spectral Theorem for Bounded Normal Operators (Theorem 274).
The Cayley transform and the unbounded spectral theorem (pp. 223–232, items 275–285). Unitary operators are normal, with spectrum on the unit circle (Lemmas 275–276). The Cayley map (Lemma 277) and the Cayley transform of a self-adjoint operator (Theorem 278), with its spectral mapping (Lemma 279), reduce the unbounded self-adjoint case to the bounded normal one: a projection-valued measure is transported along a Borel bijection (Lemma 281), the Cayley transform omits the point \(1\) (Lemma 282), and the spectral measure is transported through the Cayley transform (Theorem 284). The result is the Spectral Theorem for Unbounded, Self-Adjoint Operators (Theorem 285).
The functional calculus of an unbounded self-adjoint operator (p. 235, items 286–288). These items supply what §10.4 needs. The spectral measure of a self-adjoint operator is named (Definition 286), the functional calculus \(f(A)\) is the integral of \(f\) against it (Definition 287), and for bounded \(f\) it agrees with the bounded calculus of §10.2 (Lemma 288). Earlier in the section, a self-adjoint operator is shown to have no proper symmetric extension (Lemma 189), which §10.4 uses to identify the generator of \(e^{itA}\) with \(A\).

Where the Lean lives: Physicslib4/Spectral/Unbounded/ (Basic, Spectrum, DirectSum, Integral, Normal, AbstractCalculus, Cayley, FunctionalCalculus)

Items

Each blueprint subsection below is collapsed; click a heading to see its items. Every entry links to its node in the web blueprint and names the principal Lean declaration.

§10.3.1 · Unbounded Operators › Adjoint and Closure of an Unbounded Operator (p. 157) — 21 items

Definition 164 — Unbounded Operator · LinearPMap (+1 more)
Proposition 165 — Convergence Facts for Sequences and Series · tendsto_atTop_ciSup (+6 more)
Lemma 166 — Equality Testing on a Dense Subspace, First Slot · Dense.eq_of_inner_left
Lemma 167 — Equality Testing on a Dense Subspace, Second Slot · Dense.eq_of_inner_right
Definition 168 — Adjoint of an Unbounded Operator · LinearPMap.adjointDomain (+3 more)
Proposition 169 — The Adjoint is Well Defined · Physicslib4.Spectral.Unbounded.existsUnique_adjoint_apply
Proposition 170 — Linearity of the Adjoint · Physicslib4.Spectral.Unbounded.smul_add_mem_adjoint_domain (+1 more)
Lemma 171 — Characterizing Membership in the Adjoint’s Domain · Physicslib4.Spectral.Unbounded.mem_adjoint_domain_iff_exists (+1 more)
Definition 172 — Symmetric Operator · Physicslib4.Spectral.Unbounded.IsSymmetric (+1 more)
Definition 173 — Extension of an Operator · LinearPMap.le (+2 more)
Proposition 174 — Symmetric Operators and the Adjoint · Physicslib4.Spectral.Unbounded.isSymmetric_iff_le_adjoint
Definition 175 — Self-Adjoint Operator · LinearPMap.instStar (+1 more)
Definition 176 — Positive Operator · Physicslib4.Spectral.Unbounded.IsPositive
Lemma 177 — Positivity of a Bounded Operator · Physicslib4.Spectral.Unbounded.isPositive_toPMap_iff
Definition 178 — The Product Hilbert Space \(\mathbf{H} \times \mathbf{H}\) · WithLp.instProdInnerProductSpace (+2 more)
Theorem 179 — Sequential Characterization of Closed Sets and Closures · isSeqClosed_iff_isClosed (+1 more)
Lemma 180 — Convergence in \(\mathbf{H} \times \mathbf{H}\) is Componentwise · Prod.tendsto_iff
Definition 181 — Closed and Closable Operators · LinearPMap.graph (+4 more)
Proposition 182 — Linearity and the Sequential Description of the Closure · Physicslib4.Spectral.Unbounded.hasDenseDomain_closure (+5 more)
Lemma 183 — The Closure of a Symmetric Operator is Symmetric · Physicslib4.Spectral.Unbounded.isSymmetric_closure
Definition 184 — Essentially Self-Adjoint Operator · Physicslib4.Spectral.Unbounded.IsEssentiallySelfAdjoint

§10.3.1 · Unbounded Operators › Elementary Properties of Adjoints and Closed Operators (p. 165) — 14 items

Definition 185 — Closed Linear Map on a Subspace · LinearPMap.IsClosed (+1 more)
Proposition 186 — Closed Graph of the Adjoint; Closability of Symmetric Operators · Physicslib4.Spectral.Unbounded.isClosable_of_isSymmetric (+1 more)
Proposition 187 — The Adjoint of a Closure · Physicslib4.Spectral.Unbounded.adjoint_closure_eq_adjoint
Lemma 188 — Extension Reverses Adjoint Domains · Physicslib4.Spectral.Unbounded.adjoint_le_adjoint_of_le
Lemma 189 — A Self-Adjoint Operator has no Proper Symmetric Extension · Physicslib4.Spectral.Unbounded.eq_of_isSelfAdjoint_of_isSymmetric_of_le
Proposition 190 — Uniqueness of the Self-Adjoint Extension of an Essentially Self-Adjoint Operator · Physicslib4.Spectral.Unbounded.existsUnique_isSelfAdjoint_extension (+1 more)
Definition 191 — Kernel of an Unbounded Operator · Physicslib4.Spectral.Unbounded.ker
Definition 192 — Range of an Unbounded Operator · Physicslib4.Spectral.Unbounded.range
Proposition 193 — Orthogonal Decomposition and the Double Complement · Physicslib4.Spectral.Unbounded.existsUnique_add_mem_orthogonal (+1 more)
Corollary 194 — Trivial Complement Characterizes Density · Physicslib4.Spectral.Unbounded.dense_iff_orthogonal_eq_bot
Proposition 195 — Orthogonal Complement of the Range · Physicslib4.Spectral.Unbounded.orthogonal_range_eq_ker_adjoint
Proposition 196 — Adjoint of a Sum with a Bounded Operator · Physicslib4.Spectral.Unbounded.adjoint_add_toPMap (+1 more)
Lemma 197 — Adjoint of a Scalar Multiple of the Identity · Physicslib4.Spectral.Unbounded.adjoint_smul_id
Proposition 198 — Closedness of the Range from a Lower Bound · Physicslib4.Spectral.Unbounded.isClosed_range_subSmul

§10.3.1 · Unbounded Operators › The Spectrum of an Unbounded Operator (p. 171) — 5 items

Definition 199 — Resolvent Set and Spectrum of an Unbounded Operator · Physicslib4.Spectral.Unbounded.pmapResolventSet (+2 more)
Lemma 200 — Uniqueness of the Resolvent · Physicslib4.Spectral.Unbounded.existsUnique_isResolvent
Lemma 201 — The Two Notions of Spectrum Agree for Bounded Operators · Physicslib4.Spectral.Unbounded.pmapResolventSet_toPMap_top (+1 more)
Lemma 202 — The \(b^2\) Inequality for Symmetric Operators · Physicslib4.Spectral.Unbounded.sq_norm_le_of_isSymmetric
Theorem 203 — Spectrum of a Self-Adjoint Operator is Real · Physicslib4.Spectral.Unbounded.pmapSpectrum_subset_real

§10.3.1 · Unbounded Operators › Conditions for Self-Adjointness and Essential Self-Adjointness (p. 174) — 9 items

Theorem 204 — Essential Self-Adjointness via Dense Range · Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_iff_dense_range
Definition 205 — Hilbert Space Direct Sum · lp (+1 more)
Lemma 206 — The Finite Direct Sum is Dense · Physicslib4.Spectral.Unbounded.dense_setOf_finite_support
Definition 207 — Unitary Operator · unitary (+2 more)
Definition 208 — Internal Orthogonal Decomposition · Physicslib4.Spectral.Unbounded.IsInternalOrthogonalDecomposition
Proposition 209 — Polarization Identity for the Inner Product · inner_eq_sum_norm_sq_div_four (+1 more)
Lemma 210 — Internal Decompositions are Unitarily External Direct Sums · Physicslib4.Spectral.Unbounded.hasSum_injective_of_isInternalOrthogonalDecomposition (+2 more)
Proposition 211 — Direct Sums of Bounded Self-Adjoint Operators · Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_of_isDirectSumOperator (+6 more)
Proposition 212 — Direct Sums of Bounded Self-Adjoint Operators, Internal Form · Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_of_isInternalDirectSumOperator (+6 more)

§10.3.1 · Integration Against a Projection-Valued Measure (p. 182) — 28 items

Convention 213 — Standing Hypotheses: Integration against a Projection-Valued Measure (a standing convention, not a declaration; it carries no Lean annotation)
Lemma 214 — The Associated Measure has Total Mass \(\left\| \psi \right\|^2\) · Physicslib4.Spectral.Unbounded.assoc_univ_eq (+1 more)
Lemma 215 — Norm Identity for the Bounded Integral · Physicslib4.Spectral.Unbounded.norm_sq_integral_apply
Definition 216 — Sesquilinear Form on a Subspace · Physicslib4.Spectral.Unbounded.SesquilinearFormOn
Definition 217 — Quadratic Form on a Subspace · Physicslib4.Spectral.Unbounded.IsQuadraticFormOn (+2 more)
Proposition 218 — Properties of Quadratic Forms on a Subspace · Physicslib4.Spectral.Unbounded.polarizationOn_eq_inner (+1 more)
Lemma 219 — Restriction of a Quadratic Form to a Subspace · Physicslib4.Spectral.Unbounded.isQuadraticFormOn_restrict (+1 more)
Theorem 220 — Monotone Convergence Theorem, for Integrals · MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone (+1 more)
Theorem 221 — Dominated Convergence Theorem · MeasureTheory.tendsto_integral_of_dominated_convergence (+3 more)
Proposition 222 — Linearity of the Integral in the Measure · MeasureTheory.lintegral_add_measure (+3 more)
Proposition 223 — Monotonicity of the Integral in the Measure · MeasureTheory.lintegral_mono' (+1 more)
Definition 224 — \(L^2\) of a Measure Space · MeasureTheory.MemLp (+3 more)
Proposition 225 — Countable Additivity of the Integral over a Disjoint Cover · MeasureTheory.lintegral_iUnion (+1 more)
Proposition 226 — Integrals Agree when Measures Agree on a Set · Physicslib4.Spectral.Unbounded.setLIntegral_congr_measure
Lemma 227 — The Range of a Projection is the Kernel of its Complement · Physicslib4.Spectral.Unbounded.range_eq_ker_one_sub (+2 more)
Lemma 228 — A Closed Subspace is a Separable Hilbert Space · Physicslib4.Spectral.Unbounded.completeSpace_and_separableSpace_of_isClosed (+2 more)
Lemma 229 — Range Membership Concentrates the Associated Measure · Physicslib4.Spectral.Unbounded.assoc_compl_eq_zero (+1 more)
Lemma 230 — Norm-Convergent Decomposition over a Disjoint Cover · Physicslib4.Spectral.Unbounded.hasSum_apply_of_partition (+1 more)
Lemma 231 — \(L^2\) Implies \(L^1\) on a Finite Measure Space · MeasureTheory.MemLp.integrable (+1 more)
Proposition 232 — Properties of the Integral against a Projection-Valued Measure · Physicslib4.Spectral.Unbounded.integralDomain (+7 more)
Lemma 233 — Bounded on a Set Implies the Range Lies in the Domain · Physicslib4.Spectral.Unbounded.range_subset_integralDomain (+1 more)
Proposition 234 — The Integral against a Projection-Valued Measure · Physicslib4.Spectral.Unbounded.pmapIntegral (+5 more)
Proposition 235 — Coincidence with the Bounded Integral · Physicslib4.Spectral.Unbounded.integralDomain_eq_top_of_bddMeasurable (+1 more)
Lemma 236 — The Integral Ignores Null Sets · Physicslib4.Spectral.Unbounded.integralDomain_congr_of_null (+1 more)
Lemma 237 — Truncations Converge to the Unbounded Integral · Physicslib4.Spectral.Unbounded.tendsto_integral_truncation
Lemma 238 — The Associated Measure of a Bounded-Calculus Image · Physicslib4.Spectral.Unbounded.assoc_integral_apply (+1 more)
Lemma 239 — The Integral Preserves Spectral Subspaces on which the Integrand is Bounded · Physicslib4.Spectral.Unbounded.mapsTo_pmapIntegral_range (+1 more)
Proposition 240 — The Integral of a Real-Valued Function is Self-Adjoint · Physicslib4.Spectral.Unbounded.isSelfAdjoint_pmapIntegral_of_real

§10.3.1 · The Spectral Theorem for Bounded Normal Operators (p. 201) — 6 items

Definition 241 — Normal Operator · IsStarNormal
Lemma 242 — Bounded Self-Adjoint Operators are Normal · IsSelfAdjoint.isStarNormal
Lemma 243 — Power Growth is Controlled by the Spectral Radius · Physicslib4.Spectral.Unbounded.tendsto_norm_pow_div_atTop
Lemma 244 — Spectral Radius of a Product of Commuting Operators · Physicslib4.Spectral.Unbounded.spectralRadius_mul_le_of_commute
Lemma 245 — Adjoint of a Product; the Adjoint is an Involution · ContinuousLinearMap.adjoint_comp (+1 more)
Proposition 246 — Norm Equals Spectral Radius for Normal Operators · IsStarNormal.spectralRadius_eq_nnnorm

§10.3.1 · The Spectral Theorem for Bounded Normal Operators › Spectral Subspaces (p. 204) — 3 items

Definition 247 — Spectral Subspaces · Physicslib4.Spectral.Unbounded.spectralSubspace
Proposition 248 — Properties of Spectral Subspaces · Physicslib4.Spectral.Unbounded.pvmOperator (+3 more)
Proposition 249 — Commuting Operators Preserve Spectral Subspaces · Physicslib4.Spectral.Unbounded.commute_borelCalculus (+1 more)

§10.3.1 · The Spectral Theorem for Bounded Normal Operators › Almost Eigenvectors (p. 208) — 7 items

Lemma 250 — Normality Balances the Two Norms · Physicslib4.Spectral.Unbounded.norm_adjoint_sub_smul_apply
Definition 251 — \(\varepsilon\)-Almost Eigenvector · Physicslib4.Spectral.Unbounded.IsAlmostEigenvector
Lemma 252 — Almost Eigenvectors and the Spectrum of a Normal Operator · Physicslib4.Spectral.Unbounded.isAlmostEigenvector_adjoint (+1 more)
Lemma 253 — Polynomials Preserve Almost Eigenvectors · Physicslib4.Spectral.Unbounded.exists_const_isAlmostEigenvector_mvApply_uniform (+1 more)
Lemma 254 — Polynomials in a Normal Operator are Normal · Physicslib4.Spectral.Unbounded.mvApply (+4 more)
Lemma 255 — Restriction of a Normal Operator to a Doubly Invariant Subspace · Physicslib4.Spectral.Unbounded.exists_restrict_isStarNormal
Lemma 256 — An Almost-Eigenvector Subspace for a Polynomial in a Normal Operator · Physicslib4.Spectral.Unbounded.exists_subspace_isAlmostEigenvector

§10.3.1 · The Spectral Theorem for Bounded Normal Operators › The Two-Variable Spectral Mapping Theorem (p. 212) — 2 items

Theorem 257 — Spectral Mapping for Polynomials in \(A\) and \(A^*\) · Physicslib4.Spectral.Unbounded.spectrum_mvApply
Corollary 258 — Norm of a Polynomial in \(A\) and \(A^*\) · Physicslib4.Spectral.Unbounded.norm_mvApply

§10.3.1 · The Spectral Theorem for Bounded Normal Operators › The Continuous Functional Calculus for a Normal Operator (p. 213) — 1 item

Theorem 259 — Continuous Functional Calculus for a Normal Operator · Physicslib4.Spectral.Unbounded.mvPolyOn (+9 more)

§10.3.1 · From a Continuous Functional Calculus to a Projection-Valued Measure (p. 215) — 14 items

Convention 260 — Standing Hypotheses: The Abstract Functional Calculus (a standing convention, not a declaration; it carries no Lean annotation)
Definition 261 — Abstract Continuous Functional Calculus · Physicslib4.Spectral.Unbounded.IsAbstractCalculus
Lemma 262 — An Abstract Calculus is Non-Negative · Physicslib4.Spectral.Unbounded.isSelfAdjoint_of_real (+2 more)
Definition 263 — The Measures Associated to an Abstract Calculus · Physicslib4.Spectral.Unbounded.abstractMeasure (+2 more)
Lemma 264 — The Abstract Associated Measures are Finite · Physicslib4.Spectral.Unbounded.abstractMeasure_univ
Proposition 265 — The Extended Forms are Bounded Quadratic Forms · Physicslib4.Spectral.Unbounded.isBoundedQuadraticForm_abstractForm (+3 more)
Definition 266 — The Extended Calculus · Physicslib4.Spectral.Unbounded.extendedCalculus (+2 more)
Lemma 267 — The Extended Calculus is Linear · Physicslib4.Spectral.Unbounded.extendedCalculus_smul_add
Lemma 268 — Off-Diagonal Formula and Bounded Convergence for the Extended Calculus · Physicslib4.Spectral.Unbounded.polarization_abstractForm (+1 more)
Lemma 269 — Real Functions Give Self-Adjoint Operators · Physicslib4.Spectral.Unbounded.isSelfAdjoint_extendedCalculus_of_real
Proposition 270 — The Extended Calculus is Multiplicative · Physicslib4.Spectral.Unbounded.extendedCalculus_mul
Lemma 271 — The Extended Calculus Respects Conjugation · Physicslib4.Spectral.Unbounded.extendedCalculus_conj
Theorem 272 — A Continuous Functional Calculus Yields a Projection-Valued Measure · Physicslib4.Spectral.Unbounded.abstractPVM (+2 more)
Corollary 273 — The Extended Calculus is Norm-Bounded · Physicslib4.Spectral.Unbounded.norm_extendedCalculus_le

§10.3.1 · From a Continuous Functional Calculus to a Projection-Valued Measure › The Spectral Theorem for Bounded Normal Operators (p. 222) — 1 item

Theorem 274 — Spectral Theorem for Bounded Normal Operators · Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_normal (+1 more)

§10.3.1 · The Cayley Transform (p. 223) — 5 items

Lemma 275 — Unitary Operators are Normal · Physicslib4.Spectral.Unbounded.unitary_mul_adjoint
Lemma 276 — The Spectrum of a Unitary Operator Lies on the Unit Circle · spectrum.subset_circle_of_unitary (+1 more)
Lemma 277 — The Cayley Map and its Inverse · Physicslib4.Spectral.Unbounded.unitCircleMinusOne (+9 more)
Theorem 278 — Cayley Transform · Physicslib4.Spectral.Unbounded.IsCayleyTransform (+1 more)
Lemma 279 — Spectral Mapping for the Cayley Transform · Physicslib4.Spectral.Unbounded.mem_spectrum_iff_cayleyMap_mem_spectrum (+1 more)

§10.3.1 · Proof of the Spectral Theorem for Unbounded Self-Adjoint Operators (p. 227) — 9 items

Theorem 280 — Change of Variables for a Pushforward Measure · MeasureTheory.lintegral_map_equiv (+1 more)
Lemma 281 — A Borel Bijection Transports a Projection-Valued Measure · Physicslib4.Spectral.Unbounded.restrictPVM (+2 more)
Lemma 282 — The Cayley Transform Omits the Point \(1\) · Physicslib4.Spectral.Unbounded.spectralMeasure_singleton_one_eq_zero
Proposition 283 — Spectral Subspaces of the Cayley Transform · Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyInv_eq
Theorem 284 — Transporting the Spectral Measure through the Cayley Transform · Physicslib4.Spectral.Unbounded.cayleyPVM (+1 more)
Theorem 285 — Spectral Theorem for Unbounded, Self-Adjoint Operators · Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_unbounded (+1 more)
Definition 286 — Spectral Measure of a Self-Adjoint Operator · Physicslib4.Spectral.Unbounded.spectralMeasure (+3 more)
Definition 287 — Functional Calculus for an Unbounded Self-Adjoint Operator · Physicslib4.Spectral.Unbounded.functionalCalculus (+2 more)
Lemma 288 — Functional Calculus of a Bounded Function · Physicslib4.Spectral.Unbounded.functionalCalculus_of_bddMeasurable

Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide

← §10.2 Spectral · §10.4 Stone →