MatrixArrayFlattening.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Flattening nested matrix and Hilbert-array coordinates

theorem OAI.KadisonSimilarity.sum_fin_prod line 14
theorem OAI.KadisonSimilarity.sum_cstarMatrix_apply line 26

def OAI.KadisonSimilarity.blockMatrixProductEquiv line 37

Source documentation

First flatten block matrices to a product index.

def blockMatrixProductEquiv (p q : ℕ) :
    CStarMatrix (Fin p) (Fin p) (CStarMatrix (Fin q) (Fin q) A) ≃⋆ₐ[ℂ]
      CStarMatrix (Fin p × Fin q) (Fin p × Fin q) A where
…

theorem OAI.KadisonSimilarity.blockMatrixProductEquiv_apply line 57

def OAI.KadisonSimilarity.blockMatrixFlatten line 63

Source documentation

Flatten square blocks using the standard product enumeration.

def blockMatrixFlatten (p q : ℕ) :
    CStarMatrix (Fin p) (Fin p) (CStarMatrix (Fin q) (Fin q) A) ≃⋆ₐ[ℂ]
      CStarMatrix (Fin (p * q)) (Fin (p * q)) A :=
…

theorem OAI.KadisonSimilarity.blockMatrixFlatten_apply line 68
theorem OAI.KadisonSimilarity.norm_blockMatrixFlatten line 80
def OAI.KadisonSimilarity.entrywiseCStarMatrixEquiv line 94
Source documentation
An equivalence of coefficient algebras induces the entrywise matrix equivalence.
```
def entrywiseCStarMatrixEquiv (n : ℕ) (e : B ≃⋆ₐ[ℂ] C) :
    CStarMatrix (Fin n) (Fin n) B ≃⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) C where
…
```
theorem OAI.KadisonSimilarity.entrywiseCStarMatrixEquiv_apply line 111

def OAI.KadisonSimilarity.tripleMatrixFlatten line 122

Source documentation

Flatten three matrix indices, retaining the outer-to-inner order.

def tripleMatrixFlatten (p q t : ℕ) :
    CStarMatrix (Fin p) (Fin p)
      (CStarMatrix (Fin q) (Fin q) (CStarMatrix (Fin t) (Fin t) A)) ≃⋆ₐ[ℂ]
    CStarMatrix (Fin (p * (q * t))) (Fin (p * (q * t))) A :=
…

theorem OAI.KadisonSimilarity.tripleMatrixFlatten_apply line 129

def OAI.KadisonSimilarity.fourfoldMatrixFlatten line 139

Source documentation

The four-by-four dilation's flattened matrix has size 4 * n.

def fourfoldMatrixFlatten (n : ℕ) :
    CStarMatrix (Fin 2) (Fin 2)
      (CStarMatrix (Fin 2) (Fin 2) (CStarMatrix (Fin n) (Fin n) A)) ≃⋆ₐ[ℂ]
    CStarMatrix (Fin (4 * n)) (Fin (4 * n)) A :=
…

def OAI.KadisonSimilarity.fourfoldIndexEquiv line 147
Source documentation
The common enumeration of the three finite indices.
```
def fourfoldIndexEquiv (n : ℕ) : (Fin 2 × (Fin 2 × Fin n)) ≃ Fin (4 * n) :=
…
```
theorem OAI.KadisonSimilarity.sum_fourfold line 151
theorem OAI.KadisonSimilarity.fourfoldMatrixFlatten_apply line 159

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_blockMatrixFlatten line 181

Source documentation

Normalized diagonal traces agree under block flattening.

theorem normalizedMatrixTrace_blockMatrixFlatten (p q : ℕ) [NeZero p] [NeZero q]
    (τ : A →ₚ[ℂ] ℂ)
    (X : CStarMatrix (Fin p) (Fin p) (CStarMatrix (Fin q) (Fin q) A)) :
    normalizedMatrixTrace (normalizedMatrixTrace τ q) p X =
      normalizedMatrixTrace τ (p * q) (blockMatrixFlatten p q X) := by
…

Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.blockMatrixFlatten

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_tripleMatrixFlatten line 194
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_reindex line 210

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_fourfoldMatrixFlatten line 226

Source documentation

The normalized trace is unchanged by the complete fourfold flattening.

theorem normalizedMatrixTrace_fourfoldMatrixFlatten (n : ℕ) [NeZero n]
    (τ : A →ₚ[ℂ] ℂ)
    (X : CStarMatrix (Fin 2) (Fin 2)
      (CStarMatrix (Fin 2) (Fin 2) (CStarMatrix (Fin n) (Fin n) A))) :
    normalizedMatrixTrace τ (4 * n) (fourfoldMatrixFlatten n X) =
      normalizedMatrixTrace (normalizedMatrixTrace (normalizedMatrixTrace τ n) 2) 2 X := by
…

Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.fourfoldMatrixFlatten

theorem OAI.KadisonSimilarity.normalizedMatrixTrace_two_eq_linearMatrixTrace line 235
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_flattened_contractionSymmetry line 244
Source documentation
The actual flattened four-by-four contraction symmetry is centered for the normalized trace on the ordinary matrix algebra.
```
theorem normalizedMatrixTrace_flattened_contractionSymmetry (n : ℕ) [NeZero n]
    (τ : A →ₚ[ℂ] ℂ) (X : CStarMatrix (Fin n) (Fin n) A) (hX : ‖X‖ ≤ 1) :
    normalizedMatrixTrace τ (4 * n)
      (fourfoldMatrixFlatten n (contractionSymmetryUnitary X hX)) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary
def OAI.KadisonSimilarity.hilbertArrayFlatten line 263
Source documentation
Flatten two finite Hilbert sums in the same order as block matrices.
```
def hilbertArrayFlatten (p q : ℕ) :
    HilbertCopies (HilbertCopies H q) p ≃ₗᵢ[ℂ] HilbertCopies H (p * q) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.hilbertArrayFlatten_apply line 269
theorem OAI.KadisonSimilarity.hilbertArrayFlatten_amplify line 279
Source documentation
Repeated diagonal amplification is unchanged by flattening.
```
theorem hilbertArrayFlatten_amplify (p q : ℕ) (Y : H →L[ℂ] H)
    (x : HilbertCopies (HilbertCopies H q) p) :
    hilbertArrayFlatten p q (amplify (amplify Y q) p x) =
      amplify Y (p * q) (hilbertArrayFlatten p q x) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.hilbertArrayFlatten, OAI.KadisonSimilarity.amplify
def OAI.KadisonSimilarity.hilbertTripleFlatten line 288
Source documentation
Three nested finite Hilbert sums, in the same order as triple block matrices.
```
def hilbertTripleFlatten (p q t : ℕ) :
    HilbertCopies (HilbertCopies (HilbertCopies H t) q) p ≃ₗᵢ[ℂ]
      HilbertCopies H (p * (q * t)) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.hilbertTripleFlatten_apply line 295
def OAI.KadisonSimilarity.hilbertFourfoldFlatten line 303
Source documentation
The Hilbert-space change of coordinates for the four-by-four dilation.
```
def hilbertFourfoldFlatten (n : ℕ) :
    HilbertCopies (HilbertCopies (HilbertCopies H n) 2) 2 ≃ₗᵢ[ℂ]
      HilbertCopies H (4 * n) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.hilbertFourfoldFlatten_apply line 310
theorem OAI.KadisonSimilarity.hilbertFourfoldFlatten_amplify line 317
theorem OAI.KadisonSimilarity.hilbertArrayFlatten_represented line 334
Source documentation
Nested block multiplication and flattened matrix multiplication act identically in the corresponding Hilbert coordinates.
```
theorem hilbertArrayFlatten_represented (p q : ℕ)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (X : CStarMatrix (Fin p) (Fin p) (CStarMatrix (Fin q) (Fin q) A))
    (x : HilbertCopies (HilbertCopies H q) p) :
    hilbertArrayFlatten p q
      (matrixOperator (fun i j => representedMatrix σ (X i j)) x) =
    representedMatrix σ (blockMatrixFlatten p q X) (hilbertArrayFlatten p q x) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.hilbertArrayFlatten, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.blockMatrixFlatten
theorem OAI.KadisonSimilarity.representedDoubleMatrix_nested_apply line 362
theorem OAI.KadisonSimilarity.hilbertFourfoldFlatten_representedDoubleMatrix line 380
Source documentation
The nested action used by the dilation is precisely the ordinary flattened matrix action under the explicit Hilbert-array isometry.
```
theorem hilbertFourfoldFlatten_representedDoubleMatrix (n : ℕ)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (X : HochschildMatrixDilation.Mat
      (HochschildMatrixDilation.Mat (CStarMatrix (Fin n) (Fin n) A)))
    (x : HilbertCopies (HilbertCopies (HilbertCopies H n) 2) 2) :
    hilbertFourfoldFlatten n (representedDoubleMatrix (representedMatrixHom σ n) X x) =
      representedMatrix σ (fourfoldMatrixFlatten n X) (hilbertFourfoldFlatten n x) := by
…
```
Mentions: OAI.HochschildMatrixDilation.Mat, OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.hilbertFourfoldFlatten, OAI.KadisonSimilarity.representedDoubleMatrix, OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.fourfoldMatrixFlatten
theorem OAI.KadisonSimilarity.hilbertFourfoldFlatten_commutator line 402

theorem OAI.KadisonSimilarity.norm_fourfold_commutator line 416

Source documentation

The commutator norm is exactly preserved by the change of array coordinates.

theorem norm_fourfold_commutator (n : ℕ)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Y : H →L[ℂ] H)
    (X : HochschildMatrixDilation.Mat
      (HochschildMatrixDilation.Mat (CStarMatrix (Fin n) (Fin n) A))) :
    ‖commutator (amplify Y (4 * n)) (representedMatrix σ (fourfoldMatrixFlatten n X))‖ =
      ‖commutator (amplify (amplify (amplify Y n) 2) 2)
        (representedDoubleMatrix (representedMatrixHom σ n) X)‖ := by
…

Mentions: OAI.HochschildMatrixDilation.Mat, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.representedDoubleMatrix, OAI.KadisonSimilarity.representedMatrixHom

theorem OAI.KadisonSimilarity.norm_amplified_commutator_le_flattened_symmetry line 443

Source documentation

The original matrix test is a norm-decreasing corner of the ordinary 4 * n centered symmetry test.

theorem norm_amplified_commutator_le_flattened_symmetry {n : ℕ} [NeZero n]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Y : H →L[ℂ] H)
    (X : CStarMatrix (Fin n) (Fin n) A) (hX : ‖X‖ ≤ 1) :
    ‖commutator (amplify Y n) (representedMatrix σ X)‖ ≤
      ‖commutator (amplify Y (4 * n))
        (representedMatrix σ (fourfoldMatrixFlatten n (contractionSymmetryUnitary X hX)))‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary