Physicslib4.Spectral.Unbounded.Cayley

The Cayley transform and the spectral theorem for unbounded self-adjoint operators

The scalar Cayley map C(x) = (x + i)/(x - i) is a bijection of ℝ onto the unit circle minus the point 1, with inverse D(u) = i (u + 1)/(u - 1). Substituting a self-adjoint unbounded operator A for x produces a bounded unitary — hence normal — operator U, to which the spectral theorem for bounded normal operators applies; transporting the resulting projection-valued measure back along C gives the spectral measure of A.

Main definitions

• cayleyMap, cayleyInv, unitCircleMinusOne — the scalar maps.
• IsCayleyTransform — U is the Cayley transform of A, built from the resolvent B = (A - i 1)⁻¹.
• restrictPVM, mapPVM — restriction and transport of a projection-valued measure.
• cayleyPVM — the projection-valued measure on ℝ obtained from that of U.

Main statements

• unitary_mul_adjoint — a unitary operator is normal.
• bijOn_cayleyMap and companions — the Cayley map and its inverse.
• exists_isCayleyTransform — the Cayley transform exists and is unitary, U - 1 is injective with range Dom(A), and A = i (U + 1)(U - 1)⁻¹.
• mem_spectrum_iff_cayleyMap_mem_spectrum — spectral mapping for the Cayley transform.
• spectralMeasure_singleton_one_eq_zero — μ^U({1}) = 0.
• pmapIntegral_cayleyInv_eq — A = ∫ D dμ^U.
• pmapIntegral_cayleyPVM_id — A = ∫ λ dμ^A.
• existsUnique_spectralMeasure_unbounded — the spectral theorem for unbounded self-adjoint operators, with concentration on the spectrum.

Unitary operators

theorem Physicslib4.Spectral.Unbounded.unitary_mul_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (hU : U ∈ unitary (H →L[ℂ] H)) : ContinuousLinearMap.adjoint U * U = 1 ∧ U * ContinuousLinearMap.adjoint U = 1 ∧ IsStarNormal U

A unitary operator satisfies U* U = U U* = 1; in particular it is normal.

Blueprint reference: lmm:unitary-is-normal.

The scalar Cayley map

def Physicslib4.Spectral.Unbounded.unitCircleMinusOne : Set ℂ

The unit circle in ℂ with the point 1 removed: the image of the real line under the Cayley map.

The spectrum of a unitary operator lies on the unit circle. The Cayley map C sends ℝ bijectively onto this set (bijOn_cayleyMap), so the spectrum of the Cayley transform of a self-adjoint operator, with the point 1 removed, corresponds to the spectrum of the operator (cayleyMap_image_spectrum).

Blueprint: lmm:cayley-map

Equations

• Physicslib4.Spectral.Unbounded.unitCircleMinusOne = {u : ℂ | ‖u‖ = 1} \ {1}

noncomputable def Physicslib4.Spectral.Unbounded.cayleyMap (x : ℝ) : ℂ

The Cayley map C(x) = (x + i)/(x − i), which sends the real line onto the unit circle with the point 1 removed.

It is the scalar version of the Cayley transform: substituting a self-adjoint operator A for x gives the unitary operator U = (A + i𝟙)(A − i𝟙)⁻¹. Since |x + i| = |x − i| for real x, C(x) has modulus 1, and C(x) = 1 is impossible; as x runs from −∞ to +∞, C(x) goes once around the circle, starting and ending at 1. C is continuous (continuous_cayleyMap) and bijective onto unitCircleMinusOne (bijOn_cayleyMap), with inverse cayleyInv.

Blueprint: lmm:cayley-map

Equations

• Physicslib4.Spectral.Unbounded.cayleyMap x = (↑x + Complex.I) / (↑x - Complex.I)

noncomputable def Physicslib4.Spectral.Unbounded.cayleyInv (u : ℂ) : ℝ

The inverse Cayley map D(u) = i(u + 1)/(u − 1), taken as a real number.

On the unit circle with 1 removed, D is real-valued (cayleyInv_ofReal) and inverts the Cayley map C (cayleyInv_cayleyMap, cayleyMap_cayleyInv). Integrating D against the spectral measure of the Cayley transform U recovers the self-adjoint operator A (pmapIntegral_cayleyInv_eq); this is how the spectral theorem for A is obtained from that of U.

Implementation note: the value is the real part of i(u + 1)/(u − 1), so that D is a total function ℂ → ℝ. Off the unit circle minus 1 the value has no meaning (at u = 1 it is 0, by Lean's convention for division by zero); it is continuous on unitCircleMinusOne (continuousOn_cayleyInv) and measurable on ℂ (measurable_cayleyInv).

Blueprint: lmm:cayley-map

Equations

• Physicslib4.Spectral.Unbounded.cayleyInv u = (Complex.I * (u + 1) / (u - 1)).re

theorem Physicslib4.Spectral.Unbounded.cayleyMap_mem (x : ℝ) : cayleyMap x ∈ unitCircleMinusOne

C lands in the unit circle minus 1.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.continuous_cayleyMap : Continuous cayleyMap

C is continuous, hence Borel measurable.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.continuousOn_cayleyInv : ContinuousOn cayleyInv unitCircleMinusOne

D is continuous on its domain, hence Borel measurable there.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.cayleyInv_ofReal {u : ℂ} (hu : u ∈ unitCircleMinusOne) : ↑(cayleyInv u) = Complex.I * (u + 1) / (u - 1)

On the unit circle minus 1, i (u+1)/(u-1) is real, so cayleyInv loses no information.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.cayleyInv_cayleyMap (x : ℝ) : cayleyInv (cayleyMap x) = x

D ∘ C = id on ℝ.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.cayleyMap_cayleyInv {u : ℂ} (hu : u ∈ unitCircleMinusOne) : cayleyMap (cayleyInv u) = u

C ∘ D = id on the unit circle minus 1.

Blueprint reference: lmm:cayley-map.

theorem Physicslib4.Spectral.Unbounded.bijOn_cayleyMap : Set.BijOn cayleyMap Set.univ unitCircleMinusOne

C is a bijection of ℝ onto the unit circle minus 1.

Blueprint reference: lmm:cayley-map.

The Cayley transform of a self-adjoint operator

structure Physicslib4.Spectral.Unbounded.IsCayleyTransform {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →ₗ.[ℂ] H) (B U : H →L[ℂ] H) : Prop

A bounded operator U is the Cayley transform of an operator A, with B the bounded inverse of A − i𝟙: U = (A + i𝟙)(A − i𝟙)⁻¹, that is Uψ = (A + i𝟙)Bψ for every ψ.

The Cayley transform turns an unbounded self-adjoint operator into a bounded unitary one, in the way the Cayley map turns the real line into the unit circle. For self-adjoint A the inverse B exists (i is not in the spectrum of A), U is unitary, U − 𝟙 is injective with range Dom(A), and A can be recovered as i(U + 𝟙)(U − 𝟙)⁻¹ (exists_isCayleyTransform). The spectral theorem for the bounded normal operator U then yields that of A.

Implementation note: the structure records the inverse B as data alongside U, because the formula for U applies A to Bψ, which lies in Dom(A). The operator U is determined by A (IsCayleyTransform.unitary_eq).

Blueprint: thrm:hall-10.28

• isResolvent : IsResolvent A Complex.I B

  B is the bounded two-sided inverse of A − i𝟙.

• apply_eq (ψ : H) : U ψ = ↑A ⟨B ψ, ⋯⟩ + Complex.I • B ψ

  Uψ = (A + i𝟙)Bψ = A(Bψ) + iBψ for every ψ.

theorem Physicslib4.Spectral.Unbounded.norm_add_I_smul_eq_norm_sub_I_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {A : H →ₗ.[ℂ] H} (hsym : IsSymmetric A) (ψ : ↥A.domain) : ‖↑A ψ + Complex.I • ↑ψ‖ = ‖↑A ψ - Complex.I • ↑ψ‖

For a symmetric A and ψ ∈ Dom(A), ‖(A + i 1) ψ‖ = ‖(A - i 1) ψ‖: both squares equal ‖A ψ‖² + ‖ψ‖², the cross terms cancelling by symmetry.

Blueprint reference: thrm:hall-10.28.

theorem Physicslib4.Spectral.Unbounded.exists_isCayleyTransform {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : ∃ (B : H →L[ℂ] H) (U : H →L[ℂ] H), IsCayleyTransform A B U ∧ U ∈ unitary (H →L[ℂ] H) ∧ Function.Injective ⇑(U - 1) ∧ Set.range ⇑(U - 1) = ↑A.domain ∧ (∀ (χ : H) (h : (U - 1) χ ∈ A.domain), ↑A ⟨(U - 1) χ, h⟩ = Complex.I • (U + 1) χ) ∧ U - 1 = (2 * Complex.I) • B

Every self-adjoint operator A has a Cayley transform U = (A + i𝟙)(A − i𝟙)⁻¹, and U is unitary.

In detail, with B = (A − i𝟙)⁻¹, which exists because i is not in the spectrum of A:

1. U is unitary;
2. U − 𝟙 is injective;
3. the range of U − 𝟙 is Dom(A), and A(U − 𝟙)χ = i(U + 𝟙)χ for every χ, that is A = i(U + 𝟙)(U − 𝟙)⁻¹ on Dom(A);
4. U − 𝟙 = 2iB.

Unitarity rests on ‖(A + i𝟙)ψ‖ = ‖(A − i𝟙)ψ‖ for ψ in Dom(A), which holds because A is symmetric (norm_add_I_smul_eq_norm_sub_I_smul). Point 3 does not say that 1 is outside the spectrum of U: (U − 𝟙)⁻¹ is defined only on Dom(A) and is unbounded when A is.

Blueprint: thrm:hall-10.28

theorem Physicslib4.Spectral.Unbounded.mem_spectrum_iff_cayleyMap_mem_spectrum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (_hA : IsSelfAdjoint A) {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) (lam : ℝ) : ↑lam ∈ pmapSpectrum A ↔ cayleyMap lam ∈ spectrum ℂ U

Spectral mapping for the Cayley transform: a real λ is in the spectrum of the self-adjoint operator A exactly when C(λ) is in the spectrum of its Cayley transform U.

Together with the reality of the spectrum of A, this gives C(σ(A)) = σ(U) \ {1} (cayleyMap_image_spectrum), and it is what makes the spectral measure of A, obtained from that of U, concentrated on σ(A) (spectralMeasure_concentrated).

Implementation note: the statement is about real λ; the spectrum of A is a set of complex numbers, contained in ℝ by pmapSpectrum_subset_real.

Blueprint: lmm:cayley-spectral-mapping

theorem Physicslib4.Spectral.Unbounded.cayleyMap_image_spectrum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) : cayleyMap '' {lam : ℝ | ↑lam ∈ pmapSpectrum A} = spectrum ℂ U \ {1}

Consequently C maps σ(A) onto σ(U) \ {1}.

Blueprint reference: lmm:cayley-spectral-mapping.

Transport of projection-valued measures

noncomputable def Physicslib4.Spectral.Unbounded.restrictPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} [MeasurableSpace Y] (μ : ProjectionValuedMeasure Y H) {Y₀ : Set Y} (hY₀ : MeasurableSet Y₀) (hmass : μ Y₀ᶜ = 0) : ProjectionValuedMeasure (↑Y₀) H

The restriction of a projection-valued measure μ on Y to a measurable subset Y₀ whose complement has measure 0: the projection-valued measure on Y₀ sending E to μ(E).

When μ(Y \ Y₀) = 0 no state has any probability of a value outside Y₀, so nothing is lost by regarding μ as a measure on Y₀; in particular μ(Y₀) = 𝟙.

Implementation note: Y₀ is a subtype, with the subspace σ-algebra; a set E of Y₀ goes to μ of its image in Y. The construction of cayleyPVM does not use this definition.

Blueprint: lmm:borel-bijection-transports-pvm (Part 1)

Equations

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

noncomputable def Physicslib4.Spectral.Unbounded.mapPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) (T : Y → Z) (hT : Measurable T) (hbij : Function.Bijective T) (_hinv : Measurable ⇑(Equiv.ofBijective T hbij).symm) : ProjectionValuedMeasure Z H

The transport of a projection-valued measure μ on Y along a measurable bijection T : Y → Z with measurable inverse: the projection-valued measure on Z sending F to μ(T⁻¹(F)).

This relabels the possible values of an observable by T without changing the projections. The measure it assigns to a vector ψ is the pushforward along T of the one μ assigns (assoc_mapPVM).

Implementation note: measurability of the inverse ensures that T⁻¹(F) is non-measurable whenever F is, so that the transported measure is 0 on non-measurable sets, as ProjectionValuedMeasure requires. pushforwardPVM is the variant for a map that is not bijective. The construction of cayleyPVM does not use this definition.

Blueprint: lmm:borel-bijection-transports-pvm (Part 2)

Equations

• Physicslib4.Spectral.Unbounded.mapPVM μ T hT hbij _hinv = { toFun := fun (F : Set Z) => μ (T ⁻¹' F), isStarProjection' := ⋯, notMeasurable' := ⋯, univ' := ⋯, hasSum' := ⋯, inter' := ⋯ }

@[simp]

theorem Physicslib4.Spectral.Unbounded.mapPVM_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) (T : Y → Z) (hT : Measurable T) (hbij : Function.Bijective T) (hinv : Measurable ⇑(Equiv.ofBijective T hbij).symm) (F : Set Z) : (mapPVM μ T hT hbij hinv) F = μ (T ⁻¹' F)

theorem Physicslib4.Spectral.Unbounded.assoc_mapPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) (T : Y → Z) (hT : Measurable T) (hbij : Function.Bijective T) (hinv : Measurable ⇑(Equiv.ofBijective T hbij).symm) (ψ : H) : (mapPVM μ T hT hbij hinv).assoc ψ = MeasureTheory.Measure.map T (μ.assoc ψ)

The scalar measures of the transported projection-valued measure are the pushforwards.

Blueprint reference: lmm:borel-bijection-transports-pvm (Part 2).

The spectral measure of an unbounded self-adjoint operator

theorem Physicslib4.Spectral.Unbounded.spectralMeasure_singleton_one_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →ₗ.[ℂ] H} (_hA : IsSelfAdjoint A) {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H} (hμU : (μU.integral fun (u : ↑(spectrum ℂ U)) => ↑u) = U) : μU {u : ↑(spectrum ℂ U) | ↑u = 1} = 0

μ^U assigns no mass to {1}, so D — undefined there — is defined almost everywhere for every μ^U_ψ.

Blueprint reference: lmm:cayley-omits-one.

theorem Physicslib4.Spectral.Unbounded.measurable_cayleyInv : Measurable cayleyInv

D is Borel measurable on all of ℂ.

theorem Physicslib4.Spectral.Unbounded.eq_of_le_of_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T S : H →ₗ.[ℂ] H} (hT : IsSelfAdjoint T) (hS : IsSelfAdjoint S) (h : T ≤ S) : T = S

A self-adjoint operator has no proper self-adjoint extension.

theorem Physicslib4.Spectral.Unbounded.IsCayleyTransform.unitary_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {A : H →ₗ.[ℂ] H} {B U B' U' : H →L[ℂ] H} (hU : IsCayleyTransform A B U) (hU' : IsCayleyTransform A B' U') : U = U'

The Cayley transform U is determined by A.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyInv_apply_sub_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (hUu : U ∈ unitary (H →L[ℂ] H)) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H} (hμU : (μU.integral fun (u : ↑(spectrum ℂ U)) => ↑u) = U) (h1 : μU {u : ↑(spectrum ℂ U) | ↑u = 1} = 0) (χ : H) : ∃ (hψ : (U - 1) χ ∈ integralDomain μU fun (u : ↑(spectrum ℂ U)) => ↑(cayleyInv ↑u)), ↑(pmapIntegral μU fun (u : ↑(spectrum ℂ U)) => ↑(cayleyInv ↑u)) ⟨(U - 1) χ, hψ⟩ = Complex.I • (U + 1) χ

For unitary U with μ^U({1}) = 0 and ψ = (U - 1) χ: ψ ∈ W_D and (∫ D dμ^U) ψ = i (U + 1) χ, since D(u) (u - 1) = i (u + 1) off u = 1.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyInv_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H} (hμU : (μU.integral fun (u : ↑(spectrum ℂ U)) => ↑u) = U) : (pmapIntegral μU fun (u : ↑(spectrum ℂ U)) => ↑(cayleyInv ↑u)) = A

A is recovered from U by integrating D against μ^U, with equality of domains.

Blueprint reference: prpstn:hall-10.29.

noncomputable def Physicslib4.Spectral.Unbounded.cayleyPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H) : ProjectionValuedMeasure ℝ H

The projection-valued measure on ℝ obtained from a projection-valued measure μ(U) on the spectrum of a unitary U through the inverse Cayley map: a Borel set E goes to μ(U)(C(E)).

When U is the Cayley transform of a self-adjoint A and μ(U) its spectral measure, this is the spectral measure of A: ∫ λ dμ(λ) = A (pmapIntegral_cayleyPVM_id). The point 1 of the circle, which corresponds to no real number, carries no mass (spectralMeasure_singleton_one_eq_zero), so nothing of μ(U) is lost.

Implementation note: C(E) is written as the set of u in σ(U) with D(u) in E, using cayleyInv; the two agree on the unit circle minus 1. Non-measurable E are sent to 0, as a projection-valued measure requires; the preimage of a non-Borel set under D can still carry mass. The blueprint builds the measure by restriction and transport (restrictPVM, mapPVM); this definition composes with D directly.

Blueprint: thrm:hall-10.30

Equations

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

theorem Physicslib4.Spectral.Unbounded.cayleyPVM_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H) {E : Set ℝ} (hE : MeasurableSet E) : (cayleyPVM μU) E = μU {u : ↑(spectrum ℂ U) | cayleyInv ↑u ∈ E}

theorem Physicslib4.Spectral.Unbounded.assoc_cayleyPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H) (ψ : H) : (cayleyPVM μU).assoc ψ = MeasureTheory.Measure.map (fun (u : ↑(spectrum ℂ U)) => cayleyInv ↑u) (μU.assoc ψ)

The scalar measures of μ^A are the pushforwards of those of μ^U along D.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyPVM_id_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : H →L[ℂ] H} (μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H) : (pmapIntegral (cayleyPVM μU) fun (x : ℝ) => ↑x) = pmapIntegral μU fun (u : ↑(spectrum ℂ U)) => ↑(cayleyInv ↑u)

∫ λ dμ^A = ∫ D dμ^U, with equality of domains, by change of variables.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyPVM_id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H} (hμU : (μU.integral fun (u : ↑(spectrum ℂ U)) => ↑u) = U) : (pmapIntegral (cayleyPVM μU) fun (x : ℝ) => ↑x) = A

Transporting the spectral measure of U through the Cayley map gives a projection-valued measure on ℝ integrating the identity to A.

Blueprint reference: thrm:hall-10.30.

noncomputable def Physicslib4.Spectral.Unbounded.pushforwardPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) (T : Y → Z) (hT : Measurable T) : ProjectionValuedMeasure Z H

The pushforward of a projection-valued measure μ on Y along a measurable map T : Y → Z: the projection-valued measure on Z sending a measurable F to μ(T⁻¹(F)).

For a bounded measurable g on Z, ∫ g dμ' = ∫ (g ∘ T) dμ, where μ' is the pushforward (integral_pushforwardPVM). The uniqueness half of the unbounded spectral theorem uses it to move a second spectral measure ν of A, on ℝ, to the circle along the Cayley map, where it is compared with the spectral measure of the Cayley transform U.

Implementation note: T need not be bijective, unlike mapPVM; in exchange non-measurable F are sent to 0 by an explicit case split.

Blueprint: thrm:hall-10.4 (formalization note after its proof)

Equations

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

theorem Physicslib4.Spectral.Unbounded.pushforwardPVM_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) {T : Y → Z} (hT : Measurable T) {F : Set Z} (hF : MeasurableSet F) : (pushforwardPVM μ T hT) F = μ (T ⁻¹' F)

theorem Physicslib4.Spectral.Unbounded.integral_pushforwardPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (μ : ProjectionValuedMeasure Y H) {T : Y → Z} (hT : Measurable T) {g : Z → ℂ} (hg : g ∈ BddMeasurable Z) : (pushforwardPVM μ T hT).integral g = μ.integral (g ∘ T)

Change of variables for the bounded integral: ∫ g d(T_* μ) = ∫ g ∘ T dμ.

theorem Physicslib4.Spectral.Unbounded.integral_inv_sub_I_eq_resolvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} {B : H →L[ℂ] H} (hB : IsResolvent A Complex.I B) {μ : ProjectionValuedMeasure ℝ H} (hμ : (pmapIntegral μ fun (x : ℝ) => ↑x) = A) : (μ.integral fun (x : ℝ) => (↑x - Complex.I)⁻¹) = B

If ∫ λ dμ = A and B = (A - i 1)⁻¹, then ∫ (λ - i)⁻¹ dμ = B.

Blueprint reference: thrm:hall-10.4 (Step 1 of the uniqueness proof).

theorem Physicslib4.Spectral.Unbounded.integral_cayleyMap_eq_unitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) (hU1 : U - 1 = (2 * Complex.I) • B) {μ : ProjectionValuedMeasure ℝ H} (hμ : (pmapIntegral μ fun (x : ℝ) => ↑x) = A) : (μ.integral fun (x : ℝ) => cayleyMap x) = U

If ∫ λ dμ = A, then ∫ C dμ = U for the Cayley map C and the Cayley transform U of A, since C = 1 + 2i (λ - i)⁻¹ and U = 1 + 2i (A - i 1)⁻¹.

Blueprint reference: thrm:hall-10.4 (Step 2 of the uniqueness proof).

theorem Physicslib4.Spectral.Unbounded.eq_cayleyPVM_of_pmapIntegral_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} {B U : H →L[ℂ] H} (hU : IsCayleyTransform A B U) (hUu : U ∈ unitary (H →L[ℂ] H)) (hU1 : U - 1 = (2 * Complex.I) • B) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H} (hμU : (μU.integral fun (u : ↑(spectrum ℂ U)) => ↑u) = U) {μ : ProjectionValuedMeasure ℝ H} (hμ : (pmapIntegral μ fun (x : ℝ) => ↑x) = A) : μ = cayleyPVM μU

Uniqueness: any projection-valued measure on ℝ integrating the identity to A is the Cayley transport μ^A of the spectral measure μ^U of the Cayley transform U.

Blueprint reference: thrm:hall-10.4 (Steps 3 and 4 of the uniqueness proof).

theorem Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_unbounded {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : ∃! μ : ProjectionValuedMeasure ℝ H, (pmapIntegral μ fun (x : ℝ) => ↑x) = A

The spectral theorem for unbounded self-adjoint operators: for every self-adjoint A exactly one projection-valued measure μ on ℝ satisfies ∫ λ dμ(λ) = A.

This is the mathematical content of the statement that an observable, such as position, momentum or a Hamiltonian, has a spectral decomposition: μ(E) is the projection onto the states where the observable takes a value in E with certainty, and ⟨ψ, μ(E)ψ⟩ is the probability of a value in E for the unit vector ψ. The integral is the unbounded operator of pmapIntegral, domain included, so the equation also says that Dom(A) consists of the ψ with ∫ λ² dμ(ψ)(λ) finite, where μ(ψ) is the measure E ↦ ⟨ψ, μ(E)ψ⟩. The measure is concentrated on the spectrum of A (spectralMeasure_concentrated).

Implementation note: existence is cayleyPVM of the spectral measure of the Cayley transform of A (exists_isCayleyTransform, existsUnique_spectralMeasure_normal); uniqueness passes through eq_cayleyPVM_of_pmapIntegral_eq. The case H = {0} is treated separately. The measure itself is spectralMeasure.

Blueprint: thrm:hall-10.4

theorem Physicslib4.Spectral.Unbounded.spectralMeasure_concentrated {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {μ : ProjectionValuedMeasure ℝ H} (hμ : (pmapIntegral μ fun (x : ℝ) => ↑x) = A) : μ {x : ℝ | ↑x ∉ pmapSpectrum A} = 0 ∧ ∀ (E : Set ℝ), MeasurableSet E → μ E = μ (E ∩ {x : ℝ | ↑x ∈ pmapSpectrum A})

The spectral measure is concentrated on the spectrum.

Blueprint reference: thrm:hall-10.4.