CuntzNuclearity.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.CuntzAveraging.defect_polynomial_tendsto line 21
Source documentation
The finite-level intertwining estimate extends to every star polynomial, with no continuity assumption on a presentation of that polynomial.
```
theorem defect_polynomial_tendsto (p : CuntzPolynomial.Poly) :
    Tendsto (fun n => defect R n (inclusion p)) atTop (𝓝 0) := by
…
```
Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly, OAI.NuclearUltrapower.CuntzAveraging.defect
theorem OAI.NuclearUltrapower.CuntzAveraging.defect_tendsto line 50
Source documentation
Uniform contractivity of the averages extends polynomial intertwining to the norm completion, rather than just its algebraic dense subalgebra.
```
theorem defect_tendsto (a : Algebra) :
    Tendsto (fun n => defect R n a) atTop (𝓝 0) := by
…
```
Mentions: OAI.NuclearUltrapower.CuntzAveraging.defect
def OAI.NuclearUltrapower.CuntzAveraging.completedEval line 78
Source documentation
The concrete spatial representation on the completed Hilbert tensor product.
```
def completedEval : Algebra ⊗[ℂ] C →ₗ[ℂ] (Target H →L[ℂ] Target H) :=
…
```
Mentions: OAI.NuclearUltrapower.CuntzAveraging.Target
theorem OAI.NuclearUltrapower.CuntzAveraging.completedEval_tmul line 83
theorem OAI.NuclearUltrapower.CuntzAveraging.completedEval_norm_le line 86
def OAI.NuclearUltrapower.CuntzAveraging.jointDefect line 97
theorem OAI.NuclearUltrapower.CuntzAveraging.jointDefect_zero line 100
theorem OAI.NuclearUltrapower.CuntzAveraging.jointDefect_add line 105
theorem OAI.NuclearUltrapower.CuntzAveraging.jointDefect_tmul line 112
theorem OAI.NuclearUltrapower.CuntzAveraging.jointDefect_tendsto line 124
Source documentation
Norm convergence of the averaged intertwining errors for every algebraic tensor; the second algebra is completely arbitrary and may be nonunital.
```
theorem jointDefect_tendsto (hRS : ∀ a c, Commute (R a) (S c)) (x : Algebra ⊗[ℂ] C) :
    Tendsto (fun n => jointDefect H R S n x) atTop (𝓝 0) := by
…
```
Mentions: OAI.NuclearUltrapower.CuntzAveraging.jointDefect
theorem OAI.NuclearUltrapower.CuntzAveraging.commutingEval_support line 134
Source documentation
The output of any commuting tensor evaluation lies in the support of R.
```
theorem commutingEval_support (x : Algebra ⊗[ℂ] C) :
    R 1 * commutingEval H R S x = commutingEval H R S x := by
…
```
Mentions: OAI.NuclearUltrapower.commutingEval
theorem OAI.NuclearUltrapower.CuntzAveraging.commutingEval_norm_le_min line 147
Source documentation
Averaging proves the nontrivial maximal-to-minimal inequality directly; no faithfulness, separability or nondegeneracy of the input representations is assumed.
```
theorem commutingEval_norm_le_min (hRS : ∀ a c, Commute (R a) (S c)) (x : Algebra ⊗[ℂ] C) :
    ‖commutingEval H R S x‖ ≤ minTensorNorm.{0,0,0} x := by
…
```
Mentions: OAI.NuclearUltrapower.commutingEval
theorem OAI.NuclearUltrapower.CuntzUniversal.nuclear line 175
Source documentation
The actually constructed universal Cuntz algebra is nuclear in the full spatial/commuting tensor-norm sense used in the obstruction theorem.
```
theorem CuntzUniversal.nuclear : IsNuclear.{0,0} CuntzUniversal.Algebra := by
…
```
Mentions: OAI.NuclearUltrapower.CuntzUniversal.Algebra