Physicslib4.Spectral.ProjectionValuedMeasure

Projection-valued measures

A projection-valued measure on a measurable space X with values in the bounded operators of a complex Hilbert space H is the object the spectral theorem produces: a countably additive, multiplicative assignment of orthogonal projections to measurable subsets of X.

Main definitions

• Physicslib4.Spectral.ProjectionValuedMeasure — the blueprint's μ : Ω(X) → 𝓑(H).
• Physicslib4.Spectral.ProjectionValuedMeasure.assoc — the positive finite scalar measure μ_ψ : E ↦ ⟪ψ, μ E ψ⟫.

Main statements

• Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_assoc — μ_ψ is a well-defined positive, finite, real-valued measure.
• Physicslib4.Spectral.ProjectionValuedMeasure.inner_eq_zero_of_disjoint, Physicslib4.Spectral.ProjectionValuedMeasure.norm_sq_eq_sum_of_partition — the vectors μ(Eᵢ)ψ of a finite measurable partition are pairwise orthogonal and their squared norms add up to ‖ψ‖².
• Physicslib4.Spectral.exists_isStarProjection_tendsto_partialSum — a family of mutually annihilating projections sums to the projection onto the closed span of their ranges.

Implementation notes

Following Mathlib's MeasureTheory.VectorMeasure, a ProjectionValuedMeasure is a total function Set X → H →L[ℂ] H which is required to vanish on non-measurable sets; this makes the object canonical and avoids carrying measurability side conditions in the coercion.

The blueprint's countable additivity is stated as HasSum, Mathlib's unordered summability. For a family of pairwise orthogonal projections this is equivalent to convergence of the partial sums, which is the blueprint's formulation.

Two projection-valued measures are equivalent in the blueprint's sense exactly when they are equal as functions on Set X, so no separate relation is introduced.

structure Physicslib4.Spectral.ProjectionValuedMeasure (X : Type u_3) [MeasurableSpace X] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type (max u_3 u_4)

A projection-valued measure on X: an assignment E ↦ μ(E) of orthogonal projections on H to measurable sets, with μ(X) = 𝟙, countably additive and multiplicative on intersections.

It is the object the spectral theorem attaches to a self-adjoint operator A, with μ(E) the spectral projection of A for the set E of possible measured values. The axioms: each μ(E) is a self-adjoint idempotent; μ(X) = 𝟙; for pairwise disjoint measurable E_1, E_2, … and every vector v, μ(⋃ E_j)v = Σ μ(E_j)v with convergence in the norm of H; and μ(E ∩ F) = μ(E)μ(F), so projections of disjoint sets have orthogonal ranges. For each vector ψ, E ↦ ⟨ψ, μ(E)ψ⟩ is then a finite positive measure (assoc), and bounded measurable functions can be integrated against μ to give operators (integral).

Implementation note: as in Mathlib's MeasureTheory.VectorMeasure, μ is a total function Set X → H →L[ℂ] H that is 0 on non-measurable sets, so the coercion carries no measurability side conditions. The blueprint's μ(∅) = 0 is not a field: countable additivity for the constant family E_j = ∅ implies it, and a field would add a derivable obligation to every constructor. Countable additivity is stated with Mathlib's HasSum, unordered summation; since the vectors μ(E_j)v are pairwise orthogonal, this is equivalent to convergence of the partial sums. The blueprint's equivalence of two projection-valued measures is equality (ProjectionValuedMeasure.ext).

Blueprint: def:projection-valued-measure

• toFun : Set X → H →L[ℂ] H

  The underlying assignment E ↦ μ(E) of operators to all subsets of X.

• isStarProjection' (E : Set X) : IsStarProjection (self.toFun E)

  Every value μ(E) is an orthogonal projection: self-adjoint and idempotent.

• notMeasurable' (E : Set X) : ¬MeasurableSet E → self.toFun E = 0

  Non-measurable sets are sent to 0, so μ is determined by its values on measurable sets.

• univ' : self.toFun Set.univ = 1

  Normalisation: μ(X) is the identity operator.

• hasSum' (E : ℕ → Set X) : (∀ (j : ℕ), MeasurableSet (E j)) → (Pairwise fun (i j : ℕ) => Disjoint (E i) (E j)) → ∀ (v : H), HasSum (fun (j : ℕ) => (self.toFun (E j)) v) ((self.toFun (⋃ (j : ℕ), E j)) v)

  Countable additivity: for pairwise disjoint measurable sets E_j and every vector v, the series Σ μ(E_j)v converges in the norm of H to μ(⋃ E_j)v.

• inter' (E F : Set X) : MeasurableSet E → MeasurableSet F → self.toFun (E ∩ F) = self.toFun E * self.toFun F

  Multiplicativity: μ(E ∩ F) = μ(E)μ(F) for measurable E and F.

@[instance_reducible]

instance Physicslib4.Spectral.ProjectionValuedMeasure.instFunLike {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : FunLike (ProjectionValuedMeasure X H) (Set X) (H →L[ℂ] H)

Equations

• Physicslib4.Spectral.ProjectionValuedMeasure.instFunLike = { coe := Physicslib4.Spectral.ProjectionValuedMeasure.toFun, coe_injective := ⋯ }

@[simp]

theorem Physicslib4.Spectral.ProjectionValuedMeasure.coe_mk {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : Set X → H →L[ℂ] H) (h₁ : ∀ (E : Set X), IsStarProjection (f E)) (h₂ : ∀ (E : Set X), ¬MeasurableSet E → f E = 0) (h₃ : f Set.univ = 1) (h₄ : ∀ (E : ℕ → Set X), (∀ (j : ℕ), MeasurableSet (E j)) → (Pairwise fun (i j : ℕ) => Disjoint (E i) (E j)) → ∀ (v : H), HasSum (fun (j : ℕ) => (f (E j)) v) ((f (⋃ (j : ℕ), E j)) v)) (h₅ : ∀ (E F : Set X), MeasurableSet E → MeasurableSet F → f (E ∩ F) = f E * f F) : ⇑{ toFun := f, isStarProjection' := h₁, notMeasurable' := h₂, univ' := h₃, hasSum' := h₄, inter' := h₅ } = f

theorem Physicslib4.Spectral.ProjectionValuedMeasure.ext {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {μ ν : ProjectionValuedMeasure X H} (h : ∀ (E : Set X), μ E = ν E) : μ = ν

Two projection-valued measures agreeing as functions on Set X are equal.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.ext_iff {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {μ ν : ProjectionValuedMeasure X H} : μ = ν ↔ ∀ (E : Set X), μ E = ν E

The five structure fields, restated through the FunLike coercion.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isStarProjection_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (E : Set X) : IsStarProjection (μ E)

theorem Physicslib4.Spectral.ProjectionValuedMeasure.apply_of_not_measurableSet {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {E : Set X} (hE : ¬MeasurableSet E) : μ E = 0

@[simp]

theorem Physicslib4.Spectral.ProjectionValuedMeasure.apply_univ {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) : μ Set.univ = 1

theorem Physicslib4.Spectral.ProjectionValuedMeasure.hasSum_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (E : ℕ → Set X) (hE : ∀ (j : ℕ), MeasurableSet (E j)) (hdisj : Pairwise fun (i j : ℕ) => Disjoint (E i) (E j)) (v : H) : HasSum (fun (j : ℕ) => (μ (E j)) v) ((μ (⋃ (j : ℕ), E j)) v)

theorem Physicslib4.Spectral.ProjectionValuedMeasure.apply_inter {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) : μ (E ∩ F) = μ E * μ F

theorem Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_assoc {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) : ∃! ν : MeasureTheory.Measure X, MeasureTheory.IsFiniteMeasure ν ∧ ∀ (E : Set X), MeasurableSet E → (ν E).toReal = (inner ℂ ψ ((μ E) ψ)).re

For every ψ ∈ H there is a unique positive finite measure μ_ψ on X whose value on a measurable set E is ⟪ψ, μ(E) ψ⟫.

Blueprint reference: thrm:projection-valued-measures-associated-measure.

noncomputable def Physicslib4.Spectral.ProjectionValuedMeasure.assoc {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) : MeasureTheory.Measure X

The finite positive measure μ_ψ(E) = ⟨ψ, μ(E)ψ⟩ of a projection-valued measure μ and a vector ψ.

Since μ(E) is an orthogonal projection, ⟨ψ, μ(E)ψ⟩ = ‖μ(E)ψ‖² ≥ 0, and countable additivity of μ makes E ↦ ‖μ(E)ψ‖² a measure; its total mass is ⟨ψ, ψ⟩ = ‖ψ‖², by assoc_apply with E = X. For a unit vector ψ and the spectral measure of an observable A, μ_ψ(E) is the probability that a measurement of A in the state ψ gives a value in E. The values on measurable sets are assoc_apply; the operator-valued integral satisfies ⟨ψ, (∫ f dμ)ψ⟩ = ∫ f dμ_ψ (inner_integral).

Implementation note: the measure is chosen from existsUnique_assoc, which also gives its uniqueness and finiteness (the MeasureTheory.IsFiniteMeasure instance).

Blueprint: the measure μ_ψ of thrm:projection-valued-measures-associated-measure

Equations

• μ.assoc ψ = Exists.choose ⋯

instance Physicslib4.Spectral.ProjectionValuedMeasure.instIsFiniteMeasureAssoc {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) : MeasureTheory.IsFiniteMeasure (μ.assoc ψ)

theorem Physicslib4.Spectral.ProjectionValuedMeasure.assoc_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) {E : Set X} (hE : MeasurableSet E) : ((μ.assoc ψ) E).toReal = (inner ℂ ψ ((μ E) ψ)).re

theorem Physicslib4.Spectral.ProjectionValuedMeasure.inner_eq_zero_of_disjoint {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {n : ℕ} (E : Fin n → Set X) (hE : ∀ (i : Fin n), MeasurableSet (E i)) (hdisj : Pairwise fun (i j : Fin n) => Disjoint (E i) (E j)) (ψ : H) {i j : Fin n} (hij : i ≠ j) : inner ℂ ((μ (E i)) ψ) ((μ (E j)) ψ) = 0

For a finite pairwise disjoint measurable family E₁, …, Eₙ, the vectors μ(Eᵢ)ψ are pairwise orthogonal.

The blueprint additionally assumes that the Eᵢ cover X; that hypothesis is used only for the norm identity norm_sq_eq_sum_of_partition, not here, so it is omitted.

Blueprint reference: lmm:lemma2-of-operator-valued-integration (part 1).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.norm_sq_eq_sum_of_partition {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {n : ℕ} (E : Fin n → Set X) (hE : ∀ (i : Fin n), MeasurableSet (E i)) (hdisj : Pairwise fun (i j : Fin n) => Disjoint (E i) (E j)) (hcover : ⋃ (i : Fin n), E i = Set.univ) (ψ : H) : ‖ψ‖ ^ 2 = ∑ i : Fin n, ‖(μ (E i)) ψ‖ ^ 2

For a finite measurable partition E₁, …, Eₙ of X, ‖ψ‖² = ∑ᵢ ‖μ(Eᵢ)ψ‖².

Blueprint reference: lmm:lemma2-of-operator-valued-integration (part 2).

Sums of mutually annihilating projections

theorem Physicslib4.Spectral.exists_tendsto_partialSum_of_isStarProjection {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ → H →L[ℂ] H} (hP : ∀ (i : ℕ), IsStarProjection (P i)) (horth : ∀ (i j : ℕ), i ≠ j → P i * P j = 0) (ψ : H) : ∃ (l : H), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (P i) ψ) Filter.atTop (nhds l)

The partial sums ∑_{i<n} Pᵢ ψ of a family of mutually annihilating orthogonal projections converge in H.

Blueprint reference: prpstn:orthogonal-sum-converges.

theorem Physicslib4.Spectral.exists_isStarProjection_tendsto_partialSum' {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ → H →L[ℂ] H} (hP : ∀ (i : ℕ), IsStarProjection (P i)) (horth : ∀ (i j : ℕ), i ≠ j → P i * P j = 0) : ∃ (Q : H →L[ℂ] H), IsStarProjection Q ∧ ∀ (ψ : H), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (P i) ψ) Filter.atTop (nhds (Q ψ))

The pointwise limit of the partial sums of a family of mutually annihilating orthogonal projections is again a bounded orthogonal projection.

Blueprint reference: prpstn:orthogonal-sum-is-projection.

theorem Physicslib4.Spectral.range_eq_topologicalClosure_iSup_of_tendsto_partialSum {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ → H →L[ℂ] H} (hP : ∀ (i : ℕ), IsStarProjection (P i)) (horth : ∀ (i j : ℕ), i ≠ j → P i * P j = 0) (Q : H →L[ℂ] H) (hQ : ∀ (ψ : H), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (P i) ψ) Filter.atTop (nhds (Q ψ))) : (↑Q).range = (⨆ (i : ℕ), (↑(P i)).range).topologicalClosure

The range of the limit projection is the smallest closed subspace containing the ranges of the Pᵢ.

Blueprint reference: prpstn:orthogonal-sum-range.

theorem Physicslib4.Spectral.exists_isStarProjection_tendsto_partialSum {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ → H →L[ℂ] H} (hP : ∀ (i : ℕ), IsStarProjection (P i)) (horth : ∀ (i j : ℕ), i ≠ j → P i * P j = 0) : ∃ (Q : H →L[ℂ] H), IsStarProjection Q ∧ (∀ (ψ : H), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (P i) ψ) Filter.atTop (nhds (Q ψ))) ∧ (↑Q).range = (⨆ (i : ℕ), (↑(P i)).range).topologicalClosure

A family of mutually annihilating orthogonal projections sums pointwise to the orthogonal projection onto the smallest closed subspace containing all their ranges.

This blueprint node is exactly the conjunction of exists_isStarProjection_tendsto_partialSum' and range_eq_topologicalClosure_iSup_of_tendsto_partialSum, so it is proved from them rather than restated.

Blueprint reference: lmm:lemma-4.

theorem Physicslib4.Spectral.hasSum_of_isStarProjection_orthogonal {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ℕ → H →L[ℂ] H} (hP : ∀ (i : ℕ), IsStarProjection (P i)) (horth : ∀ (i j : ℕ), i ≠ j → P i * P j = 0) (Q : H →L[ℂ] H) (hQ : ∀ (ψ : H), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (P i) ψ) Filter.atTop (nhds (Q ψ))) (ψ : H) : HasSum (fun (i : ℕ) => (P i) ψ) (Q ψ)

A family of mutually annihilating orthogonal projections is unconditionally summable, and the (HasSum) value is the pointwise limit of the partial sums over Finset.range.

Blueprint reference: prpstn:mua-countably-additive.