Spectral theorem for unbounded self-adjoint operators (Solution)

Redeclare-bridge: PVM and StrongContUnitary are restated verbatim in the PalomarSpectralStone namespace (matching SpectralStoneChallenge.lean), with conversion functions to and from the proof library's independently-elaborated copies. spectral_theorem_intrinsic and stone_theorem_intrinsic are restated and closed by transporting the library's theorems across that conversion.

structure PalomarSpectralStone.PVM (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : Type u_2

A projection-valued measure on ℝ, countably additive in the strong operator topology. Its laws are imposed on Borel-measurable sets.

• proj : Set ℝ → E →L[ℂ] E

  The orthogonal projection assigned to a measurable subset of the real line.

• isOrthogonalProjection (S : Set ℝ) : MeasurableSet S → IsSelfAdjoint (self.proj S) ∧ IsIdempotentElem (self.proj S)
• empty : self.proj ∅ = 0
• univ : self.proj Set.univ = 1
• inter (S T : Set ℝ) : MeasurableSet S → MeasurableSet T → self.proj (S ∩ T) = self.proj S * self.proj T
• countably_additive (S : ℕ → Set ℝ) : (∀ (i : ℕ), MeasurableSet (S i)) → Pairwise (Function.onFun Disjoint S) → ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (self.proj (S i)) x) Filter.atTop (nhds ((self.proj (⋃ (i : ℕ), S i)) x))

def PalomarSpectralStone.PVM.Represents {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (A : E →ₗ.[ℂ] E) : Prop

E_pvm represents A when its scalar measures are the diagonal matrix coefficients of the spectral projections, A has precisely their finite second-moment domain, and the diagonal matrix coefficient of A is their first moment. Complex polarization recovers all mixed matrix coefficients.

Equations

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

def PalomarSpectralStone.PVM.ofRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (p : _root_.PVM E) : PVM E

Repackage a library PVM as a PalomarSpectralStone.PVM with the same fields.

Equations

• PalomarSpectralStone.PVM.ofRoot p = { proj := p.proj, isOrthogonalProjection := ⋯, empty := ⋯, univ := ⋯, inter := ⋯, countably_additive := ⋯ }

def PalomarSpectralStone.PVM.toRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (p : PVM E) : _root_.PVM E

Repackage a PalomarSpectralStone.PVM as a library PVM with the same fields.

Equations

• p.toRoot = { proj := p.proj, isOrthogonalProjection := ⋯, empty := ⋯, univ := ⋯, inter := ⋯, countably_additive := ⋯ }

theorem PalomarSpectralStone.PVM.represents_ofRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : _root_.PVM E} {A : E →ₗ.[ℂ] E} : (ofRoot p).Represents A ↔ p.Represents A

theorem PalomarSpectralStone.PVM.represents_toRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : PVM E} {A : E →ₗ.[ℂ] E} : p.toRoot.Represents A ↔ p.Represents A

theorem PalomarSpectralStone.spectral_theorem_intrinsic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : ∃ (E_pvm : PVM E), E_pvm.Represents A ∧ ∀ (F_pvm : PVM E), F_pvm.Represents A → ∀ (S : Set ℝ), MeasurableSet S → E_pvm.proj S = F_pvm.proj S

Every unbounded self-adjoint operator has a real PVM spectral representation, unique on Borel-measurable sets.

structure PalomarSpectralStone.StrongContUnitary (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : Type u_2

A strongly continuous one-parameter unitary group.

• toFun : ℝ → E →L[ℂ] E

  The unitary operator at each real time.

• isUnitary (t : ℝ) : self.toFun t ∈ unitary (E →L[ℂ] E)
• zero : self.toFun 0 = 1
• add (s t : ℝ) : self.toFun (s + t) = self.toFun s * self.toFun t
• stronglyContinuous (x : E) : Continuous fun (t : ℝ) => (self.toFun t) x

def PalomarSpectralStone.StrongContUnitary.Generates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (A : E →ₗ.[ℂ] E) : Prop

U has infinitesimal generator A: its domain is exactly the vectors whose Stone difference quotient converges, and the limit is A.

Equations

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

def PalomarSpectralStone.StrongContUnitary.ofRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (u : _root_.StrongContUnitary E) : StrongContUnitary E

Repackage a library StrongContUnitary with the same fields.

Equations

• PalomarSpectralStone.StrongContUnitary.ofRoot u = { toFun := u.toFun, isUnitary := ⋯, zero := ⋯, add := ⋯, stronglyContinuous := ⋯ }

def PalomarSpectralStone.StrongContUnitary.toRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (u : StrongContUnitary E) : _root_.StrongContUnitary E

Repackage a PalomarSpectralStone.StrongContUnitary as a library one.

Equations

• u.toRoot = { toFun := u.toFun, isUnitary := ⋯, zero := ⋯, add := ⋯, stronglyContinuous := ⋯ }

theorem PalomarSpectralStone.StrongContUnitary.generates_ofRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {u : _root_.StrongContUnitary E} {A : E →ₗ.[ℂ] E} : (ofRoot u).Generates A ↔ u.Generates A

theorem PalomarSpectralStone.StrongContUnitary.generates_toRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {u : StrongContUnitary E} {A : E →ₗ.[ℂ] E} : u.toRoot.Generates A ↔ u.Generates A

theorem PalomarSpectralStone.stone_theorem_intrinsic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : (∀ (U : StrongContUnitary E), ∃ (A : E →ₗ.[ℂ] E), IsSelfAdjoint A ∧ U.Generates A) ∧ ∀ (A : E →ₗ.[ℂ] E), IsSelfAdjoint A → ∃ (U : StrongContUnitary E), U.Generates A

Stone's theorem: every strongly continuous unitary group has a self-adjoint generator, and every self-adjoint operator generates such a group.