ScalarAmplification.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The amplified commutator estimate for finite matrix lifts

def OAI.KadisonKastler.diagonalAmplification line 16
Source documentation
The constant diagonal amplification of an element.
```
def diagonalAmplification (a : A) : CStarMatrix n n A :=
…
```
theorem OAI.KadisonKastler.diagonalAmplification_sub line 20
theorem OAI.KadisonKastler.diagonalAmplification_commute line 27
Source documentation
An element commuting with every matrix entry commutes with that matrix when amplified on the diagonal.
```
theorem diagonalAmplification_commute (a : A) (s : CStarMatrix n n A)
    (hs : ∀ i j, Commute a (s i j)) : Commute (diagonalAmplification a) s := by
…
```
Mentions: OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.norm_diagonalAmplification_le line 38

theorem OAI.KadisonKastler.norm_amplified_commutator_le line 45

Source documentation

A nearby element commuting with all entries of a unitary matrix controls the amplified commutator, independently of the matrix size.

theorem norm_amplified_commutator_le (a b : A) (s : unitary (CStarMatrix n n A))
    {δ : ℝ} (hab : ‖a - b‖ ≤ δ) (hs : ∀ i j, Commute b ((s : CStarMatrix n n A) i j)) :
    ‖diagonalAmplification a * (s : CStarMatrix n n A) -
      (s : CStarMatrix n n A) * diagonalAmplification a‖ ≤ 2 * δ := by
…

Mentions: OAI.KadisonKastler.diagonalAmplification

theorem OAI.KadisonKastler.matrixUnit_lift_commutator_le line 77

Source documentation

The controlled-representative estimate in the free-lift construction: a unitary matrix over a finite matrix subalgebra has commutator at most 2δ, where δ controls the scalar derivation on the ambient algebra.

theorem matrixUnit_lift_commutator_le (M : VonNeumannAlgebra H)
    (E : Generator.MatrixUnitSystem ι (H →L[ℂ] H)) (hE : E.algebra ≤ M.toStarSubalgebra)
    (h : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hb : ∀ a ∈ M, ‖h * a - a * h‖ ≤ δ * ‖a‖)
    (s : unitary (CStarMatrix n n (H →L[ℂ] H)))
    (hs : ∀ i j, (s : CStarMatrix n n (H →L[ℂ] H)) i j ∈ E.algebra) :
    ‖diagonalAmplification h * (s : CStarMatrix n n (H →L[ℂ] H)) -
      (s : CStarMatrix n n (H →L[ℂ] H)) * diagonalAmplification h‖ ≤ 2 * δ := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.diagonalAmplification