MatrixAveraging.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Averaging over a concrete finite matrix algebra

Signed permutation matrices give a finite unitary group whose commutant is exactly the commutant of the matrix-unit system. Its uniform average preserves the original scalar derivation bound.

def OAI.KadisonKastler.matrixUnitSignedRepresentation line 23
Source documentation
The signed permutations of a given concrete matrix-unit system.
```
def matrixUnitSignedRepresentation (E : Generator.MatrixUnitSystem ι A) :
    SignedPermutation ι →* unitary A where
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.SignedPermutation
theorem OAI.KadisonKastler.matrixUnitSignedRepresentation_mem line 39
theorem OAI.KadisonKastler.matrixUnitSignedRepresentation_inl line 43
theorem OAI.KadisonKastler.matrixUnitSignedRepresentation_inr line 50
theorem OAI.KadisonKastler.signDiagonal_reflection line 60
Source documentation
Changing one diagonal sign isolates the corresponding diagonal matrix unit.
```
theorem signDiagonal_reflection (i : ι) :
    signDiagonal (Function.update (1 : ι → ℤˣ) i (-1)) =
      1 - (2 : ℂ) • Matrix.single i i 1 := by
…
```
Mentions: OAI.KadisonKastler.signDiagonal
theorem OAI.KadisonKastler.matrixUnit_diagonal_sandwich line 73
theorem OAI.KadisonKastler.commute_matrixUnits_of_signed line 82
Source documentation
Commuting with the finite signed-permutation group is enough to commute with the entire full matrix algebra.
```
theorem commute_matrixUnits_of_signed (E : Generator.MatrixUnitSystem ι A) (x : A)
    (hx : ∀ g, Commute (matrixUnitSignedRepresentation E g : A) x) :
    ∀ i j, Commute (E.entry i j) x := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixUnitSignedRepresentation
def OAI.KadisonKastler.matrixUnitAverage line 102
Source documentation
The actual finite-matrix average of an arbitrary ambient operator.
```
def matrixUnitAverage (E : Generator.MatrixUnitSystem ι (H →L[ℂ] H))
    (h : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem
theorem OAI.KadisonKastler.matrixUnitAverage_commutes line 106

theorem OAI.KadisonKastler.exists_matrixUnitAverage line 113

Source documentation

Finite-dimensional averaging improves the commutant without enlarging either the displacement or the derivation bound.

theorem exists_matrixUnitAverage (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‖) :
    ∃ h0 : H →L[ℂ] H,
      (∀ a ∈ E.algebra, Commute a h0) ∧ ‖h - h0‖ ≤ δ ∧
      (∀ a ∈ M, ‖h0 * a - a * h0‖ ≤ δ * ‖a‖) ∧
      (IsSelfAdjoint h → IsSelfAdjoint h0) := by
…

Mentions: OAI.Generator.MatrixUnitSystem