NuclearApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Completely positive approximation in a weak closure

The norm finite-test completely positive approximation property yields simultaneous strong-star approximation on finitely many vectors. The factor maps pass through a finite-dimensional matrix algebra.

def OAI.TraceConeClassification.NuclearCPAP line 27
Source documentation
The completely positive approximation property, in norm finite-test form.
```
def NuclearCPAP : Prop :=
…
```
def OAI.TraceConeClassification.IsHyperfiniteWOT line 38
Source documentation
Hyperfiniteness witnessed by an increasing sequence of finite-dimensional star subalgebras with weak-operator dense union.
```
def IsHyperfiniteWOT (N : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) : Prop :=
…
```

theorem OAI.TraceConeClassification.NuclearCPAP.weakClosure_cp_approx line 55

Source documentation

Nuclear CPAP gives simultaneous strong-star approximation on finite sets of operators and vectors in the weak closure of a representation.

theorem NuclearCPAP.weakClosure_cp_approx (hNuc : NuclearCPAP A)
    (π : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (m k : ℕ)
    (T : Fin m → H →L[ℂ] H)
    (hT : ∀ j, T j ∈ weakClosure (NonUnitalStarAlgHom.range π))
    (ξ : Fin k → H) (ε : ℝ) (hε : 0 < ε) :
    ∃ (n : ℕ) (α : A →CP CStarMatrix (Fin n) (Fin n) ℂ)
      (β : CStarMatrix (Fin n) (Fin n) ℂ →CP A) (a : Fin m → A),
      (∀ x, ‖α x‖ ≤ ‖x‖) ∧ (∀ y, ‖β y‖ ≤ ‖y‖) ∧
      ∀ j i, ‖π (β (α (a j))) (ξ i) - T j (ξ i)‖ < ε ∧
        ‖star (π (β (α (a j)))) (ξ i) - star (T j) (ξ i)‖ < ε := by
…

Mentions: OAI.TraceConeClassification.NuclearCPAP, OAI.TraceConeClassification.weakClosure