Physicslib4.Spectral.SpectralTheorem

The spectral theorem for bounded self-adjoint operators

The projections μ^A(E) ≡ 1_E(A) of the bounded Borel functional calculus assemble into a projection-valued measure on σ(A) which integrates the identity function to A, and it is the unique projection-valued measure with that property.

Main definitions

• Physicslib4.Spectral.spectralMeasure — the projection-valued measure μ^A.
• Physicslib4.Spectral.functionalCalculus — f(A) = ∫ f dμ^A.

Main statements

• Physicslib4.Spectral.spectralMeasure_integral_id — ∫ λ dμ^A(λ) = A.
• Physicslib4.Spectral.borelCalculus_eq_integral — the two constructions of f(A) agree.
• Physicslib4.Spectral.existsUnique_spectralMeasure — the spectral theorem, proved from spectralMeasure_integral_id and pvm_eq_of_integral_id_eq.

Implementation notes

As in Physicslib4/Spectral/ContinuousCalculus.lean, the blueprint's σ(A) ⊆ ℂ is represented by Mathlib's real spectrum spectrum ℝ A, which for self-adjoint A is homeomorphic to it via Complex.ofReal; the blueprint's ∫ λ dμ^A(λ) is therefore the integral of fun l => ((l : ℝ) : ℂ).

The projections μ^A(E) = 1_E(A)

theorem Physicslib4.Spectral.isStarProjection_borelCalculus_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {E : Set ↑(spectrum ℝ A)} (hE : MeasurableSet E) : IsStarProjection (borelCalculus hA (E.indicator 1))

Each μ^A(E) = 1_E(A) is a bounded orthogonal projection.

Blueprint reference: prpstn:mua-projection.

theorem Physicslib4.Spectral.borelCalculus_indicator_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {E₁ E₂ : Set ↑(spectrum ℝ A)} (hE₁ : MeasurableSet E₁) (hE₂ : MeasurableSet E₂) : borelCalculus hA (E₁.indicator 1) * borelCalculus hA (E₂.indicator 1) = borelCalculus hA ((E₁ ∩ E₂).indicator 1)

μ^A is multiplicative: μ^A(E₁) μ^A(E₂) = μ^A(E₁ ∩ E₂).

Blueprint reference: prpstn:mua-multiplicative.

theorem Physicslib4.Spectral.borelCalculus_indicator_empty {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : borelCalculus hA (∅.indicator 1) = 0

μ^A(∅) = 0.

Blueprint reference: prpstn:mua-empty-and-whole (first part).

theorem Physicslib4.Spectral.borelCalculus_indicator_univ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : borelCalculus hA (Set.univ.indicator 1) = 1

μ^A(σ(A)) = 1.

Blueprint reference: prpstn:mua-empty-and-whole (second part).

theorem Physicslib4.Spectral.hasSum_borelCalculus_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (E : ℕ → Set ↑(spectrum ℝ A)) (hE : ∀ (j : ℕ), MeasurableSet (E j)) (hdisj : Pairwise fun (i j : ℕ) => Disjoint (E i) (E j)) (ψ : H) : HasSum (fun (j : ℕ) => (borelCalculus hA ((E j).indicator 1)) ψ) ((borelCalculus hA ((⋃ (j : ℕ), E j).indicator 1)) ψ)

μ^A is countably additive in the norm topology of H.

Blueprint reference: prpstn:mua-countably-additive.

The spectral measure

noncomputable def Physicslib4.Spectral.spectralMeasure {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

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.Spectral.spectralMeasure_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {E : Set ↑(spectrum ℝ A)} (hE : MeasurableSet E) : (spectralMeasure hA) E = borelCalculus hA (E.indicator 1)

theorem Physicslib4.Spectral.spectralMeasure_integral_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {E : Set ↑(spectrum ℝ A)} (hE : MeasurableSet E) : (spectralMeasure hA).integral (E.indicator 1) = (spectralMeasure hA) E

The integral of an indicator against μ^A recovers μ^A(E).

This is ProjectionValuedMeasure.integral_indicator specialised to μ^A.

Blueprint reference: prpstn:mua-indicator-integral.

theorem Physicslib4.Spectral.borelCalculus_eq_integral {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

The two constructions of f(A) — from the quadratic form Q_f, and as the projection-valued integral of f against μ^A — agree.

Blueprint reference: prpstn:mua-bounded-calculus-agrees.

theorem Physicslib4.Spectral.spectralMeasure_integral_id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : ((spectralMeasure hA).integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A

∫ λ dμ^A(λ) = A.

Blueprint reference: prpstn:mua-integrates-to-A.

theorem Physicslib4.Spectral.exists_spectralMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : ∃ (μ : ProjectionValuedMeasure (↑(spectrum ℝ A)) H), (∀ (E : Set ↑(spectrum ℝ A)), MeasurableSet E → μ E = borelCalculus hA (E.indicator 1)) ∧ (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A

The projections μ^A(E) = 1_E(A) form a projection-valued measure on σ(A) which integrates the identity function to A.

Both halves have already been established — the first by the construction of spectralMeasure, the second by spectralMeasure_integral_id — so this blueprint node is proved rather than restated.

Blueprint reference: thrm:hall-8.10.

Uniqueness

theorem Physicslib4.Spectral.pvm_integral_polynomial_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (μ ν : ProjectionValuedMeasure (↑(spectrum ℝ A)) H) (hμ : (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (hν : (ν.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (p : Polynomial ℂ) : (μ.integral fun (l : ↑(spectrum ℝ A)) => Polynomial.eval (↑↑l) p) = ν.integral fun (l : ↑(spectrum ℝ A)) => Polynomial.eval (↑↑l) p

Two projection-valued measures on σ(A) integrating the identity to A agree on polynomials.

Blueprint reference: prpstn:pvm-agree-on-polynomials.

theorem Physicslib4.Spectral.pvm_integral_continuous_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (μ ν : ProjectionValuedMeasure (↑(spectrum ℝ A)) H) (hμ : (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (hν : (ν.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (g : C(↑(spectrum ℝ A), ℂ)) : (μ.integral fun (l : ↑(spectrum ℝ A)) => g l) = ν.integral fun (l : ↑(spectrum ℝ A)) => g l

Two projection-valued measures on σ(A) integrating the identity to A agree on continuous functions.

Blueprint reference: prpstn:pvm-agree-on-continuous.

theorem Physicslib4.Spectral.pvm_integral_bddMeasurable_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (μ ν : ProjectionValuedMeasure (↑(spectrum ℝ A)) H) (hμ : (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (hν : (ν.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) {f : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : μ.integral f = ν.integral f

Two projection-valued measures on σ(A) integrating the identity to A agree on all bounded Borel functions.

Blueprint reference: prpstn:pvm-agree-on-measurable.

theorem Physicslib4.Spectral.pvm_eq_of_integral_id_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (μ ν : ProjectionValuedMeasure (↑(spectrum ℝ A)) H) (hμ : (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (hν : (ν.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A) (E : Set ↑(spectrum ℝ A)) : MeasurableSet E → μ E = ν E

A projection-valued measure on σ(A) integrating the identity to A is unique.

Blueprint reference: thrm:hall-prblm-8.3.4.

theorem Physicslib4.Spectral.existsUnique_spectralMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : ∃! μ : ProjectionValuedMeasure (↑(spectrum ℝ A)) H, (μ.integral fun (l : ↑(spectrum ℝ A)) => ↑↑l) = A

The spectral theorem: a self-adjoint bounded A has a unique projection-valued measure μ^A on σ(A) with ∫ λ dμ^A(λ) = A.

This is the infinite-dimensional form of diagonalising a Hermitian matrix, A = Σ_k λ_k P_k with P_k the eigenprojections: the sum over eigenvalues becomes an integral over the spectrum against projection-valued weights, which also covers continuous spectrum. The measure μ^A is spectralMeasure.

Implementation note: existence is spectralMeasure_integral_id and uniqueness is pvm_eq_of_integral_id_eq. σ(A) is Mathlib's real spectrum spectrum ℝ A with its Borel σ-algebra, and λ is the function l ↦ (l : ℂ).

Blueprint: thrm:spectral-theorem-for-bounded-operators

noncomputable def Physicslib4.Spectral.functionalCalculus {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

Equations

• Physicslib4.Spectral.functionalCalculus hA f = (Physicslib4.Spectral.spectralMeasure hA).integral f