CommonCentralData.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The common spectral model supplies the actual central-decomposition data for a weakly generating separable source. Factoriality is proved separately using the joint source.

def OAI.KadisonSimilarity.commonCentralField line 24

Source documentation

All operators commuting with the center acquire fields in the single common spectral model.

def commonCentralField (P : VonNeumannAlgebra H)
    (hcentral : starSubalgebraCommutant π.range = (vonNeumannCenter P).commutant)
    (T : (vonNeumannCenter P).commutant.toStarSubalgebra) :
    WeakDual.characterSpace ℂ A → ScalarHilbertCoordinates D.generators →L[ℂ]
      ScalarHilbertCoordinates D.generators :=
…

Mentions: OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.ScalarHilbertCoordinates

theorem OAI.KadisonSimilarity.commonCentralField_action line 31

def OAI.KadisonSimilarity.commonProjectionCentralData line 42

Source documentation

Central decomposition with all scalar/matrix norms and countable contraction tests derived from the common spectral embedding.

def commonProjectionCentralData (P : VonNeumannAlgebra H)
    (B : StarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (B : Set (H →L[ℂ] H))]
    [TopologicalSpace.SeparableSpace B]
    (hB : B ≤ P.toStarSubalgebra)
    (hBgen : representationVonNeumannAlgebra B.subtype = P)
    (hcentral : starSubalgebraCommutant π.range = (vonNeumannCenter P).commutant)
    (s : Set (WeakDual.characterSpace ℂ A)) (hs : MeasurableSet s)
    (hnull : (cyclicCommonBaseMeasure π D) sᶜ = 0)
    (ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ]
      (ScalarHilbertCoordinates D.generators →L[ℂ] ScalarHilbertCoordinates D.generators))
    (hρ : ∀ b : B, ∀ f : CommonCyclicHilbert π D,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → WeakDual.characterSpace ℂ A)
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.CommonCyclicHilbert