Physicslib4.Spectral.BorelCalculus

The bounded Borel functional calculus

For a self-adjoint A ∈ 𝓑(H) and a bounded Borel function f on σ(A), the map Q_f : ψ ↦ ∫ f dμ_ψ is a bounded quadratic form, hence of the form ψ ↦ ⟪ψ, f(A) ψ⟫ for a unique f(A) ∈ 𝓑(H). This is the blueprint's second functional calculus, def:hall-8.8, and it is multiplicative.

Main definitions

• Physicslib4.Spectral.borelForm — the blueprint's Q_f.
• Physicslib4.Spectral.FClass — the blueprint's 𝓕.
• Physicslib4.Spectral.borelCalculus — the blueprint's f ↦ f(A).
• Physicslib4.Spectral.F1Class, Physicslib4.Spectral.F2Class — the blueprint's 𝓕₁ and 𝓕₂.

Main statements

• Physicslib4.Spectral.isBoundedQuadraticForm_borelForm — Q_f is a bounded quadratic form.
• Physicslib4.Spectral.existsUnique_borelCalculus — the operator f(A).
• Physicslib4.Spectral.borelCalculus_add, Physicslib4.Spectral.borelCalculus_smul — linearity of f ↦ f(A).
• Physicslib4.Spectral.borelCalculus_mul — multiplicativity of the calculus.
• Physicslib4.Spectral.isBorelGenerating_F1Class, Physicslib4.Spectral.isBorelGenerating_F2Class — 𝓕₁ and 𝓕₂ satisfy the hypotheses of the monotone-class bootstrap of Physicslib4/Spectral/BorelClasses.lean, from which 𝓕₁ = 𝓕₂ = {bounded Borel} follows.

Supporting lemmas

• Physicslib4.Spectral.borelCalculus_of_notMem — the degenerate case: the junk value of borelCalculus off its domain of definition is 0.

Implementation notes

"Bounded Borel function on σ(A)" is spelled f ∈ BddMeasurable (spectrum ℝ A) throughout, using the submodule defined in Physicslib4/Spectral/Basic.lean, rather than a Measurable f/bounded hypothesis pair.

The quadratic forms Q_f

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

Equations

• Physicslib4.Spectral.borelForm hA f ψ = ∫ (l : ↑(spectrum ℝ A)), f l ∂Physicslib4.Spectral.assocMeasure hA ψ

def Physicslib4.Spectral.FClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : Set (↑(spectrum ℝ A) → ℂ)

The class 𝓕 of bounded Borel functions f on σ(A) whose quadratic form Q_f is bounded.

It is the class of the bootstrap that proves Q_f bounded for every bounded Borel f: 𝓕 is a complex subspace (smul_add_mem_FClass), contains the continuous real functions (continuous_mem_FClass; for them Q_f(ψ) = ⟨ψ, f(A)ψ⟩), and is closed under bounded pointwise limits (mem_FClass_of_tendsto). So it satisfies IsBorelGenerating, and is therefore every bounded Borel function; the proof of isBoundedQuadraticForm_borelForm makes this argument.

Implementation note: 𝓕 is unrelated to the classes 𝓕₁ and 𝓕₂ (F1Class, F2Class), which concern multiplicativity.

Blueprint: def:F-class

Equations

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

theorem Physicslib4.Spectral.borelForm_add {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)) (ψ : H) : borelForm hA (f + g) ψ = borelForm hA f ψ + borelForm hA g ψ

f ↦ Q_f is additive in f.

Blueprint reference: prpstn:Q-is-linear (additivity).

theorem Physicslib4.Spectral.borelForm_smul {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)) (ψ : H) : borelForm hA (α • f) ψ = α * borelForm hA f ψ

f ↦ Q_f is homogeneous in f.

Blueprint reference: prpstn:Q-is-linear (homogeneity).

theorem Physicslib4.Spectral.borelForm_smul_of_mem_FClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ FClass hA) (hg : g ∈ FClass hA) (α β l : ℂ) (ψ : H) : borelForm hA (α • f + β • g) (l • ψ) = ↑‖l‖ ^ 2 * borelForm hA (α • f + β • g) ψ

The quadratic form of a linear combination of members of 𝓕 is |λ|²-homogeneous.

Blueprint reference: prpstn:F-homogeneous.

theorem Physicslib4.Spectral.isSesquilinearForm_polarization_borelForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ FClass hA) (hg : g ∈ FClass hA) (α β : ℂ) : ∃ (L : SesquilinearForm H), ∀ (φ ψ : H), (L φ) ψ = polarization (borelForm hA (α • f + β • g)) φ ψ

The polarization of the quadratic form of a linear combination of members of 𝓕 is sesquilinear.

Blueprint reference: prpstn:F-sesquilinear.

theorem Physicslib4.Spectral.bounded_borelForm_of_mem_FClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ FClass hA) (hg : g ∈ FClass hA) (α β : ℂ) : ∃ (C : ℝ), ∀ (φ : H), ‖borelForm hA (α • f + β • g) φ‖ ≤ C * ‖φ‖ ^ 2

The quadratic form of a linear combination of members of 𝓕 is bounded.

Blueprint reference: prpstn:F-bounded (the closure property).

theorem Physicslib4.Spectral.smul_add_mem_FClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f g : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ FClass hA) (hg : g ∈ FClass hA) (α β : ℂ) : α • f + β • g ∈ FClass hA

𝓕 is a complex vector space.

This is the blueprint's "consequently" half of prpstn:F-bounded; it assembles borelForm_smul_of_mem_FClass, isSesquilinearForm_polarization_borelForm and bounded_borelForm_of_mem_FClass.

Blueprint reference: prpstn:F-bounded (the global consequence).

theorem Physicslib4.Spectral.continuous_mem_FClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (f : C(↑(spectrum ℝ A), ℝ)) : (fun (l : ↑(spectrum ℝ A)) => ↑(f l)) ∈ FClass hA

𝓕 contains the continuous real-valued functions on σ(A).

Blueprint reference: prpstn:F-contains-continuous.

theorem Physicslib4.Spectral.mem_FClass_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f : ℕ → ↑(spectrum ℝ A) → ℂ} {g : ↑(spectrum ℝ A) → ℂ} {M : ℝ} (hf : ∀ (n : ℕ), f n ∈ FClass hA) (hlim : BoundedPointwiseLimit f g fun (x : ↑(spectrum ℝ A)) => M) : g ∈ FClass hA

𝓕 is closed under pointwise limits of uniformly bounded sequences.

Blueprint reference: prpstn:F-closed-under-limits.

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

For every bounded Borel function f on σ(A), the map Q_f is a bounded quadratic form on H.

Blueprint reference: prpstn:hall-8.7.

The operators f(A)

theorem Physicslib4.Spectral.existsUnique_borelCalculus {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)) : ∃! B : H →L[ℂ] H, ∀ (ψ : H), inner ℂ ψ (B ψ) = borelForm hA f ψ

The bounded Borel functional calculus. For a bounded Borel function f on σ(A) there is a unique f(A) ∈ 𝓑(H) with ⟪ψ, f(A) ψ⟫ = Q_f(ψ) for all ψ.

Blueprint reference: def:hall-8.8.

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

Equations

• Physicslib4.Spectral.borelCalculus hA f = if h : f ∈ Physicslib4.Spectral.BddMeasurable ↑(spectrum ℝ A) then Exists.choose ⋯ else 0

theorem Physicslib4.Spectral.inner_borelCalculus {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)) (ψ : H) : inner ℂ ψ ((borelCalculus hA f) ψ) = borelForm hA f ψ

theorem Physicslib4.Spectral.borelCalculus_of_notMem {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 = 0

Linearity of the calculus

borelCalculus is defined through Exists.choose, so its linearity in f is not definitional. The two computation rules below are what the vector-space fields of isBorelGenerating_F1Class and isBorelGenerating_F2Class consume; together they say that f ↦ f(A) restricts to a ℂ-linear map on BddMeasurable (spectrum ℝ A).

theorem Physicslib4.Spectral.borelCalculus_add {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 (f + g) = borelCalculus hA f + borelCalculus hA g

Additivity of the bounded Borel functional calculus.

Blueprint reference: def:hall-8.8 (linearity of f ↦ f(A)).

theorem Physicslib4.Spectral.borelCalculus_smul {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) = α • borelCalculus hA f

Homogeneity of the bounded Borel functional calculus.

Blueprint reference: def:hall-8.8 (linearity of f ↦ f(A)).

theorem Physicslib4.Spectral.isSelfAdjoint_borelCalculus {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)) (hreal : ∀ (l : ↑(spectrum ℝ A)), (f l).im = 0) : IsSelfAdjoint (borelCalculus hA f)

If f is real-valued then f(A) is self-adjoint.

Blueprint reference: lmm:lemma-3.

The classes 𝓕₁ and 𝓕₂

def Physicslib4.Spectral.F1Class {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : Set (↑(spectrum ℝ A) → ℂ)

The class 𝓕₁ of bounded Borel f on σ(A) with (fg)(A) = f(A)g(A) for every continuous real g.

It is the first step of the proof that the Borel functional calculus is multiplicative. The class contains the continuous real functions, by multiplicativity of the continuous calculus, and satisfies IsBorelGenerating (isBorelGenerating_F1Class), so it is every bounded Borel function (F1Class_eq_bddMeasurable).

Blueprint: def:F1-F2-classes

Equations

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

def Physicslib4.Spectral.F2Class {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : Set (↑(spectrum ℝ A) → ℂ)

The class 𝓕₂ of bounded Borel g on σ(A) with (fg)(A) = f(A)g(A) for every bounded Borel f.

It is the second step of the proof that the Borel functional calculus is multiplicative. By 𝓕₁ = all bounded Borel functions, 𝓕₂ contains the continuous real functions; it satisfies IsBorelGenerating (isBorelGenerating_F2Class), so it is every bounded Borel function (F2Class_eq_bddMeasurable), which is borelCalculus_mul.

Blueprint: def:F1-F2-classes

Equations

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

theorem Physicslib4.Spectral.isBorelGenerating_F1Class {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : IsBorelGenerating (F1Class hA)

𝓕₁ satisfies the blueprint's bootstrap hypotheses: it consists of bounded Borel functions, is a complex subspace, contains the continuous real-valued functions on σ(A), and is closed under uniformly bounded pointwise limits.

The first three of these are prpstn:F1-vector-space, the last is prpstn:F1-closed-under-limits; they are packaged as IsBorelGenerating because that is exactly what the monotone-class bootstrap of Physicslib4/Spectral/BorelClasses.lean consumes.

Blueprint reference: prpstn:F1-vector-space.

theorem Physicslib4.Spectral.tendsto_borelForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f : ℕ → ↑(spectrum ℝ A) → ℂ} {g : ↑(spectrum ℝ A) → ℂ} {M : ℝ} (hmeas : ∀ (n : ℕ), Measurable (f n)) (hlim : BoundedPointwiseLimit f g fun (x : ↑(spectrum ℝ A)) => M) (ψ : H) : Filter.Tendsto (fun (n : ℕ) => borelForm hA (f n) ψ) Filter.atTop (nhds (borelForm hA g ψ))

Q_f is continuous under uniformly bounded pointwise limits of the integrand.

Blueprint reference: prpstn:Q-continuous-under-limits (first part).

theorem Physicslib4.Spectral.tendsto_polarization_borelForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f : ℕ → ↑(spectrum ℝ A) → ℂ} {g : ↑(spectrum ℝ A) → ℂ} {M : ℝ} (hmeas : ∀ (n : ℕ), Measurable (f n)) (hlim : BoundedPointwiseLimit f g fun (x : ↑(spectrum ℝ A)) => M) (φ ψ : H) : Filter.Tendsto (fun (n : ℕ) => polarization (borelForm hA (f n)) φ ψ) Filter.atTop (nhds (polarization (borelForm hA g) φ ψ))

The polarization of Q_f is continuous under uniformly bounded pointwise limits of the integrand.

Blueprint reference: prpstn:Q-continuous-under-limits (second part).

theorem Physicslib4.Spectral.mem_F1Class_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {f : ℕ → ↑(spectrum ℝ A) → ℂ} {g : ↑(spectrum ℝ A) → ℂ} {M : ℝ} (hf : ∀ (n : ℕ), f n ∈ F1Class hA) (hlim : BoundedPointwiseLimit f g fun (x : ↑(spectrum ℝ A)) => M) : g ∈ F1Class hA

𝓕₁ is closed under uniformly bounded pointwise limits.

Blueprint reference: prpstn:F1-closed-under-limits (the closure property).

theorem Physicslib4.Spectral.F1Class_eq_bddMeasurable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : F1Class hA = ↑(BddMeasurable ↑(spectrum ℝ A))

𝓕₁ is the set of all bounded Borel functions on σ(A).

This is the blueprint's "consequently" half of prpstn:F1-closed-under-limits; it has no hypotheses beyond self-adjointness of A and follows from the bootstrap lemma IsBorelGenerating.eq_bddMeasurable.

Blueprint reference: prpstn:F1-closed-under-limits (the global consequence).

theorem Physicslib4.Spectral.isBorelGenerating_F2Class {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : IsBorelGenerating (F2Class hA)

𝓕₂ satisfies the blueprint's bootstrap hypotheses: it consists of bounded Borel functions, is a complex subspace, contains the continuous real-valued functions on σ(A), and is closed under uniformly bounded pointwise limits.

Blueprint reference: prpstn:F2-is-everything (hypotheses (1)–(3)).

theorem Physicslib4.Spectral.F2Class_eq_bddMeasurable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : F2Class hA = ↑(BddMeasurable ↑(spectrum ℝ A))

𝓕₂ is the set of all bounded Borel functions on σ(A).

Blueprint reference: prpstn:F2-is-everything.

theorem Physicslib4.Spectral.borelCalculus_mul {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 : ↑(spectrum ℝ A)) => f l * g l) = borelCalculus hA f * borelCalculus hA g

Multiplicativity of the bounded Borel functional calculus.

Blueprint reference: prpstn:hall-8.9.