AmplificationGap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing matrix approximants to the infinite amplification

Finite compressions have norm at most one. Weak operator compactness gives a single limiting approximant in the target amplification, retaining the same error at every coefficient and therefore in operator norm.

theorem OAI.KadisonKastler.FullMatrixCorner.exists_amplified_approx_of_matrix_approx line 36

Source documentation

Uniform finite matrix approximation implies approximation in the actual countable amplification, with no loss of constant.

theorem exists_amplified_approx_of_matrix_approx
    (M N : VonNeumannAlgebra E) {r : ℝ} (hr : 0 ≤ r)
    (hnear : ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (E →L[ℂ] E)),
      (∀ i j, X i j ∈ M) → ‖X‖ ≤ 1 →
      ∃ Y : CStarMatrix (Fin n) (Fin n) (E →L[ℂ] E),
        (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ r)
    (T : H →L[ℂ] H) (hT : T ∈ unitBall (F.amplifiedAlgebra M)) :
    ∃ S ∈ unitBall (F.amplifiedAlgebra N), ‖T - S‖ ≤ r := by
…

Mentions: OAI.KadisonKastler.unitBall

theorem OAI.KadisonKastler.FullMatrixCorner.kkDistance_amplifiedAlgebra_le_of_common_matrix_units line 73
Source documentation
Common countable matrix units in the original pair make every matrix approximation available with its original ordinary tolerance.
```
theorem kkDistance_amplifiedAlgebra_le_of_common_matrix_units
    (M N : VonNeumannAlgebra E) (D : Submodule ℂ E) [CompleteSpace D]
    (G : FullMatrixCorner D)
    (hM : ∀ i j, G.entry i j ∈ M) (hN : ∀ i j, G.entry i j ∈ N) :
    kkDistance (F.amplifiedAlgebra M) (F.amplifiedAlgebra N) ≤ kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.kkDistance