ClippedDrift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The clipped coefficient-column drift

Finite matrix averaging preserves the scalar derivation bound. The support column estimate and the through-label square sum give 64δ for the averaged operator; its distance at most δ from the original operator costs 2δ.

theorem OAI.KadisonKastler.hilbertMatrix_matrixCommutator line 33
Source documentation
The matrix commutator acts as the ordinary commutator on the Hilbert direct sum.
```
theorem hilbertMatrix_matrixCommutator (h : H →L[ℂ] H)
    (K : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    hilbertMatrix (matrixCommutator h K) =
      hilbertMatrix (diagonalAmplification (n := Fin n) h) * hilbertMatrix K -
…
```
Mentions: OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.matrixCommutator, OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.hilbertMatrix_supportProjection line 45
Source documentation
A support projection is the sum of its actual Hilbert-space diagonal atoms.
```
theorem hilbertMatrix_supportProjection
    (E : Generator.MatrixUnitSystem (Fin q) (H →L[ℂ] H))
    (S : Finset (Fin n × Fin q)) :
    hilbertMatrix (supportProjection E S) =
      ∑ a ∈ S, hilbertMatrix (supportAtom E a) := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.supportProjection, OAI.KadisonKastler.supportAtom
theorem OAI.KadisonKastler.clipped_coefficient_drift_le_sixty_six line 55
Source documentation
The original implementing operator moves the contractive clipped coefficient column by at most 66δ.
```
theorem clipped_coefficient_drift_le_sixty_six {ω : Type*} [Fintype ω]
    (M : VonNeumannAlgebra H)
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.clipped_matrixCommutator_drift_le_sixty_six line 112
Source documentation
The same estimate expressed entrywise in the original operator algebra.
```
theorem clipped_matrixCommutator_drift_le_sixty_six {ω : Type*} [Fintype ω]
    (M : VonNeumannAlgebra H)
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra