Physicslib4.Spectral.ContinuousCalculus

The real-valued continuous functional calculus

For a self-adjoint A ∈ 𝓑(H) the blueprint builds a bounded linear map C⁰(σ(A); ℝ) → 𝓑(H), f ↦ f(A), extending p ↦ p(A) on real polynomials, and then represents each ψ ↦ ⟪ψ, f(A) ψ⟫ as an integral against a finite positive measure μ_ψ on σ(A).

Implementation notes

The blueprint's σ(A) is a subset of ℂ which, for self-adjoint A, is contained in ℝ (Physicslib4.Spectral.spectrum_subset_real). We use Mathlib's real spectrum spectrum ℝ A throughout this file, which is the canonical Lean shape (it is the index type of Mathlib's cfcHom) and is homeomorphic to the blueprint's σ(A) via Complex.ofReal.

Main definitions

• Physicslib4.Spectral.polyOn — a real polynomial restricted to σ(A).
• Physicslib4.Spectral.realCalculus — the real-valued continuous functional calculus f ↦ f(A). This is Mathlib's cfcHom: H →L[ℂ] H is a C⋆-algebra, so the continuous functional calculus is already available and there is no reason to rebuild it. Its StarAlgHom type also carries the multiplicativity and *-compatibility that the blueprint's prpstn:hall-8.4 asserts separately.
• Physicslib4.Spectral.assocMeasure — the finite positive measure μ_ψ on σ(A).

Main statements

• Physicslib4.Spectral.existsUnique_realCalculus — existence and uniqueness of the functional calculus.
• Physicslib4.Spectral.realCalculus_properties — multiplicativity, self-adjointness, positivity, the norm identity and the spectral mapping theorem.
• Physicslib4.Spectral.existsUnique_assocMeasure — the Riesz representation of f ↦ ⟪ψ, f(A) ψ⟫.

Prerequisites

theorem Physicslib4.Spectral.existsUnique_measure_of_positive_linear {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), (∀ (x : X), 0 ≤ f x) → 0 ≤ Λ f) : ∃! ν : MeasureTheory.Measure X, MeasureTheory.IsFiniteMeasure ν ∧ ∀ (f : C(X, ℝ)), ∫ (x : X), f x ∂ν = Λ f

Riesz representation theorem. A positive linear functional on the continuous real-valued functions on a compact metric space is integration against a unique finite positive Borel measure.

Blueprint reference: thrm:riesz-representation.

theorem Physicslib4.Spectral.existsUnique_extension_of_dense {V₁ : Type u_2} {V₂ : Type u_3} [NormedAddCommGroup V₁] [NormedSpace ℂ V₁] [NormedAddCommGroup V₂] [NormedSpace ℂ V₂] [CompleteSpace V₂] (W : Submodule ℂ V₁) (hW : Dense ↑W) (T : ↥W →L[ℂ] V₂) : ∃! S : V₁ →L[ℂ] V₂, (∀ (w : ↥W), S ↑w = T w) ∧ ‖S‖ = ‖T‖

Bounded linear transformation theorem. A bounded linear map defined on a dense subspace of a normed space, with values in a Banach space, extends uniquely to a bounded linear map of the same norm.

This is Mathlib's LinearMap.extendOfNorm together with its API (LinearMap.extendOfNorm_eq, LinearMap.opNorm_extendOfNorm_le).

Blueprint reference: thrm:bounded-linear-transformation-theorem.

theorem Physicslib4.Spectral.dense_polynomial_spectrum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : Dense {f : C(↑(spectrum ℝ A), ℂ) | ∃ (p : Polynomial ℂ), ∀ (l : ↑(spectrum ℝ A)), f l = Polynomial.eval (↑↑l) p}

The complex polynomials are dense in the continuous complex-valued functions on the real spectrum of a bounded operator, for the supremum norm.

Self-adjointness of A is not needed: this is Stone–Weierstrass for the compact subset spectrum ℝ A of ℝ, and holds for every A. The blueprint states it for self-adjoint A only because that is where it is applied.

Blueprint reference: lmm:lemma-5.

The functional calculus

noncomputable def Physicslib4.Spectral.polyOn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (p : Polynomial ℝ) : C(↑(spectrum ℝ A), ℝ)

A real polynomial p restricted to the spectrum of A, as a continuous real function on σ(A).

The continuous functional calculus is pinned down by its values on these functions: it must send the restriction of p to the operator p(A) = a₀𝟙 + a₁A + ⋯ + a_n Aⁿ (realCalculus_polyOn), and these restrictions are dense in C⁰(σ(A); ℝ) by the Weierstrass approximation theorem.

Implementation note: σ(A) here is Mathlib's real spectrum spectrum ℝ A, and the function is l ↦ p(l) bundled as a ContinuousMap.

Blueprint: the restricted polynomials of prpstn:hall-8.3

Equations

• Physicslib4.Spectral.polyOn A p = { toFun := fun (l : ↑(spectrum ℝ A)) => Polynomial.eval (↑l) p, continuous_toFun := ⋯ }

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

Equations

• Physicslib4.Spectral.realCalculus hA = cfcHom hA

theorem Physicslib4.Spectral.realCalculus_polyOn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (p : Polynomial ℝ) : (realCalculus hA) (polyOn A p) = (Polynomial.aeval A) p

realCalculus extends the evaluation of real polynomials at A: this is the defining property of the map whose existence and uniqueness existsUnique_realCalculus asserts.

Blueprint reference: prpstn:hall-8.3 (the defining property).

theorem Physicslib4.Spectral.existsUnique_realCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : ∃! T : C(↑(spectrum ℝ A), ℝ) →L[ℝ] H →L[ℂ] H, ∀ (p : Polynomial ℝ), T (polyOn A p) = (Polynomial.aeval A) p

The real-valued functional calculus. For self-adjoint A there is a unique bounded ℝ-linear map C⁰(σ(A); ℝ) → 𝓑(H) which sends a real polynomial p to p(A).

Existence is realCalculus, i.e. cfcHom hA, made continuous by the isometry norm_cfcHom; uniqueness is Stone–Weierstrass, in the form polynomialFunctions.topologicalClosure.

Blueprint reference: prpstn:hall-8.3.

theorem Physicslib4.Spectral.realCalculus_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (f g : C(↑(spectrum ℝ A), ℝ)) : (realCalculus hA) (f * g) = (realCalculus hA) f * (realCalculus hA) g

Multiplicativity of the real-valued functional calculus.

Blueprint reference: prpstn:cfc-multiplicative.

theorem Physicslib4.Spectral.isSelfAdjoint_realCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) : IsSelfAdjoint ((realCalculus hA) f)

The functional calculus of a real-valued continuous function is self-adjoint.

Blueprint reference: prpstn:cfc-self-adjoint.

theorem Physicslib4.Spectral.isPositive_realCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) (hf : ∀ (l : ↑(spectrum ℝ A)), 0 ≤ f l) : ((realCalculus hA) f).IsPositive

The functional calculus of a non-negative continuous function is a non-negative bounded operator.

Blueprint reference: prpstn:cfc-non-negative.

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

The functional calculus is isometric for the supremum norm.

Blueprint reference: prpstn:cfc-norm.

theorem Physicslib4.Spectral.spectrum_realCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) : spectrum ℝ ((realCalculus hA) f) = Set.range ⇑f

The spectral mapping theorem for the continuous functional calculus.

Blueprint reference: prpstn:cfc-spectral-mapping.

theorem Physicslib4.Spectral.realCalculus_properties {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : (∀ (f g : C(↑(spectrum ℝ A), ℝ)), (realCalculus hA) (f * g) = (realCalculus hA) f * (realCalculus hA) g) ∧ (∀ (f : C(↑(spectrum ℝ A), ℝ)), IsSelfAdjoint ((realCalculus hA) f)) ∧ (∀ (f : C(↑(spectrum ℝ A), ℝ)), (∀ (l : ↑(spectrum ℝ A)), 0 ≤ f l) → ((realCalculus hA) f).IsPositive) ∧ (∀ (f : C(↑(spectrum ℝ A), ℝ)), ‖(realCalculus hA) f‖ = ‖f‖) ∧ ∀ (f : C(↑(spectrum ℝ A), ℝ)), spectrum ℝ ((realCalculus hA) f) = Set.range ⇑f

The five properties of the real-valued functional calculus: multiplicativity, self-adjointness, non-negativity, and the norm and spectrum identities.

This blueprint node is exactly the conjunction of the five statements above, so it is proved from them rather than restated.

Blueprint reference: prpstn:hall-8.4.

The associated scalar measures

noncomputable def Physicslib4.Spectral.assocFunctional {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (ψ : H) : CompactlySupportedContinuousMap ↑(spectrum ℝ A) ℝ →ₚ[ℝ] ℝ

The positive linear functional Λ_ψ(f) = ⟨ψ, f(A)ψ⟩ on continuous real functions on σ(A).

For a unit vector ψ, Λ_ψ(f) is the quantum expectation value of the observable f(A) in the state ψ. It is linear in f, real because f(A) is self-adjoint, and non-negative for f ≥ 0 because f(A) is then a non-negative operator (isPositive_realCalculus). The Riesz–Markov–Kakutani theorem makes it integration against a measure, assocMeasure.

Implementation note: the functional is the real part of ⟨ψ, f(A)ψ⟩, bundled as a positive linear map on CompactlySupportedContinuousMap (spectrum ℝ A) ℝ, the domain of Mathlib's RealRMK.rieszMeasure; since σ(A) is compact, every continuous function on it is compactly supported.

Blueprint: the functional Λ_ψ of prpstn:associated-measures-self-adjoint

Equations

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

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

Equations

• Physicslib4.Spectral.assocMeasure hA ψ = RealRMK.rieszMeasure (Physicslib4.Spectral.assocFunctional hA ψ)

instance Physicslib4.Spectral.instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdAssocMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (ψ : H) : MeasureTheory.IsFiniteMeasure (assocMeasure hA ψ)

theorem Physicslib4.Spectral.integral_assocMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (ψ : H) (f : C(↑(spectrum ℝ A), ℝ)) : inner ℂ ψ (((realCalculus hA) f) ψ) = ↑(∫ (l : ↑(spectrum ℝ A)), f l ∂assocMeasure hA ψ)

theorem Physicslib4.Spectral.existsUnique_assocMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (ψ : H) : ∃! ν : MeasureTheory.Measure ↑(spectrum ℝ A), MeasureTheory.IsFiniteMeasure ν ∧ ∀ (f : C(↑(spectrum ℝ A), ℝ)), inner ℂ ψ (((realCalculus hA) f) ψ) = ↑(∫ (l : ↑(spectrum ℝ A)), f l ∂ν)

For self-adjoint A and every ψ ∈ H there is a unique finite positive Borel measure μ_ψ on σ(A) with ⟪ψ, f(A) ψ⟫ = ∫ f dμ_ψ for all continuous real f.

Existence is assocMeasure together with integral_assocMeasure; uniqueness is Measure.ext_of_integral_eq_on_compactlySupported, the uniqueness half of Riesz–Markov–Kakutani.

Blueprint reference: prpstn:associated-measures-self-adjoint.

theorem Physicslib4.Spectral.assocMeasure_univ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (ψ : H) : (assocMeasure hA ψ) Set.univ = ENNReal.ofReal (‖ψ‖ ^ 2)

The total mass of μ_ψ is ‖ψ‖²; in particular μ_ψ is a finite measure.

Blueprint reference: lmm:associated-measures-are-finite.