RegularCoreSemifinite.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Descent from a type II∞ regular core

All matrix, injectivity, and finite-corner data are constructed from the ordinary projection-theoretic type II∞ predicate and the published countable copy theorem. The source-core orientation is retained.

theorem OAI.KadisonKastler.regularCore_spatial_of_typeIIInfinity line 31

Source documentation

A type II∞ source core yields conjugacy on the original Hilbert space.

theorem regularCore_spatial_of_typeIIInfinity
    (h : FiniteFactorPublishedInputs.{u})
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (hM : ∀ s T, T ∈ M → unitaryConj (U s) T ∈ M)
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryConj