Imports
/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module
public import Mathlib.Analysis.InnerProductSpace.Adjoint
public import Mathlib.MeasureTheory.VectorMeasure.BasicSpectral measures
i. Overview
A spectral measure μS on a measurable space α is a σ-additive function Set α → H →L[ℂ] H
such that each set is mapped to a star projection on H, the empty set and non-measurable sets are
mapped to zero, and univ is mapped to the identity.
This is implemented as a structure extending VectorMeasure α (H →L[ℂ] H) with additional fields
constraining μS A to be a star projection for each set A and μS univ = 1.
For each x : H there is an associated measure μₓ given by μₓ A = ‖μS A x‖² = ⟪x, μS A x⟫ ≤ 1.
ii. Key results
SpectralMeasure : A star projection-valued measure.
comp_eq_of_inter : For a spectral measure μS and measurable sets A and B,
the composition μS A ∘ μS B = μS (A ∩ B).
iii. Table of contents
A. Definition
B. Composition
iv. References
@[expose] public sectioninstance (H : Type*) [SeminormedAddCommGroup H] [InnerProductSpace ℂ H] :
IsAddTorsionFree (H →L[ℂ] H) where
nsmul_right_injective n hn := H:Type u_1inst✝¹:SeminormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hn:ℕhn:n ≠ 0⊢ Function.Injective fun a => n • a
H:Type u_1inst✝¹:SeminormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hn:ℕhn:n ≠ 0x:H →L[ℂ] H⊢ (fun f => (↑n)⁻¹ • f) ((fun a => n • a) x) = x
All goals completed! 🐙A. Definition
A spectral measure on a measurable space α is a σ-additive function Set α → H →L[ℂ] H
such that each set is mapped to a star projection on H, the empty set and non-measurable sets
are mapped to zero, and univ is mapped to the identity.
structure SpectralMeasure
(α : Type*) [MeasurableSpace α]
(H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
extends VectorMeasure α (H →L[ℂ] H) where
isStarProjection' : ∀ A, IsStarProjection (measureOf' A)
univ' : measureOf' univ = 1attribute [coe] toVectorMeasureinstance instCoeVectorMeasure : Coe (SpectralMeasure α H) (VectorMeasure α (H →L[ℂ] H)) :=
⟨toVectorMeasure⟩instance instCoeFun : CoeFun (SpectralMeasure α H) fun _ ↦ Set α → H →L[ℂ] H :=
⟨fun μS ↦ ⇑μS.toVectorMeasure⟩lemma isStarProjection (A : Set α) : IsStarProjection (μS A) := μS.isStarProjection' A@[simp]
lemma univ : μS univ = 1 := μS.univ'B. Composition
@[simp]
lemma comp_self (A : Set α) : μS A ∘L μS A = μS A := (μS.isStarProjection A).isIdempotentElemα:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αh:Disjoint A BhA:MeasurableSet AhB:MeasurableSet B⊢ ↑μS A ∘SL ↑μS (A ∪ B) = ↑μS A
α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αh:Disjoint A BhA:MeasurableSet AhB:MeasurableSet B⊢ IsStarProjection (↑μS (A ∪ B) - ↑μS A)
All goals completed! 🐙α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhA:MeasurableSet AhB:MeasurableSet B⊢ ↑μS (B ∩ A) ∘SL ↑μS (B ∩ A) + 0 + (0 + ↑μS (A \ B) ∘SL ↑μS (B \ A)) = ↑μS (B ∩ A)
All goals completed! 🐙lemma commute (A B : Set α) : Commute (μS A) (μS B) := α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set α⊢ Commute (↑μS A) (↑μS B)
α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:MeasurableSet A ∧ MeasurableSet B⊢ Commute (↑μS A) (↑μS B)α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)⊢ Commute (↑μS A) (↑μS B)
α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:MeasurableSet A ∧ MeasurableSet B⊢ Commute (↑μS A) (↑μS B) All goals completed! 🐙
α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)⊢ Commute (↑μS A) (↑μS B) α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)hA:¬MeasurableSet A⊢ Commute (↑μS A) (↑μS B)α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)hB:¬MeasurableSet B⊢ Commute (↑μS A) (↑μS B) α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)hA:¬MeasurableSet A⊢ Commute (↑μS A) (↑μS B)α:Type u_1inst✝³:MeasurableSpace αH:Type u_2inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HμS:SpectralMeasure α HA:Set αB:Set αhAB:¬(MeasurableSet A ∧ MeasurableSet B)hB:¬MeasurableSet B⊢ Commute (↑μS A) (↑μS B) All goals completed! 🐙