RegularTensorGap.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Complete matrix bounds control the regular tensor gap

The scalar Hilbert coordinates identify the actual regular tensor algebra with the canonical countable amplification. Uniform finite-matrix approximation, or actual common countable matrix units, therefore bounds its gap. No ordinary-gap amplification principle is assumed.

theorem OAI.KadisonKastler.spatialTransportAlgebra_commutant line 25
theorem OAI.KadisonKastler.mem_canonicalAmplifiedAlgebra_iff line 35
theorem OAI.KadisonKastler.spatialTransport_regularTensorAlgebra line 54
Source documentation
The actual regular tensor algebra in scalar Hilbert coordinates.
```
theorem spatialTransport_regularTensorAlgebra (M : VonNeumannAlgebra H) :
    spatialTransportAlgebra (regularHilbertCoordinates (H := H) regularScalarBasis)
…
```
Mentions: OAI.KadisonKastler.spatialTransportAlgebra, OAI.KadisonKastler.regularHilbertCoordinates, OAI.KadisonKastler.regularScalarBasis
theorem OAI.KadisonKastler.kkDistance_regularTensorAlgebra line 84
Source documentation
The regular tensor gap is exactly the canonical amplification gap.
```
theorem kkDistance_regularTensorAlgebra (M N : VonNeumannAlgebra H) :
    kkDistance (regularTensorAlgebra M) (regularTensorAlgebra N) =
      kkDistance (canonicalAmplifiedAlgebra H M) (canonicalAmplifiedAlgebra H N) := by
…
```
Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.canonicalAmplifiedAlgebra

theorem OAI.KadisonKastler.matrixApprox_spatialTransport line 99

Source documentation

Finite-matrix approximation transports across an actual Hilbert isometry.

theorem matrixApprox_spatialTransport (e : H ≃ₗᵢ[ℂ] K)
    (M N : VonNeumannAlgebra H) {r : ℝ}
    (hnear : ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)),
      (∀ i j, X i j ∈ M) → ‖X‖ ≤ 1 →
      ∃ Y : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H),
        (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ r)
    (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (K →L[ℂ] K))
    (hX : ∀ i j, X i j ∈ spatialTransportAlgebra e M) (hn : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix (Fin n) (Fin n) (K →L[ℂ] K),
      (∀ i j, Y i j ∈ spatialTransportAlgebra e N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ r := by
…

Mentions: OAI.KadisonKastler.spatialTransportAlgebra

theorem OAI.KadisonKastler.kkDistance_regularTensorAlgebra_le_of_matrix_approx line 131

Source documentation

Two-sided complete matrix approximation controls the regular tensor gap.

theorem kkDistance_regularTensorAlgebra_le_of_matrix_approx
    (M N : VonNeumannAlgebra H) {r : ℝ} (hr : 0 ≤ r)
    (hMN : ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)),
      (∀ i j, X i j ∈ M) → ‖X‖ ≤ 1 →
      ∃ Y : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H),
        (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ r)
    (hNM : ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)),
      (∀ i j, X i j ∈ N) → ‖X‖ ≤ 1 →
      ∃ Y : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H),
        (∀ i j, Y i j ∈ M) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ r) :
    kkDistance (regularTensorAlgebra M) (regularTensorAlgebra N) ≤ r := by
…

Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularTensorAlgebra

theorem OAI.KadisonKastler.kkDistance_regularTensorAlgebra_le_of_common_matrix_units line 156

Source documentation

Actual common matrix units are sufficient for the tensor gap bound.

theorem kkDistance_regularTensorAlgebra_le_of_common_matrix_units
    (M N : VonNeumannAlgebra H) (D : Submodule ℂ H) [CompleteSpace D]
    (F : FullMatrixCorner D) (hM : ∀ i j, F.entry i j ∈ M)
    (hN : ∀ i j, F.entry i j ∈ N) :
    kkDistance (regularTensorAlgebra M) (regularTensorAlgebra N) ≤ kkDistance M N := by
…

Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularTensorAlgebra