CoreMatrixDescent.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-corner argument followed by character descent

This combines the proved common-action gap estimate, injective-matrix finite-corner conjugacy, and the actual character average. The concrete core fixed-point identities remain explicit representation data.

theorem OAI.KadisonKastler.spatial_of_core_matrix_data line 32

Source documentation

A small gap of the upper invariant algebras gives a concrete conjugacy of the originals, with the finite-corner modulus.

theorem spatial_of_core_matrix_data
    (h : FiniteFactorPublishedInputs.{v}) (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (mU : ScalarInvariantMean G) (mV : ScalarInvariantMean L)
    (U : G →* unitary (K →L[ℂ] K)) (V : L →* unitary (K →L[ℂ] K))
    (A B : VonNeumannAlgebra K)
    (hA : ∀ g T, T ∈ A → unitaryConj (U g) T ∈ A)
    (hB : ∀ g T, T ∈ B → unitaryConj (U g) T ∈ B)
    (hV : ∀ l T, T ∈ fixedPointAlgebra U B →
      unitaryConj (V l) T ∈ fixedPointAlgebra U B)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
…

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