Physicslib4.Spectral.Unbounded.AbstractCalculus

From a continuous functional calculus to a projection-valued measure

This file carries out, abstractly, the second stage of the spectral theorem: the input is a compact metric space X and an isometric *-homomorphism Φ : C(X, ℂ) → 𝓑(H), with no operator in sight, and the output is a projection-valued measure abstractPVM on X integrating to Φ. The bounded normal case below is an instance of it. The bounded self-adjoint case of Physicslib4/Spectral/SpectralTheorem.lean runs the same argument directly on X = σ(A), and is not derived from this file.

Main definitions

• IsAbstractCalculus — the five properties of def:abstract-continuous-functional-calculus.
• abstractMeasure — the measure μ_ψ supplied by Riesz representation.
• abstractForm, extendedCalculus — the quadratic form Q_f and the operator Φ̃(f) for bounded measurable f.
• abstractPVM — the resulting projection-valued measure.

Main statements

• isSelfAdjoint_of_real, inner_nonneg_of_nonneg — an abstract calculus is non-negative.
• abstractMeasure_univ — the associated measures are finite of mass ‖ψ‖².
• isBoundedQuadraticForm_abstractForm, norm_abstractForm_le — the extended forms are bounded quadratic forms, with bound ‖f‖_∞ ‖ψ‖².
• extendedCalculus_add, extendedCalculus_smul, inner_extendedCalculus, tendsto_inner_extendedCalculus, isSelfAdjoint_extendedCalculus_of_real, extendedCalculus_mul, extendedCalculus_conj.
• abstractPVM_integral, abstractPVM_integral_continuous — the projection-valued measure integrates to Φ̃, and to Φ on continuous functions.
• norm_extendedCalculus_le — the extended calculus is norm-bounded.
• existsUnique_spectralMeasure_normal, eq_of_integral_id_eq_ambient — the spectral theorem for bounded normal operators, with its ambient uniqueness form.

noncomputable def Physicslib4.Spectral.Unbounded.ofRealCM {X : Type u_2} [MetricSpace X] (f : C(X, ℝ)) : C(X, ℂ)

A continuous real function on X, regarded as a continuous complex function.

An abstract continuous functional calculus is defined on complex functions; the real ones are those whose operators are self-adjoint (isSelfAdjoint_of_real), and the measures μ(ψ) of abstractMeasure are characterised by their integrals of real functions.

Blueprint: lmm:abstract-calculus-non-negative

Equations

• Physicslib4.Spectral.Unbounded.ofRealCM f = { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ }

structure Physicslib4.Spectral.Unbounded.IsAbstractCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] (Φ : C(X, ℂ) → H →L[ℂ] H) : Prop

A map Φ from continuous complex functions on a compact metric space X to bounded operators on H is an abstract continuous functional calculus: it is linear and multiplicative, sends f̄ to Φ(f)*, is isometric for the supremum norm, and sends the constant 1 to 𝟙.

These are the properties of f ↦ f(A) for a bounded normal operator A on X = σ(A) (normalCalculus), with the operator itself forgotten. From such a Φ alone the file builds a projection-valued measure on X whose integrals reproduce Φ (abstractPVM), so the passage from a continuous functional calculus to a spectral measure is carried out once, in general. The spectral theorem for bounded normal operators (existsUnique_spectralMeasure_normal) is its special case Φ = normalCalculus.

Implementation note: the five properties are separate fields on an unbundled map rather than a bundled star-algebra homomorphism, as in the blueprint. X carries its Borel σ-algebra (BorelSpace X).

Blueprint: def:abstract-continuous-functional-calculus

• map_smul_add (α β : ℂ) (f g : C(X, ℂ)) : Φ (α • f + β • g) = α • Φ f + β • Φ g

  Φ is linear: Φ(αf + βg) = αΦ(f) + βΦ(g).

• map_mul (f g : C(X, ℂ)) : Φ (f * g) = Φ f * Φ g

  Φ is multiplicative: Φ(fg) = Φ(f)Φ(g).

• map_star (f : C(X, ℂ)) : Φ (star f) = ContinuousLinearMap.adjoint (Φ f)

  Φ sends the complex conjugate f̄ to the adjoint Φ(f)*.

• norm_map (f : C(X, ℂ)) : ‖Φ f‖ = ‖f‖

  Φ is isometric: ‖Φ(f)‖ = sup |f| over X.

• map_one : Φ 1 = 1

  Φ sends the constant function 1 to the identity 𝟙.

theorem Physicslib4.Spectral.Unbounded.isSelfAdjoint_of_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : C(X, ℝ)) : IsSelfAdjoint (Φ (ofRealCM f)) ∧ ∀ (ψ : H), (inner ℂ ψ ((Φ (ofRealCM f)) ψ)).im = 0

A real-valued continuous function gives a self-adjoint operator, and hence a real expectation value.

Blueprint reference: lmm:abstract-calculus-non-negative (Part 1).

theorem Physicslib4.Spectral.Unbounded.inner_nonneg_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : C(X, ℝ)} (hf : ∀ (x : X), 0 ≤ f x) (ψ : H) : 0 ≤ (inner ℂ ψ ((Φ (ofRealCM f)) ψ)).re

A non-negative continuous function gives a non-negative expectation value.

Blueprint reference: lmm:abstract-calculus-non-negative (Part 2).

theorem Physicslib4.Spectral.Unbounded.existsUnique_abstractMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) : ∃! ν : MeasureTheory.Measure X, MeasureTheory.IsFiniteMeasure ν ∧ ∀ (f : C(X, ℝ)), ∫ (x : X), f x ∂ν = (inner ℂ ψ ((Φ (ofRealCM f)) ψ)).re

For each vector ψ, exactly one finite Borel measure μ(ψ) on X has ∫ f dμ(ψ) = ⟨ψ, Φ(f)ψ⟩ for every continuous real function f.

The map f ↦ ⟨ψ, Φ(f)ψ⟩ is real, linear and non-negative on non-negative f (isSelfAdjoint_of_real, inner_nonneg_of_nonneg), so the Riesz–Markov–Kakutani representation theorem turns it into a measure. In quantum-mechanical terms, for a unit vector ψ the measure μ(ψ) is the probability distribution of the observable described by Φ in the state ψ.

Implementation note: existence is Mathlib's RealRMK.rieszMeasure; uniqueness is Mathlib's Measure.ext_of_integral_eq_on_compactlySupported.

Blueprint: def:abstract-associated-measures

noncomputable def Physicslib4.Spectral.Unbounded.abstractMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) : MeasureTheory.Measure X

The measure μ(ψ) on X associated with a vector ψ by an abstract continuous functional calculus Φ: the Borel measure with ∫ f dμ(ψ) = ⟨ψ, Φ(f)ψ⟩ for continuous real f.

It is a finite measure of total mass ‖ψ‖² (abstractMeasure_univ), and it is the measure ⟨ψ, μ(E)ψ⟩ that the projection-valued measure abstractPVM assigns to ψ (abstractPVM_assoc).

Implementation note: the measure is the one supplied by existsUnique_abstractMeasure, extracted with Exists.choose; its defining property is integral_abstractMeasure, and its finiteness is an instance.

Blueprint: def:abstract-associated-measures

Equations

• Physicslib4.Spectral.Unbounded.abstractMeasure hΦ ψ = Exists.choose ⋯

instance Physicslib4.Spectral.Unbounded.instIsFiniteMeasureAbstractMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) : MeasureTheory.IsFiniteMeasure (abstractMeasure hΦ ψ)

theorem Physicslib4.Spectral.Unbounded.integral_abstractMeasure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) (f : C(X, ℝ)) : ∫ (x : X), f x ∂abstractMeasure hΦ ψ = (inner ℂ ψ ((Φ (ofRealCM f)) ψ)).re

The defining property of abstractMeasure.

Blueprint reference: def:abstract-associated-measures.

theorem Physicslib4.Spectral.Unbounded.abstractMeasure_univ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) : (abstractMeasure hΦ ψ) Set.univ = ENNReal.ofReal (‖ψ‖ ^ 2)

The associated measures are finite, with total mass ‖ψ‖².

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

noncomputable def Physicslib4.Spectral.Unbounded.abstractForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : X → ℂ) (ψ : H) : ℂ

The quadratic form Q(f)(ψ) = ∫ f dμ(ψ) of a function f on X, built from the measures of an abstract continuous functional calculus.

For continuous f it is the expectation value ⟨ψ, Φ(f)ψ⟩ (abstractForm_continuous). The point is that the right-hand side makes sense for every bounded measurable f, such as the indicator function of a set, where Φ(f) is not defined. For such f, Q(f) is a bounded quadratic form with |Q(f)(ψ)| ≤ sup |f| · ‖ψ‖² (isBoundedQuadraticForm_abstractForm, norm_abstractForm_le), and so is the expectation value of exactly one bounded operator, extendedCalculus.

Implementation note: the definition is a Bochner integral and accepts any f : X → ℂ; the theorems about it assume f ∈ BddMeasurable X.

Blueprint: prpstn:abstract-extended-forms-are-bounded

Equations

• Physicslib4.Spectral.Unbounded.abstractForm hΦ f ψ = ∫ (x : X), f x ∂Physicslib4.Spectral.Unbounded.abstractMeasure hΦ ψ

theorem Physicslib4.Spectral.Unbounded.isBoundedQuadraticForm_abstractForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : IsBoundedQuadraticForm (abstractForm hΦ f)

Q_f is a bounded quadratic form, with |Q_f(ψ)| ≤ ‖f‖_∞ ‖ψ‖².

Blueprint reference: prpstn:abstract-extended-forms-are-bounded.

theorem Physicslib4.Spectral.Unbounded.norm_abstractForm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) (ψ : H) : ‖abstractForm hΦ f ψ‖ ≤ (⨆ (x : X), ‖f x‖) * ‖ψ‖ ^ 2

The explicit bound |Q_f(ψ)| ≤ ‖f‖_∞ ‖ψ‖², with ‖f‖_∞ = ⨆ x, ‖f x‖ as in ProjectionValuedMeasure.norm_integral_le.

Blueprint reference: prpstn:abstract-extended-forms-are-bounded (explicit bound).

theorem Physicslib4.Spectral.Unbounded.abstractForm_continuous {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : C(X, ℂ)) (ψ : H) : abstractForm hΦ (fun (x : X) => f x) ψ = inner ℂ ψ ((Φ f) ψ)

For continuous f, the extended form is the quadratic form of Φ(f).

Blueprint reference: prpstn:abstract-extended-forms-are-bounded (final claim).

noncomputable def Physicslib4.Spectral.Unbounded.extendedCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : X → ℂ) : H →L[ℂ] H

The extended calculus Φ̃(f) of a bounded measurable function f on X: the bounded operator with ⟨ψ, Φ̃(f)ψ⟩ = ∫ f dμ(ψ) for every ψ.

It extends the abstract continuous functional calculus Φ from continuous to bounded measurable functions: Φ̃(f) = Φ(f) for continuous f (extendedCalculus_continuous). Like Φ it is linear, multiplicative and sends f̄ to Φ̃(f)* (extendedCalculus_smul_add, extendedCalculus_mul, extendedCalculus_conj). Applied to indicator functions it gives the projections of the spectral measure (abstractPVM).

Implementation note: the operator is IsBoundedQuadraticForm.toOperator of abstractForm. The definition takes any f : X → ℂ and returns 0 when f is not bounded and measurable, so that it is a total function.

Blueprint: def:abstract-extended-calculus

Equations

• Physicslib4.Spectral.Unbounded.extendedCalculus hΦ f = if h : f ∈ Physicslib4.Spectral.BddMeasurable X then ⋯.toOperator else 0

theorem Physicslib4.Spectral.Unbounded.inner_extendedCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) (ψ : H) : inner ℂ ψ ((extendedCalculus hΦ f) ψ) = abstractForm hΦ f ψ

The defining property of the extended calculus.

Blueprint reference: def:abstract-extended-calculus.

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_continuous {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : C(X, ℂ)) : (extendedCalculus hΦ fun (x : X) => f x) = Φ f

The extended calculus agrees with Φ on continuous functions.

Blueprint reference: def:abstract-extended-calculus (final clause).

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_smul_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (α β : ℂ) {f g : X → ℂ} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : (extendedCalculus hΦ fun (x : X) => α * f x + β * g x) = α • extendedCalculus hΦ f + β • extendedCalculus hΦ g

The extended calculus is linear.

Blueprint reference: lmm:abstract-extended-linear.

theorem Physicslib4.Spectral.Unbounded.polarization_abstractForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {h : X → ℂ} (hh : h ∈ BddMeasurable X) (φ ψ : H) : polarization (abstractForm hΦ h) φ ψ = inner ℂ φ ((extendedCalculus hΦ h) ψ)

The off-diagonal formula: the sesquilinear form associated to Q_h is (φ, ψ) ↦ ⟪φ, Φ̃(h) ψ⟫.

Blueprint reference: lmm:abstract-extended-convergence (Part 1).

theorem Physicslib4.Spectral.Unbounded.tendsto_inner_extendedCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {h : ℕ → X → ℂ} {h₀ : X → ℂ} {M : ℝ} (hh : ∀ (i : ℕ), h i ∈ BddMeasurable X) (hbdd : ∀ (i : ℕ) (x : X), ‖h i x‖ ≤ M) (hlim : ∀ (x : X), Filter.Tendsto (fun (i : ℕ) => h i x) Filter.atTop (nhds (h₀ x))) (φ ψ : H) : Filter.Tendsto (fun (i : ℕ) => inner ℂ φ ((extendedCalculus hΦ (h i)) ψ)) Filter.atTop (nhds (inner ℂ φ ((extendedCalculus hΦ h₀) ψ)))

The convergence principle: uniformly bounded pointwise limits of the integrand pass to the weak limit of the operators.

Blueprint reference: lmm:abstract-extended-convergence (Part 2).

theorem Physicslib4.Spectral.Unbounded.isSelfAdjoint_extendedCalculus_of_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) (hreal : ∀ (x : X), (f x).im = 0) : IsSelfAdjoint (extendedCalculus hΦ f)

A real-valued bounded measurable function gives a self-adjoint operator.

Blueprint reference: lmm:abstract-extended-real-self-adjoint.

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f g : X → ℂ} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : (extendedCalculus hΦ fun (x : X) => f x * g x) = extendedCalculus hΦ f * extendedCalculus hΦ g

The extended calculus is multiplicative.

Blueprint reference: prpstn:abstract-extended-multiplicative.

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : (extendedCalculus hΦ fun (x : X) => (starRingEnd ℂ) (f x)) = ContinuousLinearMap.adjoint (extendedCalculus hΦ f)

The extended calculus intertwines conjugation with the adjoint.

Blueprint reference: lmm:abstract-extended-conjugation.

theorem Physicslib4.Spectral.Unbounded.indicator_one_mem_bddMeasurable_iff {X : Type u_2} [MeasurableSpace X] {E : Set X} : E.indicator 1 ∈ BddMeasurable X ↔ MeasurableSet E

The indicator 1_E is bounded and measurable exactly when E is measurable.

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) : extendedCalculus hΦ 0 = 0

Φ̃(0) = 0.

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_indicator_inter {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) : extendedCalculus hΦ ((E ∩ F).indicator 1) = extendedCalculus hΦ (E.indicator 1) * extendedCalculus hΦ (F.indicator 1)

Φ̃(1_{E ∩ F}) = Φ̃(1_E) Φ̃(1_F).

theorem Physicslib4.Spectral.Unbounded.extendedCalculus_indicator_union {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) (hEF : Disjoint E F) : extendedCalculus hΦ ((E ∪ F).indicator 1) = extendedCalculus hΦ (E.indicator 1) + extendedCalculus hΦ (F.indicator 1)

Φ̃(1_{E ∪ F}) = Φ̃(1_E) + Φ̃(1_F) for disjoint E, F.

theorem Physicslib4.Spectral.Unbounded.isStarProjection_extendedCalculus_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (E : Set X) : IsStarProjection (extendedCalculus hΦ (E.indicator 1))

Each Φ̃(1_E) is an orthogonal projection.

theorem Physicslib4.Spectral.Unbounded.norm_sq_apply_of_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) (ψ : H) : ‖P ψ‖ ^ 2 = (inner ℂ ψ (P ψ)).re

For an orthogonal projection P, ‖P ψ‖² = Re ⟪ψ, P ψ⟫.

theorem Physicslib4.Spectral.Unbounded.hasSum_extendedCalculus_indicator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (E : ℕ → Set X) (hE : ∀ (j : ℕ), MeasurableSet (E j)) (hdisj : Pairwise fun (i j : ℕ) => Disjoint (E i) (E j)) (v : H) : HasSum (fun (j : ℕ) => (extendedCalculus hΦ ((E j).indicator 1)) v) ((extendedCalculus hΦ ((⋃ (j : ℕ), E j).indicator 1)) v)

Countable additivity of E ↦ Φ̃(1_E), in the norm topology of H.

noncomputable def Physicslib4.Spectral.Unbounded.abstractPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) : ProjectionValuedMeasure X H

The projection-valued measure on X defined by an abstract continuous functional calculus Φ: each measurable set E goes to the projection Φ̃(1(E)), the extended calculus of its indicator function.

Φ̃(1(E)) is a projection because 1(E)² = 1(E) and 1(E) is real. Countable additivity is a consequence of the convergence of ⟨φ, Φ̃(fₙ)ψ⟩ along bounded pointwise convergent sequences fₙ (tendsto_inner_extendedCalculus), applied to the indicators of the remainders of a disjoint union. Its integral is the extended calculus: ∫ f dμ = Φ̃(f) for bounded measurable f, and so ∫ f dμ = Φ(f) for continuous f (abstractPVM_integral, abstractPVM_integral_continuous). For Φ the functional calculus of a normal operator A, this is the spectral measure of A.

Implementation note: the value on a non-measurable set is 0, as the structure ProjectionValuedMeasure requires; it holds because extendedCalculus is 0 on functions that are not bounded and measurable.

Blueprint: thrm:abstract-calculus-yields-pvm

Equations

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

@[simp]

theorem Physicslib4.Spectral.Unbounded.abstractPVM_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (E : Set X) : (abstractPVM hΦ) E = extendedCalculus hΦ (E.indicator 1)

theorem Physicslib4.Spectral.Unbounded.abstractPVM_assoc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (ψ : H) : (abstractPVM hΦ).assoc ψ = abstractMeasure hΦ ψ

The measures associated with μ^Φ are the measures μ_ψ of the calculus.

theorem Physicslib4.Spectral.Unbounded.abstractPVM_integral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : (abstractPVM hΦ).integral f = extendedCalculus hΦ f

The projection-valued measure integrates to the extended calculus; in particular to Φ on continuous functions.

Blueprint reference: thrm:abstract-calculus-yields-pvm.

theorem Physicslib4.Spectral.Unbounded.abstractPVM_integral_continuous {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) (f : C(X, ℂ)) : ((abstractPVM hΦ).integral fun (x : X) => f x) = Φ f

On continuous functions the projection-valued measure integrates to Φ itself.

Blueprint reference: thrm:abstract-calculus-yields-pvm (final clause).

theorem Physicslib4.Spectral.Unbounded.norm_extendedCalculus_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] {Φ : C(X, ℂ) → H →L[ℂ] H} (hΦ : IsAbstractCalculus Φ) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : ‖extendedCalculus hΦ f‖ ≤ ⨆ (x : X), ‖f x‖

The extended calculus is bounded by the supremum norm ‖f‖_∞ = ⨆ x, ‖f x‖ of the integrand (the same form as ProjectionValuedMeasure.norm_integral_le; the supremum is 0 when X is empty).

Blueprint reference: crllr:abstract-extended-norm-bound.

The spectral theorem for bounded normal operators

theorem Physicslib4.Spectral.Unbounded.continuousMap_mem_bddMeasurable {Z : Type u_3} [TopologicalSpace Z] [CompactSpace Z] [MeasurableSpace Z] [OpensMeasurableSpace Z] (f : C(Z, ℂ)) : (fun (z : Z) => f z) ∈ BddMeasurable Z

A continuous function on a compact space is a bounded measurable integrand.

theorem Physicslib4.Spectral.Unbounded.continuous_integral_continuousMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Z : Type u_3} [TopologicalSpace Z] [CompactSpace Z] [MeasurableSpace Z] [OpensMeasurableSpace Z] (μ : ProjectionValuedMeasure Z H) : Continuous fun (f : C(Z, ℂ)) => μ.integral fun (z : Z) => f z

On a compact space, f ↦ ∫ f dμ is continuous (indeed 1-Lipschitz) for the sup norm on C(Z, ℂ).

theorem Physicslib4.Spectral.Unbounded.integral_const_eq_smul_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Z : Type u_3} [MeasurableSpace Z] (μ : ProjectionValuedMeasure Z H) (c : ℂ) : (μ.integral fun (x : Z) => c) = c • 1

The integral of a constant c is c • 1.

theorem Physicslib4.Spectral.Unbounded.integral_continuousMap_eq_comp_inclusion {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} {Y : Set ℂ} [CompactSpace ↑Y] (hsub : spectrum ℂ A ⊆ Y) {μA : ProjectionValuedMeasure (↑(spectrum ℂ A)) H} (hμA : (μA.integral fun (lam : ↑(spectrum ℂ A)) => ↑lam) = A) {ν : ProjectionValuedMeasure (↑Y) H} (hν : (ν.integral fun (y : ↑Y) => ↑y) = A) (g : C(↑Y, ℂ)) : (ν.integral fun (y : ↑Y) => g y) = μA.integral fun (lam : ↑(spectrum ℂ A)) => g (Set.inclusion hsub lam)

If PVMs on Y ⊇ σ(A) and on σ(A) both integrate the identity to A, then they agree on every continuous g on Y (restricted to σ(A) on the right): both sides are *-homomorphisms in g agreeing on λ, and Stone–Weierstrass gives density.

theorem Physicslib4.Spectral.Unbounded.assoc_eq_map_inclusion {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} {Y : Set ℂ} [CompactSpace ↑Y] (hsub : spectrum ℂ A ⊆ Y) {μA : ProjectionValuedMeasure (↑(spectrum ℂ A)) H} (hμA : (μA.integral fun (lam : ↑(spectrum ℂ A)) => ↑lam) = A) {ν : ProjectionValuedMeasure (↑Y) H} (hν : (ν.integral fun (y : ↑Y) => ↑y) = A) (ψ : H) : ν.assoc ψ = MeasureTheory.Measure.map (Set.inclusion hsub) (μA.assoc ψ)

Under the hypotheses of integral_continuousMap_eq_comp_inclusion, the measure ν_ψ on Y is the push-forward of (μA)_ψ along Set.inclusion hsub.

theorem Physicslib4.Spectral.Unbounded.apply_eq_apply_preimage_inclusion {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} {Y : Set ℂ} [CompactSpace ↑Y] (hsub : spectrum ℂ A ⊆ Y) {μA : ProjectionValuedMeasure (↑(spectrum ℂ A)) H} (hμA : (μA.integral fun (lam : ↑(spectrum ℂ A)) => ↑lam) = A) {ν : ProjectionValuedMeasure (↑Y) H} (hν : (ν.integral fun (y : ↑Y) => ↑y) = A) {E : Set ↑Y} (hE : MeasurableSet E) : ν E = μA (Set.inclusion hsub ⁻¹' E)

The ambient uniqueness statement, for a compact Y ⊇ σ(A) (normality of A is not needed): ν(E) = μA(E ∩ σ(A)), compared through the associated measures.

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

The spectral theorem for bounded normal operators: exactly one projection-valued measure μ on the spectrum of a bounded normal operator A satisfies ∫ λ dμ(λ) = A.

A normal A need not be self-adjoint, so its spectrum is a compact subset of ℂ rather than of ℝ; unitary operators, with spectrum on the unit circle, are the case used for the unbounded spectral theorem (through the Cayley transform). The measure is abstractPVM for the continuous functional calculus normalCalculus of A.

Implementation note: the blueprint assumes H ≠ {0}; the Lean statement does not need it. Uniqueness is proved through apply_eq_apply_preimage_inclusion, which also gives the ambient form eq_of_integral_id_eq_ambient.

Blueprint: thrm:hall-10.20

theorem Physicslib4.Spectral.Unbounded.eq_of_integral_id_eq_ambient {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (_hA : IsStarNormal A) {Y : Set ℂ} (hY : IsCompact Y) (hsub : spectrum ℂ A ⊆ Y) {μA : ProjectionValuedMeasure (↑(spectrum ℂ A)) H} (hμA : (μA.integral fun (lam : ↑(spectrum ℂ A)) => ↑lam) = A) {ν : ProjectionValuedMeasure (↑Y) H} (hν : (ν.integral fun (y : ↑Y) => ↑y) = A) {E : Set ↑Y} (hE : MeasurableSet E) : ν E = μA (Set.inclusion hsub ⁻¹' E)

The ambient form of uniqueness: a projection-valued measure on a larger compact set Y integrating to A assigns no mass off σ(A) and agrees with μ^A there.

Blueprint reference: thrm:hall-10.20.