FiniteTypeIEstimate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite type-I branch of the factor argument. Actual normalized matrix-unitary averaging puts the operator within its scalar commutator norm of the commutant, giving complete commutator constant two.

theorem OAI.KadisonSimilarity.finiteTypeI_commutator_estimate line 19
Source documentation
A represented full finite matrix algebra has the uniform matrix commutator estimate with constant two, in every multiplicity.
```
theorem finiteTypeI_commutator_estimate (P : VonNeumannAlgebra H)
    (ι : Matrix α α ℂ →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hmem : ∀ a, ι a ∈ P)
    (hsurj : ∀ T : H →L[ℂ] H, T ∈ P → ∃ a, ι a = T) :
    CommutatorEstimate P 2 := by
…
```
Mentions: OAI.KadisonSimilarity.CommutatorEstimate