RegularSpatialField.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

First-leg fields in the relative commutant of the product centralizer

theorem OAI.KadisonKastler.first_leg_field_of_product_centralizer line 22

Source documentation

In the Fourier decomposition of a central core operator, constant product-centralizer commutation removes the entire second tensor leg. The coefficient field is obtained by a concrete slice, so measurability and its norm bound are retained.

theorem first_leg_field_of_product_centralizer
    (M : VonNeumannAlgebra H) {D : VonNeumannAlgebra K} {Ω : K}
    (L : LocalProductSwaps D Ω) (hΩ : ‖Ω‖ = 1)
    (hsep : Function.Injective (algebraVectorMap D Ω))
    (F : ℝ → SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (T : RegularCoreHilbert (SpatialHilbert H K) →L[ℂ]
      RegularCoreHilbert (SpatialHilbert H K))
    (hFT : RepresentsOperatorField volume F T)
    (hmeas : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume)
    (C : ℝ) (hbound : ∀ᵐ t ∂volume, ‖F t‖ ≤ C)
    (hT : T ∈ regularTensorAlgebra (spatialProductAlgebra M D))
    (hcomm : ∀ u : unitary (K →L[ℂ] K), (u : K →L[ℂ] K) ∈ D →
…

Mentions: OAI.KadisonKastler.LocalProductSwaps, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.spatialProductAlgebra