Documentation

LeanPool.SpectralTheory.Spectral.Spectral.Intrinsic

Intrinsic statement of the unbounded spectral theorem #

This file packages the spectral representation without exposing the library's particular construction of the unbounded spectral integral. The scalar measure of a vector is fixed by the PVM's diagonal matrix coefficients, the operator domain is exactly the finite-second-moment space, and the operator's diagonal matrix coefficient is the first moment.

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

A PVM intrinsically represents a partial linear operator when its scalar spectral measures give the exact domain and first-moment quadratic form.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PVM.represents_of_unboundedIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (A : E →ₗ.[ℂ] E) (h : E_pvm.unboundedIntegral Complex.ofReal ⋯ = A) :
    E_pvm.Represents A

    Equality with the coordinate spectral integral supplies an intrinsic representation.

    source
    theorem spectral_theorem_intrinsic_existence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) :
    ∃ (E_pvm : PVM E), E_pvm.Represents A

    Every self-adjoint partial linear operator has an intrinsic spectral representation by a real projection-valued measure.

    source
    theorem PVM.Represents.unboundedIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {E_pvm : PVM E} {A : E →ₗ.[ℂ] E} (hrep : E_pvm.Represents A) (hA : IsSelfAdjoint A) :
    E_pvm.unboundedIntegral Complex.ofReal ⋯ = A

    The intrinsic representation is equivalent to the library's spectral integral representation. In particular, its diagonal moment formulation does not weaken the operator equality: complex polarization recovers every mixed matrix coefficient.

    source
    theorem PVM.represents_iff_unboundedIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) :
    E_pvm.Represents A ↔ E_pvm.unboundedIntegral Complex.ofReal ⋯ = A

    For self-adjoint operators, the intrinsic and constructed spectral integral formulations are logically equivalent.

    source
    theorem PVM.Represents.proj_eq_on_measurable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : E →ₗ.[ℂ] E} (hA : IsSelfAdjoint A) {E₁ E₂ : PVM E} (h₁ : E₁.Represents A) (h₂ : E₂.Represents A) (S : Set ℝ) (hS : MeasurableSet S) :
    E₁.proj S = E₂.proj S

    Intrinsic representations of a self-adjoint operator have the same spectral projections on every measurable set.

    source
    theorem 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

    The unbounded spectral theorem in intrinsic PVM form: every self-adjoint partial operator has a spectral representation, unique on Borel sets.