RegularCoreDescent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Descent from the actual regular cores

The action, character multipliers, faithful embedding, and joint fixed algebra are the concrete regular objects. The only structural inputs are the published commutant and diagonal-decomposition theorems. A supplied nearby core conjugacy descends by the proved scalar character mean and UCP perturbation argument.

theorem OAI.KadisonKastler.kkDistance_regularCore_le_of_common_matrix_units line 28

Source documentation

A common full matrix corner supplies the complete tensor comparison needed before taking the common-action fixed points.

theorem kkDistance_regularCore_le_of_common_matrix_units
    (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)
    (D : Submodule ℂ H) [CompleteSpace D] (F : FullMatrixCorner D)
    (hFM : ∀ i j, F.entry i j ∈ M) (hFN : ∀ i j, F.entry i j ∈ N) :
    kkDistance (regularCoreAlgebra U hU M) (regularCoreAlgebra U hU N) ≤
      kkDistance M N :=
…

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

theorem OAI.KadisonKastler.concrete_unitary_of_regularCore_conjugacy line 50

Source documentation

The actual regular-core conjugacy descends to the original Hilbert space with the quantitative UCP bound.

theorem concrete_unitary_of_regularCore_conjugacy
    (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)
    (hN : ∀ s T, T ∈ N → unitaryConj (U s) T ∈ N)
…

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