MatrixGNSRecovery.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact recovery of finite matrix commutators from the normalized matrix GNS space. The surjective linear isometry transports the represented operators and preserves their commutator norms.

theorem OAI.KadisonSimilarity.matrixLeftArray_eq_representedMatrix line 21
Source documentation
The matrix left action is the represented matrix for the actual amplified scalar GNS representation.
```
theorem matrixLeftArray_eq_representedMatrix (τ : A →ₚ[ℂ] ℂ)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    matrixLeftArray τ X =
      representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom n) X := rfl
```
Mentions: OAI.KadisonSimilarity.matrixLeftArray, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation
theorem OAI.KadisonSimilarity.norm_matrixGNSLiftOperator_commutator line 28
Source documentation
The normalized matrix GNS identification preserves the full commutator norm, rather than only one inequality.
```
theorem norm_matrixGNSLiftOperator_commutator (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    ‖commutator (matrixGNSLiftOperator τ Y)
      ((normalizedMatrixTrace τ n).gnsStarAlgHom X)‖ =
      ‖commutator (amplify Y n) (matrixLeftArray τ X)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixLeftArray
theorem OAI.KadisonSimilarity.norm_matrixGNSLiftOperator_commutator_represented line 53
Source documentation
The same equality in the notation used by finite amplification.
```
theorem norm_matrixGNSLiftOperator_commutator_represented (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    ‖commutator (matrixGNSLiftOperator τ Y)
      ((normalizedMatrixTrace τ n).gnsStarAlgHom X)‖ =
      ‖commutator (amplify Y n)
        (representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom n) X)‖ :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation

theorem OAI.KadisonSimilarity.matrixGNS_centered_symmetry_bound_transfer line 64

Source documentation

A centered-symmetry estimate on the actual matrix GNS space transfers with precisely the same constant to the square Hilbert array.

theorem matrixGNS_centered_symmetry_bound_transfer (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n) {B : ℝ}
    (hbound : ∀ S : CStarMatrix (Fin n) (Fin n) A,
      star S = S → S * S = 1 → normalizedMatrixTrace τ n S = 0 →
      ‖commutator (matrixGNSLiftOperator τ Y)
        ((normalizedMatrixTrace τ n).gnsStarAlgHom S)‖ ≤ B)
    (S : CStarMatrix (Fin n) (Fin n) A)
    (hstar : star S = S) (hsq : S * S = 1) (htrace : normalizedMatrixTrace τ n S = 0) :
    ‖commutator (amplify Y n)
      (representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom n) S)‖ ≤ B := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation

theorem OAI.KadisonSimilarity.finite_amplification_bound_of_matrixGNS_symmetry line 79

Source documentation

A bound on the single actual dilated symmetry in normalized matrix GNS recovers the original finite matrix test after the multiplicity replacement.

theorem finite_amplification_bound_of_matrixGNS_symmetry {r h : ℕ}
    (τ : A →ₚ[ℂ] ℂ) (e : Fin r ↪ Fin (4 * n)) (f : Fin h ↪ Fin n)
    (Y : HilbertCopies τ.GNS r →L[ℂ] HilbertCopies τ.GNS r)
    (X : CStarMatrix (Fin h) (Fin h) A) (hX : ‖X‖ ≤ 1)
    (Y₀ : HilbertCopies τ.GNS (4 * n) →L[ℂ] HilbertCopies τ.GNS (4 * n))
    {η B : ℝ} (hclose : ‖Y₀ - padArrayOperator e Y‖ ≤ η)
    (hbound : ‖commutator (matrixGNSLiftOperator τ Y₀)
      ((normalizedMatrixTrace τ (4 * n)).gnsStarAlgHom
        (fourfoldMatrixFlatten n (contractionSymmetryUnitary (cstarMatrixPadding f X)
          (by simpa only [norm_cstarMatrixPadding] using hX))))‖ ≤ B) :
    ‖commutator (amplify Y h)
      (representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom r) X)‖ ≤
…

theorem OAI.KadisonSimilarity.finite_amplification_bound_of_matrixGNS_centered_tests line 99

Source documentation

Only selfadjoint square-one centered elements are needed on the matrix GNS side; all other tests are supplied by the concrete dilation.

theorem finite_amplification_bound_of_matrixGNS_centered_tests {r h : ℕ}
    (τ : A →ₚ[ℂ] ℂ) (e : Fin r ↪ Fin (4 * n)) (f : Fin h ↪ Fin n)
    (Y : HilbertCopies τ.GNS r →L[ℂ] HilbertCopies τ.GNS r)
    (X : CStarMatrix (Fin h) (Fin h) A) (hX : ‖X‖ ≤ 1)
    (Y₀ : HilbertCopies τ.GNS (4 * n) →L[ℂ] HilbertCopies τ.GNS (4 * n))
    {η B : ℝ} (hclose : ‖Y₀ - padArrayOperator e Y‖ ≤ η)
    (hbound : ∀ S : CStarMatrix (Fin (4 * n)) (Fin (4 * n)) A,
      star S = S → S * S = 1 → normalizedMatrixTrace τ (4 * n) S = 0 →
      ‖commutator (matrixGNSLiftOperator τ Y₀)
        ((normalizedMatrixTrace τ (4 * n)).gnsStarAlgHom S)‖ ≤ B) :
    ‖commutator (amplify Y h)
      (representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom r) X)‖ ≤
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation

theorem OAI.KadisonSimilarity.finite_standard_bound_of_matrixGNS_replacements line 121

Source documentation

Uniform replacements on square matrix GNS spaces control every finite standard multiplicity and every matrix size. Normalization of arbitrary tests, dimension padding, and the two approximation errors are all handled by the proved dilation reduction.

theorem finite_standard_bound_of_matrixGNS_replacements {r : ℕ}
    (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS r →L[ℂ] HilbertCopies τ.GNS r) {η B : ℝ}
    (hconstant : 0 ≤ B + 2 * η)
    (hreplace : ∀ (m : ℕ) [NeZero m], ∀ e : Fin r ↪ Fin (4 * m),
      ∃ Y₀ : HilbertCopies τ.GNS (4 * m) →L[ℂ] HilbertCopies τ.GNS (4 * m),
        ‖Y₀ - padArrayOperator e Y‖ ≤ η ∧
        ∀ S : CStarMatrix (Fin (4 * m)) (Fin (4 * m)) A,
          star S = S → S * S = 1 → normalizedMatrixTrace τ (4 * m) S = 0 →
          ‖commutator (matrixGNSLiftOperator τ Y₀)
            ((normalizedMatrixTrace τ (4 * m)).gnsStarAlgHom S)‖ ≤ B)
    (h : ℕ) (X : CStarMatrix (Fin h) (Fin h) A) :
…