FiniteFactorSymmetrization.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite-factor averaging stage uses actual normalized Haar measures on the finite matrix-unitary groups. Their continuity and weak integrability are proved here; the resulting operator is within the original scalar commutator bound and has scalar commutator bound at most three times it.

def OAI.KadisonSimilarity.matrixUnitaryAction line 31

Source documentation

Restriction of a matrix representation to its unitary group.

def matrixUnitaryAction (R : Matrix α α ℂ →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    Matrix.unitaryGroup α ℂ →* (H →L[ℂ] H) :=
…

theorem OAI.KadisonSimilarity.matrixUnitaryAction_norm_le line 35
theorem OAI.KadisonSimilarity.matrixUnitaryAction_adjoint line 41
theorem OAI.KadisonSimilarity.matrixUnitaryAction_continuous line 49
Source documentation
Finite-dimensional continuity proves strong continuity of the action.
```
theorem matrixUnitaryAction_continuous (R : Matrix α α ℂ →⋆ₐ[ℂ] (H →L[ℂ] H)) (x : H) :
    Continuous (fun u : Matrix.unitaryGroup α ℂ => matrixUnitaryAction R u x) := by
…
```
Mentions: OAI.KadisonSimilarity.matrixUnitaryAction
theorem OAI.KadisonSimilarity.commutes_matrix_of_unitaries line 56
Source documentation
Commutation with matrix unitaries implies commutation with every matrix, by the four-unitary spanning theorem in the actual C-star matrix algebra.
```
theorem commutes_matrix_of_unitaries [Nonempty α]
    (R : Matrix α α ℂ →⋆ₐ[ℂ] (H →L[ℂ] H))
    (S : H →L[ℂ] H) (hS : ∀ u, commutator S (matrixUnitaryAction R u) = 0)
    (a : Matrix α α ℂ) : commutator S (R a) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixUnitaryAction
def OAI.KadisonSimilarity.finiteMatrixHaarProbability line 100
Source documentation
Normalized Haar measure on each actual finite matrix-unitary group.
```
def finiteMatrixHaarProbability (n : ℕ) : Measure (Matrix.unitaryGroup (I n) ℂ) :=
…
```
instance OAI.KadisonSimilarity.finiteMatrixHaarProbability_probability line 103
instance OAI.KadisonSimilarity.finiteMatrixHaarProbability_leftInvariant line 109

theorem OAI.KadisonSimilarity.exists_finite_matrix_symmetrization line 116

Source documentation

Actual Haar averaging over increasing matrix stages produces the finite-factor perturbation with the manuscript's factor-three estimate.

theorem exists_finite_matrix_symmetrization
    [∀ n, Nonempty (I n)]
    (M : VonNeumannAlgebra H)
    (R : ∀ n, Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hmem : ∀ n a, R n a ∈ M)
    (ι : ∀ n m, n ≤ m → Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] Matrix (I m) (I m) ℂ)
    (hcompat : ∀ n m h a, R m (ι n m h a) = R n a)
    (Y : H →L[ℂ] H) :
    ∃ Y₀ : H →L[ℂ] H, ‖Y₀‖ ≤ ‖Y‖ ∧
      ‖Y₀ - Y‖ ≤ scalarCommutatorNorm M Y ∧
      scalarCommutatorNorm M Y₀ ≤ 3 * scalarCommutatorNorm M Y ∧
      ∀ n a, commutator Y₀ (R n a) = 0 := by
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.exists_generated_factor_symmetrization line 144

Source documentation

Double-commutant generation extends the finite-stage conclusion to the whole generated subfactor. No extra invariant operator is assumed.

theorem exists_generated_factor_symmetrization
    [∀ n, Nonempty (I n)]
    (M N : VonNeumannAlgebra H)
    (R : ∀ n, Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hmem : ∀ n a, R n a ∈ M)
    (ι : ∀ n m, n ≤ m → Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] Matrix (I m) (I m) ℂ)
    (hcompat : ∀ n m h a, R m (ι n m h a) = R n a)
    (hgenerate : (N : Set (H →L[ℂ] H)) = Set.centralizer
      (Set.centralizer {x | ∃ n a, R n a = x}))
    (Y : H →L[ℂ] H) :
    ∃ Y₀ : H →L[ℂ] H, ‖Y₀‖ ≤ ‖Y‖ ∧
      ‖Y₀ - Y‖ ≤ scalarCommutatorNorm M Y ∧
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm