RegularCoreGap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The regular core gap from the tensor gap

The fixed-point comparison uses the actual invariant mean for the additive real group. It does not assert that an ordinary gap survives tensor amplification: the tensor gap remains explicit in this theorem.

theorem OAI.KadisonKastler.kkDistance_regularCore_le_tensor line 27

Source documentation

For one common regular action, passage from the tensor algebras to their actual generated cores decreases the gap.

theorem kkDistance_regularCore_le_tensor
    (hComm : PublishedRegularCommutant.{u})
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ =>
      (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (M N : VonNeumannAlgebra H)
    (hM : ∀ s T, T ∈ M → unitaryConj (U s) T ∈ M)
    (hN : ∀ s T, T ∈ N → unitaryConj (U s) T ∈ N) :
    kkDistance (regularCoreAlgebra U hU M) (regularCoreAlgebra U hU N) ≤
      kkDistance (regularTensorAlgebra M) (regularTensorAlgebra N) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.regularTensorAlgebra