TwoFrequencyCoreFactor.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Factoriality of the core from two site frequencies

This is the fixed tensor-factor argument of the manuscript. Its product hypotheses concern local swaps and two explicit site eigenoperators. These hypotheses imply factoriality of the crossed product.

theorem OAI.KadisonKastler.scalarCenter_regularCore_of_two_site_frequencies line 28

Source documentation

Independent product swaps and two incommensurable site frequencies force the actual regular crossed product of a tensor factor to be a factor.

theorem scalarCenter_regularCore_of_two_site_frequencies
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (M : VonNeumannAlgebra H) (hM : ScalarCenter M)
    (D : VonNeumannAlgebra K) (Ω : K) (hΩ : ‖Ω‖ = 1)
    (L : LocalProductSwaps D Ω)
    (hsep : Function.Injective (algebraVectorMap D Ω))
    (U : Multiplicative ℝ →* unitary (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) ξ))
    (hP : ∀ s x, x ∈ spatialProductAlgebra M D →
      unitaryConj (U s) x ∈ spatialProductAlgebra M D)
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.LocalProductSwaps, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.unitaryConj