2.Β Bounded spectral theoryπŸ”—

This chapter describes how the library encodes the spectral theory of bounded self-adjoint operators on a complex Hilbert space, up to the spectral theorem. It corresponds to Section 10.2 of the blueprint, which follows the presentation of Hall's Quantum Theory for Mathematicians. The spectral theorem for unbounded operators and Stone's theorem, in Sections 10.3 and 10.4 of the blueprint, build on it.

2.1.Β OverviewπŸ”—

As you will recall, a Hermitian matrix A has real eigenvalues \lambda_k and mutually orthogonal eigenprojections P_k summing to \mathbf{1}, so that A = \sum_k \lambda_k P_k, and a function of A is f(A) = \sum_k f(\lambda_k) P_k. The spectral theorem for a bounded self-adjoint operator A on a Hilbert space H says the same with the sum over eigenvalues replaced by an integral over the spectrum \sigma(A) against a projection-valued measure \mu^A:

A = \int_{\sigma(A)} \lambda \, d\mu^A(\lambda), \qquad f(A) = \int_{\sigma(A)} f \, d\mu^A.

For a unit vector \psi, \langle \psi, \mu^A(E)\psi \rangle is the probability that a measurement of A in the state \psi gives a value in E. The integral also covers continuous spectrum: the multiplication operator (M\psi)(x) = x\,\psi(x) on L^2([0, 1]) has spectrum [0, 1] and no eigenvalues.

The library proves the theorem as the blueprint does, in stages:

  • Spectrum and resolvent. The spectrum of a bounded operator is compact, and nonempty when H \neq 0; the resolvent set is open, and the resolvent is a power series near each of its points; the spectrum of a self-adjoint operator is real.

  • The continuous functional calculus. For self-adjoint A, f \mapsto f(A) on the continuous real functions on \sigma(A) is the unique bounded linear map that extends p \mapsto p(A) on polynomials. It is multiplicative and isometric, f(A) is self-adjoint, non-negative when f \ge 0, and \sigma(f(A)) = f(\sigma(A)).

  • The associated measures. By the Riesz–Markov–Kakutani theorem, for each \psi there is a unique finite positive measure \mu_\psi on \sigma(A) with \langle \psi, f(A)\psi \rangle = \int f \, d\mu_\psi for continuous f, of total mass \|\psi\|^2.

  • Forms. A bounded quadratic form Q is \psi \mapsto \langle \psi, B\psi \rangle for a unique bounded operator B. This is how operators are constructed in the rest of the section.

  • The Borel functional calculus. For a bounded Borel function f on \sigma(A), Q_f(\psi) = \int f \, d\mu_\psi is a bounded quadratic form, and f(A) is its operator. The map f \mapsto f(A) is linear and multiplicative, and f(A) is self-adjoint for real f. The boundedness of Q_f and the multiplicativity are extended from continuous to Borel functions by a monotone-class argument.

  • Projection-valued measures and their integrals. A projection-valued measure \mu gives a measure \mu_\psi(E) = \langle \psi, \mu(E)\psi \rangle for each vector and an operator \int f \, d\mu for each bounded measurable f, with \langle \psi, (\int f \, d\mu)\psi \rangle = \int f \, d\mu_\psi. The integral is linear and multiplicative, bounded by \sup |f|, and sends \bar f to the adjoint.

  • The spectral theorem. The projections \mu^A(E) = 1_E(A) form a projection-valued measure on \sigma(A) that integrates the identity function to A, and it is the only one that does. For bounded Borel f, f(A) = \int f \, d\mu^A.

Every statement of the section is proved in Lean. The standard results the blueprint states without proof, such as the Heine–Borel, Riesz representation, Stone–Weierstrass and bounded convergence theorems, are Mathlib theorems or short derivations from them. The declarations are in the namespace Physicslib4.Spectral, written without the prefix below.

2.2.Β DesignπŸ”—

The conventions inherited from Mathlib, among them realCalculus as Mathlib's cfcHom, are collected in the conventions chapter under Implementation choices.

The blueprint is the specification. Where the library departs from the blueprint's route, this section says so; where the blueprint records the departure in a formalization note or a convention, the section links to it.

2.2.1.Β Operators, adjoints and the Hilbert spaceπŸ”—

A bounded operator is an element of H β†’L[β„‚] H, Mathlib's continuous linear maps, which is the blueprint's \mathcal{B}(H). Mathlib supplies the operator norm, the adjoint (ContinuousLinearMap.adjoint), self-adjointness (IsSelfAdjoint), orthogonal projections (IsStarProjection), and a C*-algebra structure on H β†’L[β„‚] H. Its inner product is conjugate-linear in the first argument, the physics convention that the blueprint fixes in def:inner-product.

The blueprint takes H separable and nonzero, but only for convenience. No declaration assumes separability; the convergence arguments use only completeness. Nonzero H appears as a Nontrivial H hypothesis on just the statements that use it, such as the nonemptiness of the spectrum (conv:nonzero-hilbert-space).

2.2.2.Β Spectrum and resolvent are Mathlib'sπŸ”—

The spectrum and the resolvent set are Mathlib's spectrum β„‚ A and resolventSet β„‚ A. Mathlib defines them through \lambda\mathbf{1} - A, the blueprint through A - \lambda\mathbf{1}; the two give the same set, which mem_resolventSet_iff_isUnit_sub_smul records. Mathlib's resolvent A Ξ» is (\lambda\mathbf{1} - A)^{-1}, the negative of the blueprint's resolvent.

Once \sigma(A) is known to be real for self-adjoint A (spectrum_subset_real), every later statement uses Mathlib's real spectrum spectrum ℝ A, a compact subset of \mathbb{R}, instead of the blueprint's subset of \mathbb{C}. It is the type on which Mathlib's functional calculus is indexed, and it carries the Borel Οƒ-algebra of its topology as a subspace of \mathbb{R}. Functions on the spectrum are functions on this subtype, and the identity function \lambda is fun l => ((l : ℝ) : β„‚), which Lean prints as fun l => ↑↑l.

2.2.3.Β The continuous calculus is Mathlib'sπŸ”—

The blueprint builds f \mapsto f(A) by hand: polynomials first, then the extension to continuous functions by density (the Stone–Weierstrass theorem) and the bounded linear transformation theorem. Mathlib already has the continuous functional calculus for self-adjoint elements of a C*-algebra, cfcHom, and the library uses it: realCalculus hA is cfcHom hA. Its type, a *-algebra homomorphism C(spectrum ℝ A, ℝ) →⋆ₐ[ℝ] (H β†’L[β„‚] H), records multiplicativity and compatibility with the adjoint, and Mathlib proves the norm identity and spectral mapping for it. What the library adds is the blueprint's characterisation: realCalculus is the unique bounded linear map that sends each polynomial to p(A), proved from the density of the polynomials (formalization note of prpstn:hall-8.3).

As in the blueprint, the continuous calculus is for real functions; the Borel calculus below takes complex ones.

2.2.4.Β Measures from the Riesz–Markov–Kakutani theoremπŸ”—

The measure \mu_\psi is Mathlib's Riesz–Markov–Kakutani measure RealRMK.rieszMeasure of the positive functional f \mapsto \langle \psi, f(A)\psi \rangle. Mathlib states that theorem for compactly supported functions; on the compact \sigma(A) these are all continuous functions. Uniqueness of \mu_\psi is Mathlib's uniqueness of the representing measure, so the associated-measure theorem is fully proved.

2.2.5.Β Operators from quadratic formsπŸ”—

Two constructions in the section produce operators: the Borel calculus f(A) and the integral \int f \, d\mu. Both go through the same lemma (prpstn:hall-a.63): a bounded quadratic form Q determines a unique bounded B with Q(\psi) = \langle \psi, B\psi \rangle. The form in both cases is Q_f(\psi) = \int f \, d\mu_\psi, so the hard work is to show that it is a bounded quadratic form.

Sesquilinear forms are Mathlib's bundled semilinear maps: H →ₗ⋆[β„‚] H β†’β‚—[β„‚] β„‚, and, for bounded ones, the continuous version H β†’L⋆[β„‚] H β†’L[β„‚] β„‚, whose continuity is the bound |L(\varphi, \psi)| \le C\|\varphi\|\|\psi\|. A quadratic form is a property of a plain function Q : H β†’ β„‚ (IsQuadraticForm, IsBoundedQuadraticForm): Q_f arrives as a function, and these properties are what must be proved of it. The operator IsBoundedQuadraticForm.toOperator comes from the polarization of Q through Mathlib's Riesz representation of bounded sesquilinear forms.

The operators borelCalculus hA f and μ.integral f are chosen from the existence-and-uniqueness theorems, so their properties are theorems and not definitional: linearity is borelCalculus_add, integral_add and their scalar versions. Both are defined on all functions, with the value 0 on functions that are not bounded and measurable, so every statement takes the hypothesis f ∈ BddMeasurable _ explicitly.

2.2.6.Β Bounded Borel functions and the monotone-class bootstrapπŸ”—

The bounded measurable functions on X form the complex subspace BddMeasurable X, a Mathlib Submodule; membership is the pair "measurable, and bounded by a constant". It is the one spelling of "bounded Borel function" in the section.

Three results extend a property from continuous to bounded Borel functions: that Q_f is a bounded quadratic form, that the Borel calculus is multiplicative, and that two spectral measures of A integrate every bounded Borel function to the same operator. All three use one lemma, IsBorelGenerating.eq_bddMeasurable: a class of bounded measurable functions that is a subspace, contains the continuous real functions, and is closed under uniformly bounded pointwise limits, is all of BddMeasurable X. The proof follows the blueprint. The class \mathcal{L}_0 (L0) of sets whose indicator is a bounded pointwise limit of continuous functions contains the closed sets (by bump functions) and is an algebra of sets, and the monotone class theorem, proved in the library, extends it to all Borel sets. Mathlib's dominated convergence theorem gives the bounded convergence theorem, which is what passes the limits through \int \cdot \, d\mu_\psi. Each application then defines its class and checks the three conditions: FClass for boundedness, F1Class and F2Class for multiplicativity.

The lemma needs a metric space with its Borel Οƒ-algebra but not compactness. L0 omits the blueprint's requirement that the set be measurable, since that follows (measurableSet_of_mem_L0).

2.2.7.Β Projection-valued measuresπŸ”—

ProjectionValuedMeasure X H is a structure, with the blueprint's axioms as fields (def:projection-valued-measure). As for Mathlib's vector measures, the underlying map is defined on all subsets of X, and is 0 on non-measurable ones, so applying \mu to a set needs no measurability proof. Countable additivity is strong: \sum_j \mu(E_j)v converges to \mu(\bigcup_j E_j)v for each vector v, stated with Mathlib's unconditional HasSum, which for orthogonal vectors is the same as convergence of the partial sums. \mu(\emptyset) = 0 is not a field, since it follows from countable additivity. The blueprint's equivalence of projection-valued measures is equality.

2.2.8.Β Two routes to f(A) and uniquenessπŸ”—

The section has two Borel calculi. borelCalculus hA f is built from Q_f with the measures \mu_\psi of the Riesz–Markov–Kakutani theorem. The spectral measure is then \mu^A(E) = 1_E(A), spectralMeasure hA, and functionalCalculus hA f is \int f \, d\mu^A. They agree (borelCalculus_eq_integral), so f(A) is unambiguous.

The spectral theorem is stated with βˆƒ! over projection-valued measures on spectrum ℝ A. Uniqueness follows the blueprint: two projection-valued measures that integrate \lambda to A agree on polynomials, then on continuous functions by the complex Stone–Weierstrass theorem, then on bounded Borel functions by the bootstrap, and so on indicator functions, which give the projections themselves.

2.3.Β Main definitions and theoremsπŸ”—

Definitions are shown with their docstrings, which give the mathematics and the blueprint entry; theorems with their statements, as Lean prints them, and a line or two of explanation. Each subsection opens with the blueprint entries it covers. In the printed statements, inner β„‚ x y is the inner product \langle x, y \rangle, hA : IsSelfAdjoint A is the hypothesis that A is self-adjoint, ↑(spectrum ℝ A) is the real spectrum as a type, and fun l => ↑↑l is the function \lambda on it. For the declarations not shown here, see the API documentation and the files listed at the end of the chapter. The subsections follow the order of the proof; the blueprint introduces projection-valued measures before the continuous calculus.

2.3.1.Β Spectrum and resolventπŸ”—

Blueprint: def:bounded-operator-resolvent-and-spectrum, prpstn:hall-7.5, prpstn:resolvent-holomorphy-and-neumann-series, prpstn:hall-7.7, lmm:spectrum-is-compact-metric-measurable, def:spectral-radius, thrm:gelfand-formula.

The spectrum and the resolvent set are Mathlib's. The library identifies them with the blueprint's, in its sign convention:

open Physicslib4 Spectral in Physicslib4.Spectral.mem_resolventSet_iff_isUnit_sub_smul.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] (A : H β†’L[β„‚] H) (lam : β„‚) : lam ∈ resolventSet β„‚ A ↔ IsUnit (A - lam β€’ 1)#check mem_resolventSet_iff_isUnit_sub_smul 
Physicslib4.Spectral.mem_resolventSet_iff_isUnit_sub_smul.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] (A : H β†’L[β„‚] H) (lam : β„‚) : lam ∈ resolventSet β„‚ A ↔ IsUnit (A - lam β€’ 1)

The spectrum is compact (isCompact_spectrum) and, for H \neq 0, nonempty (spectrum_nonempty); the resolvent set is open, and near each of its points the resolvent is a norm-convergent power series (isOpen_resolventSet, exists_hasSum_resolvent). The spectral radius and Gelfand's formula are Mathlib's spectralRadius and spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius. For a self-adjoint operator the spectrum is real:

open Physicslib4 Spectral in Physicslib4.Spectral.spectrum_subset_real.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) : spectrum β„‚ A βŠ† {z | z.im = 0}#check spectrum_subset_real 
Physicslib4.Spectral.spectrum_subset_real.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) : spectrum β„‚ A βŠ† {z | z.im = 0}

The proof takes this from Mathlib (IsSelfAdjoint.spectrumRestricts). The blueprint's estimate behind it, \|(A - (a + ib)\mathbf{1})\psi\|^2 \ge b^2\|\psi\|^2 for real a and b, is sq_norm_sub_smul_apply_le.

2.3.2.Β The continuous functional calculusπŸ”—

Blueprint: prpstn:hall-8.3, prpstn:hall-8.4, and its parts prpstn:cfc-multiplicative to prpstn:cfc-spectral-mapping.

πŸ”—def
Physicslib4.Spectral.realCalculus.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) :
  C(↑(spectrum ℝ A), ℝ) →⋆ₐ[ℝ] H β†’L[β„‚] H
Physicslib4.Spectral.realCalculus.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A) :
  C(↑(spectrum ℝ A), ℝ) →⋆ₐ[ℝ] H β†’L[β„‚] H

The real continuous functional calculus f ↦ f(A) of a self-adjoint bounded operator A.

For a continuous real function f on the spectrum Οƒ(A), f(A) is the norm limit of p_n(A) for any polynomials p_n converging to f uniformly on Οƒ(A). In finite dimensions, where A has an orthonormal eigenbasis, f(A) multiplies each eigenvector by f of its eigenvalue. The map is linear, sends polynomials to the evident operators (realCalculus_polyOn), and is the unique bounded linear map that does so (existsUnique_realCalculus). It is multiplicative, f(A) is self-adjoint, f β‰₯ 0 gives a non-negative operator, β€–f(A)β€– = sup |f| on Οƒ(A), and Οƒ(f(A)) = f(Οƒ(A)) (realCalculus_properties).

Implementation note: the definition is Mathlib's continuous functional calculus cfcHom at the hypothesis hA, available because Mathlib makes H β†’L[β„‚] H a C*-algebra; it is not extracted from existsUnique_realCalculus. Its type, a StarAlgHom over ℝ, records that f ↦ f(A) is a *-algebra homomorphism and not only an ℝ-linear map, which is part of prpstn:hall-8.4. Οƒ(A) is Mathlib's real spectrum spectrum ℝ A.

Blueprint: the map f ↦ f(A) of prpstn:hall-8.3

The blueprint's characterisation, with polyOn A p the polynomial p restricted to \sigma(A):

open Physicslib4 Spectral in Physicslib4.Spectral.existsUnique_realCalculus.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) : βˆƒ! T, βˆ€ (p : Polynomial ℝ), T (polyOn A p) = (Polynomial.aeval A) p#check existsUnique_realCalculus 
Physicslib4.Spectral.existsUnique_realCalculus.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) :
  βˆƒ! T, βˆ€ (p : Polynomial ℝ), T (polyOn A p) = (Polynomial.aeval A) p

Here T ranges over the bounded ℝ-linear maps C(spectrum ℝ A, ℝ) β†’L[ℝ] (H β†’L[β„‚] H), and realCalculus_polyOn says that realCalculus is the one. The properties are separate theorems, collected in realCalculus_properties; for example, the norm identity \|f(A)\| = \sup_{\sigma(A)} |f|:

open Physicslib4 Spectral in Physicslib4.Spectral.norm_realCalculus.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) : β€–(realCalculus hA) fβ€– = β€–fβ€–#check norm_realCalculus 
Physicslib4.Spectral.norm_realCalculus.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) : β€–(realCalculus hA) fβ€– = β€–fβ€–

2.3.3.Β The associated measuresπŸ”—

Blueprint: thrm:riesz-representation, prpstn:associated-measures-self-adjoint, lmm:associated-measures-are-finite.

πŸ”—def
Physicslib4.Spectral.assocMeasure.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (ψ : H) :
  MeasureTheory.Measure ↑(spectrum ℝ A)
Physicslib4.Spectral.assocMeasure.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A) (ψ : H) :
  MeasureTheory.Measure ↑(spectrum ℝ A)

The finite positive Borel measure ΞΌ_ψ on Οƒ(A) with ⟨ψ, f(A)ψ⟩ = ∫ f dΞΌ_ψ for continuous real f.

For a unit vector ψ, ΞΌ_ψ is the probability distribution of the outcomes of a measurement of A in the state ψ: ΞΌ_ψ(E) is the probability of finding a value in E. Its total mass is β€–Οˆβ€–Β² (assocMeasure_univ), the integral identity is integral_assocMeasure, and ΞΌ_ψ is the only finite measure with that identity (existsUnique_assocMeasure). It defines the quadratic form Q_f(ψ) = ∫ f dΞΌ_ψ of the Borel functional calculus (borelForm).

Implementation note: the measure is Mathlib's Riesz–Markov–Kakutani measure RealRMK.rieszMeasure of assocFunctional hA ψ, not a choice from existsUnique_assocMeasure.

Blueprint: the measure μ_ψ of prpstn:associated-measures-self-adjoint

The associated-measure theorem, existence and uniqueness:

open Physicslib4 Spectral in Physicslib4.Spectral.existsUnique_assocMeasure.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (ψ : H) : βˆƒ! Ξ½, MeasureTheory.IsFiniteMeasure Ξ½ ∧ βˆ€ (f : C(↑(spectrum ℝ A), ℝ)), inner β„‚ ψ (((realCalculus hA) f) ψ) = ↑(∫ (l : ↑(spectrum ℝ A)), f l βˆ‚Ξ½)#check existsUnique_assocMeasure 
Physicslib4.Spectral.existsUnique_assocMeasure.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (ψ : H) :
  βˆƒ! Ξ½,
    MeasureTheory.IsFiniteMeasure ν ∧
      βˆ€ (f : C(↑(spectrum ℝ A), ℝ)), inner β„‚ ψ (((realCalculus hA) f) ψ) = ↑(∫ (l : ↑(spectrum ℝ A)), f l βˆ‚Ξ½)

Here Ξ½ ranges over the measures on spectrum ℝ A; the integral is real, and ↑ embeds it in \mathbb{C}. The total mass is assocMeasure_univ, \mu_\psi(\sigma(A)) = \|\psi\|^2, stated in Mathlib's extended non-negative reals, where measures take their values. The Riesz–Markov–Kakutani theorem itself, for a positive functional on the continuous functions on a compact metric space, is existsUnique_measure_of_positive_linear.

2.3.4.Β Sesquilinear and quadratic formsπŸ”—

Blueprint: def:bounded-sesquilinear-form, def:bounded-quadratic-form, prpstn:hall-a.61, prpstn:hall-a.63.

πŸ”—def
Physicslib4.Spectral.BoundedSesquilinearForm.{u_2} (H : Type u_2)
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] : Type u_2
Physicslib4.Spectral.BoundedSesquilinearForm.{u_2}
  (H : Type u_2) [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] : Type u_2

The bounded sesquilinear forms on H: sesquilinear L with |L(Ο†, ψ)| ≀ Cβ€–Ο†β€–β€–Οˆβ€– for some constant C.

The matrix elements L(Ο†, ψ) = βŸ¨Ο†, Aψ⟩ of a bounded operator A are the basic example, with C = β€–Aβ€–. The polarization of a bounded quadratic form is one (IsBoundedQuadraticForm.toSesq), and this is how the spectral files turn quadratic forms into operators.

Implementation note: this is Mathlib's space H β†’L⋆[β„‚] H β†’L[β„‚] β„‚ of continuous conjugate-linear maps into the continuous linear functionals. Continuity of the outer map is the bound β€–L Ο†β€– ≀ Cβ€–Ο†β€– in the operator norm, which is the bound |L(Ο†, ψ)| ≀ Cβ€–Ο†β€–β€–Οˆβ€–.

Blueprint: def:bounded-sesquilinear-form

πŸ”—structure
Physicslib4.Spectral.IsQuadraticForm.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] (Q : H β†’ β„‚) : Prop
Physicslib4.Spectral.IsQuadraticForm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] (Q : H β†’ β„‚) :
  Prop

A quadratic form on H: a map Q : H β†’ β„‚, |Ξ»|Β²-homogeneous, whose polarization is sesquilinear.

The conditions are Q(λψ) = |Ξ»|Β² Q(ψ) for Ξ» ∈ β„‚ and that the polarization of Q is a sesquilinear form. The prototype is the expectation-value map Q(ψ) = ⟨ψ, Aψ⟩ of an operator A. The spectral files build operators from quadratic forms: Q_f(ψ) = ∫ f dΞΌ_ψ defines the operator-valued integral and the Borel functional calculus.

Blueprint: the quadratic forms of def:bounded-quadratic-form

Constructor

Physicslib4.Spectral.IsQuadraticForm.mk.{u_1}

Fields

smul : βˆ€ (l : β„‚) (ψ : H), Q (l β€’ ψ) = ↑‖lβ€– ^ 2 * Q ψ

Q (Ξ» β€’ ψ) = |Ξ»|Β² Q ψ.

isSesquilinear : βˆƒ L, βˆ€ (Ο† ψ : H), (L Ο†) ψ = polarization Q Ο† ψ

The polarization of Q is a sesquilinear form.

πŸ”—structure
Physicslib4.Spectral.IsBoundedQuadraticForm.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] (Q : H β†’ β„‚) : Prop
Physicslib4.Spectral.IsBoundedQuadraticForm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] (Q : H β†’ β„‚) :
  Prop

A bounded quadratic form on H: a quadratic form Q with |Q(Ο†)| ≀ Cβ€–Ο†β€–Β² for some constant C.

Every bounded quadratic form is the expectation-value map of a unique bounded operator: Q(ψ) = ⟨ψ, Aψ⟩ for exactly one A (existsUnique_operator_of_isBoundedQuadraticForm; the operator is IsBoundedQuadraticForm.toOperator), and A is self-adjoint when Q is real-valued (IsBoundedQuadraticForm.isSelfAdjoint_toOperator). This is the route by which the operator-valued integral and the Borel functional calculus are defined.

Blueprint: def:bounded-quadratic-form

Constructor

Physicslib4.Spectral.IsBoundedQuadraticForm.mk.{u_1}

Fields

isQuadratic : IsQuadraticForm Q

The underlying form is quadratic.

bounded : βˆƒ C, βˆ€ (Ο† : H), β€–Q Ο†β€– ≀ C * β€–Ο†β€– ^ 2

The form is bounded by a multiple of β€–Ο†β€–Β².

The representation theorem for bounded quadratic forms:

open Physicslib4 Spectral in Physicslib4.Spectral.existsUnique_operator_of_isBoundedQuadraticForm.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {Q : H β†’ β„‚} (hQ : IsBoundedQuadraticForm Q) : βˆƒ! A, βˆ€ (ψ : H), Q ψ = inner β„‚ ψ (A ψ)#check existsUnique_operator_of_isBoundedQuadraticForm 
Physicslib4.Spectral.existsUnique_operator_of_isBoundedQuadraticForm.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] [CompleteSpace H] {Q : H β†’ β„‚} (hQ : IsBoundedQuadraticForm Q) :
  βˆƒ! A, βˆ€ (ψ : H), Q ψ = inner β„‚ ψ (A ψ)

The operator is hQ.toOperator, and it is self-adjoint when Q is real-valued (IsBoundedQuadraticForm.isSelfAdjoint_toOperator). The polarization formula is polarization. To apply the theorem to a candidate Q_f, one proves the homogeneity Q_f(c\psi) = |c|^2 Q_f(\psi), the sesquilinearity of its polarization and a bound |Q_f(\psi)| \le C\|\psi\|^2; for the Borel calculus these are the propositions from prpstn:F-homogeneous to prpstn:F-bounded.

2.3.5.Β Bounded Borel functions and the bootstrapπŸ”—

Blueprint: thrm:bounded-convergence-theorem, def:L0-class, thrm:monotone-class-theorem, lmm:hall-prblm-8.3.3a, lmm:hall-prblm-8.3.3b, lmm:hall-prblm-8.3.3c.

πŸ”—def
Physicslib4.Spectral.BddMeasurable.{u_2} (X : Type u_2)
  [MeasurableSpace X] : Submodule β„‚ (X β†’ β„‚)
Physicslib4.Spectral.BddMeasurable.{u_2}
  (X : Type u_2) [MeasurableSpace X] :
  Submodule β„‚ (X β†’ β„‚)

The complex vector space of bounded measurable complex-valued functions on a measurable space X.

A function f : X β†’ β„‚ belongs to it when f is measurable and |f(x)| ≀ C for some constant C and every x ∈ X. On the spectrum of an operator, with its Borel Οƒ-algebra, these are the bounded Borel functions to which the Borel functional calculus applies: indicator functions 1_E of Borel sets E (the spectral projections), step functions, and every bounded continuous function.

Implementation note: the class is a Submodule β„‚ (X β†’ β„‚), so membership packages the two hypotheses Measurable f and βˆƒ C, βˆ€ x, β€–f xβ€– ≀ C (mem_bddMeasurable), and closure under sums and scalar multiples is part of the structure. It is the single spelling of "bounded Borel function" in the spectral files.

Blueprint: the bounded Borel functions of def:hall-8.8 and thrm:operator-valued-integration

πŸ”—structure
Physicslib4.Spectral.BoundedPointwiseLimit.{u_2} {Ξ± : Type u_2}
  (f : β„• β†’ Ξ± β†’ β„‚) (g : Ξ± β†’ β„‚) (b : Ξ± β†’ ℝ) : Prop
Physicslib4.Spectral.BoundedPointwiseLimit.{u_2}
  {Ξ± : Type u_2} (f : β„• β†’ Ξ± β†’ β„‚)
  (g : Ξ± β†’ β„‚) (b : Ξ± β†’ ℝ) : Prop

A sequence of functions f_n : Ξ± β†’ β„‚ is bounded by b uniformly in n and converges pointwise to g.

The hypotheses are |f_n(x)| ≀ b(x) for every n and every x, and f_n(x) β†’ g(x) for every x. The convergence is pointwise, not uniform: its rate may depend on the point. This is the hypothesis of the bounded convergence theorem (tendsto_integral_of_boundedPointwiseLimit), which extends the functional calculus from continuous to bounded Borel functions.

Implementation note: the bound b is usually a constant fun _ => M; it may vary so that the same predicate covers the quadratic bound fun Ο† => C * β€–Ο†β€– ^ 2 for sequences of quadratic forms in Physicslib4/Spectral/Forms.lean.

Blueprint: the hypotheses of thrm:bounded-convergence-theorem

Constructor

Physicslib4.Spectral.BoundedPointwiseLimit.mk.{u_2}

Fields

norm_le : βˆ€ (n : β„•) (x : Ξ±), β€–f n xβ€– ≀ b x

The sequence is dominated by b, uniformly in the index.

tendsto : βˆ€ (x : Ξ±), Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))

The sequence converges to g pointwise.

πŸ”—structure
Physicslib4.Spectral.IsBorelGenerating.{u_1} {X : Type u_1}
  [TopologicalSpace X] [MeasurableSpace X] (π’ž : Set (X β†’ β„‚)) : Prop
Physicslib4.Spectral.IsBorelGenerating.{u_1}
  {X : Type u_1} [TopologicalSpace X]
  [MeasurableSpace X] (π’ž : Set (X β†’ β„‚)) :
  Prop

A class π’ž of bounded measurable functions that is a subspace, contains the continuous real functions, and is closed under bounded pointwise limits.

These are the hypotheses of the bootstrap from continuous to bounded Borel functions. On a metric space with its Borel Οƒ-algebra such a class contains the indicator of every Borel set (IsBorelGenerating.indicator_mem) and is in fact all bounded measurable functions (IsBorelGenerating.eq_bddMeasurable). This is how a property known for continuous f, such as multiplicativity of the functional calculus, is extended to every bounded Borel f: one shows that the functions with the property form such a class (isBorelGenerating_F1Class, isBorelGenerating_F2Class).

Implementation note: the structure assumes only a topology and a Οƒ-algebra on X; the metric and Borel hypotheses are on the two theorems, which do not need compactness.

Blueprint: the hypotheses (1)–(3) of lmm:hall-prblm-8.3.3b

Constructor

Physicslib4.Spectral.IsBorelGenerating.mk.{u_1}

Fields

bddMeasurable : π’ž βŠ† ↑(BddMeasurable X)

Every member is bounded and measurable.

smul_add_mem : βˆ€ (Ξ± Ξ² : β„‚) (f g : X β†’ β„‚), f ∈ π’ž β†’ g ∈ π’ž β†’ Ξ± β€’ f + Ξ² β€’ g ∈ π’ž

π’ž is a complex subspace.

continuous_mem : βˆ€ (f : C(X, ℝ)), (fun x => ↑(f x)) ∈ π’ž

π’ž contains the continuous real-valued functions.

tendsto_mem : βˆ€ (f : β„• β†’ X β†’ β„‚) (g : X β†’ β„‚) (M : ℝ), (βˆ€ (n : β„•), f n ∈ π’ž) β†’ (BoundedPointwiseLimit f g fun x => M) β†’ g ∈ π’ž

π’ž is closed under uniformly bounded pointwise limits.

The conclusion of the bootstrap:

open Physicslib4 Spectral in Physicslib4.Spectral.IsBorelGenerating.eq_bddMeasurable.{u_1} {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {π’ž : Set (X β†’ β„‚)} (hπ’ž : IsBorelGenerating π’ž) : π’ž = ↑(BddMeasurable X)#check IsBorelGenerating.eq_bddMeasurable 
Physicslib4.Spectral.IsBorelGenerating.eq_bddMeasurable.{u_1} {X : Type u_1} [MetricSpace X] [MeasurableSpace X]
  [BorelSpace X] {π’ž : Set (X β†’ β„‚)} (hπ’ž : IsBorelGenerating π’ž) : π’ž = ↑(BddMeasurable X)

Its ingredients are the class L0, an algebra of sets containing the open sets (isSetAlgebra_L0), the monotone class theorem (generateFrom_subset_of_isMonotoneClass), and the indicator step IsBorelGenerating.indicator_mem.

2.3.6.Β Projection-valued measures and the operator-valued integralπŸ”—

Blueprint: def:projection-valued-measure, thrm:projection-valued-measures-associated-measure, thrm:operator-valued-integration, prpstn:integral-of-indicator, prpstn:integral-norm-bound, prpstn:integral-multiplicative, prpstn:integral-conjugation.

πŸ”—structure
Physicslib4.Spectral.ProjectionValuedMeasure.{u_3, u_4} (X : Type u_3)
  [MeasurableSpace X] (H : Type u_4) [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] [CompleteSpace H] : Type (max u_3 u_4)
Physicslib4.Spectral.ProjectionValuedMeasure.{u_3,
    u_4}
  (X : Type u_3) [MeasurableSpace X]
  (H : Type u_4) [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] : Type (max u_3 u_4)

A projection-valued measure on X: an assignment E ↦ ΞΌ(E) of orthogonal projections on H to measurable sets, with ΞΌ(X) = πŸ™, countably additive and multiplicative on intersections.

It is the object the spectral theorem attaches to a self-adjoint operator A, with ΞΌ(E) the spectral projection of A for the set E of possible measured values. The axioms: each ΞΌ(E) is a self-adjoint idempotent; ΞΌ(X) = πŸ™; for pairwise disjoint measurable E_1, E_2, … and every vector v, ΞΌ(⋃ E_j)v = Ξ£ ΞΌ(E_j)v with convergence in the norm of H; and ΞΌ(E ∩ F) = ΞΌ(E)ΞΌ(F), so projections of disjoint sets have orthogonal ranges. For each vector ψ, E ↦ ⟨ψ, ΞΌ(E)ψ⟩ is then a finite positive measure (assoc), and bounded measurable functions can be integrated against ΞΌ to give operators (integral).

Implementation note: as in Mathlib's MeasureTheory.VectorMeasure, ΞΌ is a total function Set X β†’ H β†’L[β„‚] H that is 0 on non-measurable sets, so the coercion carries no measurability side conditions. The blueprint's ΞΌ(βˆ…) = 0 is not a field: countable additivity for the constant family E_j = βˆ… implies it, and a field would add a derivable obligation to every constructor. Countable additivity is stated with Mathlib's HasSum, unordered summation; since the vectors ΞΌ(E_j)v are pairwise orthogonal, this is equivalent to convergence of the partial sums. The blueprint's equivalence of two projection-valued measures is equality (ProjectionValuedMeasure.ext).

Blueprint: def:projection-valued-measure

Constructor

Physicslib4.Spectral.ProjectionValuedMeasure.mk.{u_3, u_4}

Fields

toFun : Set X β†’ H β†’L[β„‚] H

The underlying assignment E ↦ ΞΌ(E) of operators to all subsets of X.

isStarProjection' : βˆ€ (E : Set X), IsStarProjection (self.toFun E)

Every value ΞΌ(E) is an orthogonal projection: self-adjoint and idempotent.

notMeasurable' : βˆ€ (E : Set X), Β¬MeasurableSet E β†’ self.toFun E = 0

Non-measurable sets are sent to 0, so ΞΌ is determined by its values on measurable sets.

univ' : self.toFun Set.univ = 1

Normalisation: ΞΌ(X) is the identity operator.

hasSum' : βˆ€ (E : β„• β†’ Set X),
  (βˆ€ (j : β„•), MeasurableSet (E j)) β†’
    (Pairwise fun i j => Disjoint (E i) (E j)) β†’
      βˆ€ (v : H), HasSum (fun j => (self.toFun (E j)) v) ((self.toFun (⋃ j, E j)) v)

Countable additivity: for pairwise disjoint measurable sets E_j and every vector v, the series Ξ£ ΞΌ(E_j)v converges in the norm of H to ΞΌ(⋃ E_j)v.

inter' : βˆ€ (E F : Set X), MeasurableSet E β†’ MeasurableSet F β†’ self.toFun (E ∩ F) = self.toFun E * self.toFun F

Multiplicativity: μ(E ∩ F) = μ(E)μ(F) for measurable E and F.

πŸ”—def
Physicslib4.Spectral.ProjectionValuedMeasure.assoc.{u_1, u_2}
  {X : Type u_1} [MeasurableSpace X] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  (μ : ProjectionValuedMeasure X H) (ψ : H) : MeasureTheory.Measure X
Physicslib4.Spectral.ProjectionValuedMeasure.assoc.{u_1,
    u_2}
  {X : Type u_1} [MeasurableSpace X]
  {H : Type u_2} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H]
  (ΞΌ : ProjectionValuedMeasure X H)
  (ψ : H) : MeasureTheory.Measure X

The finite positive measure μ_ψ(E) = ⟨ψ, μ(E)ψ⟩ of a projection-valued measure μ and a vector ψ.

Since ΞΌ(E) is an orthogonal projection, ⟨ψ, ΞΌ(E)ψ⟩ = β€–ΞΌ(E)Οˆβ€–Β² β‰₯ 0, and countable additivity of ΞΌ makes E ↦ β€–ΞΌ(E)Οˆβ€–Β² a measure; its total mass is ⟨ψ, ψ⟩ = β€–Οˆβ€–Β², by assoc_apply with E = X. For a unit vector ψ and the spectral measure of an observable A, ΞΌ_ψ(E) is the probability that a measurement of A in the state ψ gives a value in E. The values on measurable sets are assoc_apply; the operator-valued integral satisfies ⟨ψ, (∫ f dΞΌ)ψ⟩ = ∫ f dΞΌ_ψ (inner_integral).

Implementation note: the measure is chosen from existsUnique_assoc, which also gives its uniqueness and finiteness (the MeasureTheory.IsFiniteMeasure instance).

Blueprint: the measure μ_ψ of thrm:projection-valued-measures-associated-measure

πŸ”—def
Physicslib4.Spectral.ProjectionValuedMeasure.integral.{u_1, u_2}
  {X : Type u_1} [MeasurableSpace X] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  (ΞΌ : ProjectionValuedMeasure X H) (f : X β†’ β„‚) : H β†’L[β„‚] H
Physicslib4.Spectral.ProjectionValuedMeasure.integral.{u_1,
    u_2}
  {X : Type u_1} [MeasurableSpace X]
  {H : Type u_2} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H]
  (ΞΌ : ProjectionValuedMeasure X H)
  (f : X β†’ β„‚) : H β†’L[β„‚] H

The operator-valued integral ∫ f dΞΌ of a bounded measurable f : X β†’ β„‚ against a projection-valued measure ΞΌ.

It is the bounded operator with ⟨ψ, (∫ f dΞΌ)ψ⟩ = ∫ f dΞΌ_ψ for every vector ψ (inner_integral), where ΞΌ_ψ(E) = ⟨ψ, ΞΌ(E)ψ⟩. For a step function f = Ξ£ c_k 1_(E_k) it is Ξ£ c_k ΞΌ(E_k), and in general a norm limit of such sums; the spectral theorem writes a self-adjoint operator as A = ∫ Ξ» dΞΌ^A(Ξ»). The integral of 1_E is ΞΌ(E) (integral_indicator), it is linear (integral_add, integral_smul) and multiplicative (integral_mul), satisfies β€–βˆ« f dΞΌβ€– ≀ sup |f| (norm_integral_le), and sends the complex conjugate fΜ„ to the adjoint (integral_conj).

Implementation note: the operator is chosen from the unique linear map of existsUnique_integral, built from the bounded quadratic form Q_f(ψ) = ∫ f dμ_ψ, so linearity is recovered by integral_add and integral_smul rather than definitional. On functions that are not bounded and measurable the integral is defined to be 0, so it is a total function.

Blueprint: the integral ∫ f dμ of thrm:operator-valued-integration

The integral comes from a unique linear map on the bounded measurable functions, characterised by its expectation values:

open Physicslib4 Spectral in Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_integral.{u_1, u_2} {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] (ΞΌ : ProjectionValuedMeasure X H) : βˆƒ! T, βˆ€ (f : β†₯(BddMeasurable X)) (ψ : H), inner β„‚ ψ ((T f) ψ) = ∫ (x : X), ↑f x βˆ‚ΞΌ.assoc ψ#check ProjectionValuedMeasure.existsUnique_integral 
Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_integral.{u_1, u_2} {X : Type u_1} [MeasurableSpace X]
  {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] (ΞΌ : ProjectionValuedMeasure X H) :
  βˆƒ! T, βˆ€ (f : β†₯(BddMeasurable X)) (ψ : H), inner β„‚ ψ ((T f) ψ) = ∫ (x : X), ↑f x βˆ‚ΞΌ.assoc ψ

Here T ranges over the β„‚-linear maps BddMeasurable X β†’β‚—[β„‚] (H β†’L[β„‚] H), ↑f is the function underlying an element of the subspace, and ΞΌ.assoc ψ is \mu_\psi. That Q_f(\psi) = \int f \, d\mu_\psi is a bounded quadratic form is proved in three stages, as in the blueprint: for indicator functions, for simple functions, and for bounded measurable functions as uniform limits of simple ones (isBoundedQuadraticForm_integral_bddMeasurable).

It is multiplicative, the operator form of \int fg \, d\mu = (\int f \, d\mu)(\int g \, d\mu):

open Physicslib4 Spectral in Physicslib4.Spectral.ProjectionValuedMeasure.integral_mul.{u_1, u_2} {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] (ΞΌ : ProjectionValuedMeasure X H) {f g : X β†’ β„‚} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : ΞΌ.integral (f * g) = ΞΌ.integral f * ΞΌ.integral g#check ProjectionValuedMeasure.integral_mul 
Physicslib4.Spectral.ProjectionValuedMeasure.integral_mul.{u_1, u_2} {X : Type u_1} [MeasurableSpace X] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] (ΞΌ : ProjectionValuedMeasure X H) {f g : X β†’ β„‚}
  (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : μ.integral (f * g) = μ.integral f * μ.integral g

The bound \|\int f \, d\mu\| \le \sup_x |f(x)| is norm_integral_le; its proof first establishes the weaker bound 6\sup_x |f(x)|, which it uses to pass to the limit of simple functions (formalization note of prpstn:integral-norm-bound). The identity \int \bar f \, d\mu = (\int f \, d\mu)^* is integral_conj. The measure \mu_\psi exists and is unique by existsUnique_assoc.

2.3.7.Β The Borel functional calculusπŸ”—

Blueprint: def:hall-8.6, prpstn:hall-8.7, def:F-class, def:hall-8.8, lmm:lemma-3, prpstn:hall-8.9, def:F1-F2-classes.

πŸ”—def
Physicslib4.Spectral.borelForm.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (f : ↑(spectrum ℝ A) β†’ β„‚)
  (ψ : H) : β„‚
Physicslib4.Spectral.borelForm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A)
  (f : ↑(spectrum ℝ A) β†’ β„‚) (ψ : H) : β„‚

The quadratic form Q_f(ψ) = ∫ f dμ_ψ of a function f on the spectrum of a self-adjoint A.

Here μ_ψ is the measure of assocMeasure, with ⟨ψ, g(A)ψ⟩ = ∫ g dμ_ψ for continuous real g. For a unit vector ψ, Q_f(ψ) is the expectation value of the observable f(A) in the state ψ: the average of f over the distribution μ_ψ of measured values of A. For bounded Borel f it is a bounded quadratic form (isBoundedQuadraticForm_borelForm), and the Borel functional calculus defines f(A) as the operator with ⟨ψ, f(A)ψ⟩ = Q_f(ψ).

Implementation note: the integral is the Bochner integral over Mathlib's real spectrum spectrum ℝ A; it is defined for every f, and is 0 when f is not integrable.

Blueprint: def:hall-8.6

Every bounded Borel function gives a bounded quadratic form, by the bootstrap applied to FClass:

open Physicslib4 Spectral in Physicslib4.Spectral.isBoundedQuadraticForm_borelForm.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f : ↑(spectrum ℝ A) β†’ β„‚} (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : IsBoundedQuadraticForm (borelForm hA f)#check isBoundedQuadraticForm_borelForm 
Physicslib4.Spectral.isBoundedQuadraticForm_borelForm.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f : ↑(spectrum ℝ A) β†’ β„‚}
  (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : IsBoundedQuadraticForm (borelForm hA f)
πŸ”—def
Physicslib4.Spectral.borelCalculus.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (f : ↑(spectrum ℝ A) β†’ β„‚) :
  H β†’L[β„‚] H
Physicslib4.Spectral.borelCalculus.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A)
  (f : ↑(spectrum ℝ A) β†’ β„‚) : H β†’L[β„‚] H

The bounded Borel functional calculus f ↦ f(A) of a self-adjoint bounded operator A.

For a bounded Borel function f on Οƒ(A), f(A) is the unique bounded operator with ⟨ψ, f(A)ψ⟩ = ∫ f dΞΌ_ψ for every vector ψ (inner_borelCalculus, existsUnique_borelCalculus). It extends the continuous calculus to discontinuous functions; most importantly, the indicator 1_E of a Borel set E gives the spectral projection 1_E(A), from which the spectral measure is built (spectralMeasure). The map is linear (borelCalculus_add, borelCalculus_smul) and multiplicative, (fg)(A) = f(A)g(A) (borelCalculus_mul), and f(A) is self-adjoint for real f (isSelfAdjoint_borelCalculus). On continuous real functions it agrees with realCalculus, and it is the integral against the spectral measure, f(A) = ∫ f dΞΌ^A (borelCalculus_eq_integral).

Implementation note: the operator is chosen from existsUnique_borelCalculus, whose proof takes IsBoundedQuadraticForm.toOperator of Q_f. On functions that are not bounded and measurable the value is defined to be 0 (borelCalculus_of_notMem). The agreement with realCalculus is proved as a private lemma of Physicslib4/Spectral/SpectralTheorem.lean.

Blueprint: def:hall-8.8

Multiplicativity, proved by the bootstrap twice, through the classes F1Class and F2Class:

open Physicslib4 Spectral in Physicslib4.Spectral.borelCalculus_mul.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) β†’ β„‚} (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) (hg : g ∈ BddMeasurable ↑(spectrum ℝ A)) : (borelCalculus hA fun l => f l * g l) = borelCalculus hA f * borelCalculus hA g#check borelCalculus_mul 
Physicslib4.Spectral.borelCalculus_mul.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) β†’ β„‚}
  (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) (hg : g ∈ BddMeasurable ↑(spectrum ℝ A)) :
  (borelCalculus hA fun l => f l * g l) = borelCalculus hA f * borelCalculus hA g

The first application shows that the bounded Borel f with (fg)(A) = f(A)g(A) for every continuous real g form a class satisfying IsBorelGenerating, starting from the multiplicativity of the continuous calculus. The second does the same for the g with (fg)(A) = f(A)g(A) for every bounded Borel f, starting from the first.

2.3.8.Β The spectral theoremπŸ”—

Blueprint: thrm:hall-8.10, prpstn:mua-projection to prpstn:mua-integrates-to-A, thrm:hall-prblm-8.3.4, thrm:spectral-theorem-for-bounded-operators, def:functional-calculus.

πŸ”—def
Physicslib4.Spectral.spectralMeasure.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) :
  ProjectionValuedMeasure (↑(spectrum ℝ A)) H
Physicslib4.Spectral.spectralMeasure.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A) :
  ProjectionValuedMeasure
    (↑(spectrum ℝ A)) H

The spectral measure ΞΌ^A of a self-adjoint bounded operator A: the projection-valued measure E ↦ 1_E(A) on the Borel sets of Οƒ(A).

Each ΞΌ^A(E) is the spectral projection of A for the set E: in finite dimensions, the projection onto the span of the eigenvectors whose eigenvalues lie in E. For a unit vector ψ, ⟨ψ, ΞΌ^A(E)ψ⟩ is the probability that a measurement of A in the state ψ gives a value in E. The spectral measure integrates the identity function to A, A = ∫ Ξ» dΞΌ^A(Ξ») (spectralMeasure_integral_id), and it is the only projection-valued measure on Οƒ(A) that does (existsUnique_spectralMeasure, the spectral theorem). Integrating a bounded Borel f against it gives f(A) (borelCalculus_eq_integral).

Implementation note: the definition takes 1_E(A) = borelCalculus hA (E.indicator 1) on measurable E and 0 otherwise (spectralMeasure_apply). The structure fields are discharged by the propositions prpstn:mua-projection, prpstn:mua-multiplicative, prpstn:mua-empty-and-whole and prpstn:mua-countably-additive. Οƒ(A) is Mathlib's real spectrum spectrum ℝ A.

Blueprint: the projection-valued measure ΞΌ^A of thrm:hall-8.10

The headline theorem of the section:

open Physicslib4 Spectral in Physicslib4.Spectral.existsUnique_spectralMeasure.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) : βˆƒ! ΞΌ, (ΞΌ.integral fun l => ↑↑l) = A#check existsUnique_spectralMeasure 
Physicslib4.Spectral.existsUnique_spectralMeasure.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) : βˆƒ! ΞΌ, (ΞΌ.integral fun l => ↑↑l) = A

Here ΞΌ ranges over ProjectionValuedMeasure (spectrum ℝ A) H, and the integrand is \lambda. The blueprint's form of the existence half, with \mu^A(E) = 1_E(A) on Borel sets, is exists_spectralMeasure. Existence is spectralMeasure_integral_id and uniqueness pvm_eq_of_integral_id_eq. The two Borel calculi agree:

open Physicslib4 Spectral in Physicslib4.Spectral.borelCalculus_eq_integral.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f : ↑(spectrum ℝ A) β†’ β„‚} (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : borelCalculus hA f = (spectralMeasure hA).integral f#check borelCalculus_eq_integral 
Physicslib4.Spectral.borelCalculus_eq_integral.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) {f : ↑(spectrum ℝ A) β†’ β„‚}
  (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : borelCalculus hA f = (spectralMeasure hA).integral f
πŸ”—def
Physicslib4.Spectral.functionalCalculus.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H]
  {A : H β†’L[β„‚] H} (hA : IsSelfAdjoint A) (f : ↑(spectrum ℝ A) β†’ β„‚) :
  H β†’L[β„‚] H
Physicslib4.Spectral.functionalCalculus.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace β„‚ H]
  [CompleteSpace H] {A : H β†’L[β„‚] H}
  (hA : IsSelfAdjoint A)
  (f : ↑(spectrum ℝ A) β†’ β„‚) : H β†’L[β„‚] H

The functional calculus f(A) = ∫ f dΞΌ^A of a self-adjoint bounded operator A, for bounded Borel f on Οƒ(A).

This is the standard meaning of a function of an observable: in finite dimensions f(A) = Ξ£_k f(Ξ»_k) P_k. For example, the indicator of E gives the spectral projection ΞΌ^A(E), and f(Ξ») = e^(iΞ»t) gives the operator written e^(itA). By borelCalculus_eq_integral it agrees with the operator borelCalculus obtained from the quadratic form Q_f, so the notation f(A) is unambiguous, and the properties proved for borelCalculus (linearity, multiplicativity, self-adjointness for real f) transfer to it through that equation.

Implementation note: the definition is (spectralMeasure hA).integral f, so it is 0 on functions that are not bounded and measurable.

Blueprint: def:functional-calculus

2.4.Β Where to lookπŸ”—

The section is formalised in the top-level files of Physicslib4/Spectral/, one topic per file. Each entry links to the API documentation of a representative declaration, from which the rest of the file can be browsed.

  • Basic.lean: the prerequisites about bounded operators that Mathlib does not state in the blueprint's form, bounded measurable functions, the resolvent in the blueprint's sign convention, and the bounded convergence theorem, BddMeasurable. Its module documentation lists the blueprint entries that are Mathlib declarations.

  • Spectrum.lean: compactness and nonemptiness of the spectrum, the resolvent as a power series, and the reality of the spectrum of a self-adjoint operator, spectrum_subset_real.

  • ContinuousCalculus.lean: the continuous functional calculus and the associated measures, realCalculus.

  • Forms.lean: sesquilinear and quadratic forms, polarization, and the operator of a bounded quadratic form, existsUnique_operator_of_isBoundedQuadraticForm.

  • BorelClasses.lean: bump functions, the monotone class theorem, \mathcal{L}_0 and the bootstrap, IsBorelGenerating.

  • ProjectionValuedMeasure.lean: projection-valued measures, their associated measures, and sums of orthogonal projections, ProjectionValuedMeasure.

  • OperatorIntegral.lean: the operator-valued integral and its properties, ProjectionValuedMeasure.integral.

  • BorelCalculus.lean: the quadratic forms Q_f, the Borel functional calculus and its multiplicativity, borelCalculus.

  • SpectralTheorem.lean: the spectral measure, uniqueness, the spectral theorem and the functional calculus, existsUnique_spectralMeasure.

The subdirectories Unbounded/ and Stone/ formalise Sections 10.3 and 10.4 of the blueprint. The blueprint section is Section 10.2, and each entry there links to the Lean declarations that formalise it.