MatrixTracialGNS.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Normalized matrix traces and their actual GNS Hilbert spaces. The GNS space of M_n(A) is identified with the square array of copies of the GNS space of A; its algebra vectors have entries n^(-1/2) V(a_ij).

theorem OAI.KadisonSimilarity.denseRange_hilbert_entries line 16

Source documentation

Coordinatewise dense maps stay dense in a finite Hilbert sum.

private theorem denseRange_hilbert_entries {J D B : Type*} [Fintype J]
    [NormedAddCommGroup B] [NormedSpace ℂ B] (f : D → B) (hf : DenseRange f) :
    DenseRange (fun x : J → D => WithLp.toLp 2 (fun j => f (x j))) := by
…

def OAI.KadisonSimilarity.normalizedMatrixTraceLinear line 34

Source documentation

The normalized sum of the diagonal functionals.

def normalizedMatrixTraceLinear (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    CStarMatrix (Fin n) (Fin n) A →ₗ[ℂ] ℂ where
…

theorem OAI.KadisonSimilarity.matrix_diagonal_nonneg line 46
Source documentation
Positivity of a matrix gives positivity of each diagonal entry.
```
theorem matrix_diagonal_nonneg (X : CStarMatrix (Fin n) (Fin n) A)
    (hX : 0 ≤ X) (i : Fin n) : 0 ≤ X i i := by
…
```
def OAI.KadisonSimilarity.normalizedMatrixTrace line 56
Source documentation
The normalized matrix trace as a positive linear functional.
```
def normalizedMatrixTrace (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    CStarMatrix (Fin n) (Fin n) A →ₚ[ℂ] ℂ :=
…
```
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_apply line 62
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_one line 66
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_tracial line 70

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_star_mul line 84

Source documentation

Entrywise formula for the matrix GNS inner product.

theorem normalizedMatrixTrace_star_mul (τ : A →ₚ[ℂ] ℂ)
    (X Y : CStarMatrix (Fin n) (Fin n) A) :
    normalizedMatrixTrace τ n (star X * Y) =
      (n : ℂ)⁻¹ * ∑ i : Fin n, ∑ j : Fin n, τ (star (X i j) * Y i j) := by
…

Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace

abbrev OAI.KadisonSimilarity.MatrixGNSArray line 94
Source documentation
Square arrays use the ordinary Hilbert sum norm in both coordinates.
```
abbrev MatrixGNSArray (τ : A →ₚ[ℂ] ℂ) (n : ℕ) :=
…
```
def OAI.KadisonSimilarity.matrixGNSArrayLinear line 98
Source documentation
The unscaled array of represented matrix entries.
```
def matrixGNSArrayLinear (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    CStarMatrix (Fin n) (Fin n) A →ₗ[ℂ] MatrixGNSArray τ n where
…
```
Mentions: OAI.KadisonSimilarity.MatrixGNSArray
theorem OAI.KadisonSimilarity.matrixGNSArrayLinear_apply line 109
def OAI.KadisonSimilarity.matrixGNSScale line 114
Source documentation
Normalization converting the array norm into normalized tracial L² norm.
```
def matrixGNSScale (n : ℕ) : ℝ := (Real.sqrt n)⁻¹
```
theorem OAI.KadisonSimilarity.matrixGNSScale_pos line 116
theorem OAI.KadisonSimilarity.matrixGNSScale_sq line 121
def OAI.KadisonSimilarity.matrixGNSVector line 125
Source documentation
Normalized represented matrix vectors.
```
def matrixGNSVector (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    CStarMatrix (Fin n) (Fin n) A →ₗ[ℂ] MatrixGNSArray τ n :=
…
```
Mentions: OAI.KadisonSimilarity.MatrixGNSArray
theorem OAI.KadisonSimilarity.matrixGNSVector_apply line 129
theorem OAI.KadisonSimilarity.matrixGNSVector_inner line 133
theorem OAI.KadisonSimilarity.matrixGNSVector_norm line 150

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_faithful line 158

Source documentation

Faithfulness of the trace is preserved by normalized matrix extension.

theorem normalizedMatrixTrace_faithful (τ : A →ₚ[ℂ] ℂ)
    (hf : ∀ a : A, τ (star a * a) = 0 → a = 0)
    (X : CStarMatrix (Fin n) (Fin n) A)
    (hX : normalizedMatrixTrace τ n (star X * X) = 0) : X = 0 := by
…

Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_single line 175

Source documentation

The normalized trace of one diagonal entry has weight 1/n.

theorem normalizedMatrixTrace_single (τ : A →ₚ[ℂ] ℂ) (i : Fin n) (a : A) :
    normalizedMatrixTrace τ n (CStarMatrix.ofMatrix (Matrix.single i i a)) =
      τ a / (n : ℂ) := by
…

Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_matrixUnit line 180
def OAI.KadisonSimilarity.matrixGNSIsometry line 186
Source documentation
The completed matrix GNS space embeds isometrically in its entry array.
```
def matrixGNSIsometry (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    (normalizedMatrixTrace τ n).GNS →ₗᵢ[ℂ] MatrixGNSArray τ n :=
…
```
Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.MatrixGNSArray
theorem OAI.KadisonSimilarity.matrixGNSIsometry_vector line 191
theorem OAI.KadisonSimilarity.matrixGNSArrayLinear_dense line 198
theorem OAI.KadisonSimilarity.matrixGNSVector_dense line 208
theorem OAI.KadisonSimilarity.matrixGNSIsometry_surjective line 218
def OAI.KadisonSimilarity.matrixGNSUnitary line 230
Source documentation
The completed normalized matrix GNS space is exactly the square Hilbert array.
```
def matrixGNSUnitary (τ : A →ₚ[ℂ] ℂ) (n : ℕ) [NeZero n] :
    (normalizedMatrixTrace τ n).GNS ≃ₗᵢ[ℂ] MatrixGNSArray τ n :=
…
```
Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.MatrixGNSArray
theorem OAI.KadisonSimilarity.matrixGNSUnitary_vector line 234
def OAI.KadisonSimilarity.matrixLeftArray line 243
Source documentation
The ordinary matrix action on the row coordinate, with a standard copy in each column coordinate.
```
def matrixLeftArray (τ : A →ₚ[ℂ] ℂ) (X : CStarMatrix (Fin n) (Fin n) A) :
    MatrixGNSArray τ n →L[ℂ] MatrixGNSArray τ n :=
…
```
Mentions: OAI.KadisonSimilarity.MatrixGNSArray
theorem OAI.KadisonSimilarity.matrixLeftArray_apply line 248
theorem OAI.KadisonSimilarity.matrixGNSVector_mul line 253
theorem OAI.KadisonSimilarity.matrixGNSUnitary_left line 262
Source documentation
The GNS left representation becomes actual left matrix multiplication under the normalized array identification.
```
theorem matrixGNSUnitary_left (τ : A →ₚ[ℂ] ℂ)
    (X : CStarMatrix (Fin n) (Fin n) A) (ξ : (normalizedMatrixTrace τ n).GNS) :
    matrixGNSUnitary τ n ((normalizedMatrixTrace τ n).gnsStarAlgHom X ξ) =
      matrixLeftArray τ X (matrixGNSUnitary τ n ξ) := by
…
```
Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.matrixGNSUnitary, OAI.KadisonSimilarity.matrixLeftArray

theorem OAI.KadisonSimilarity.matrixGNSUnitary_conjugates_left line 279

Source documentation

Conjugation by the normalized array unitary gives actual left matrix action.

theorem matrixGNSUnitary_conjugates_left (τ : A →ₚ[ℂ] ℂ)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    (matrixGNSUnitary τ n).toContinuousLinearEquiv.toContinuousLinearMap.comp
      (((normalizedMatrixTrace τ n).gnsStarAlgHom X).comp
        (matrixGNSUnitary τ n).symm.toContinuousLinearEquiv.toContinuousLinearMap) =
      matrixLeftArray τ X := by
…

Mentions: OAI.KadisonSimilarity.matrixGNSUnitary, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.matrixLeftArray