SpatialCompleteGap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Complete proximity of spatial products with matrix-generated factors

The finite-stage approximants retain all matrix levels. Kaplansky density and weak compactness extend the same bound to the spatial products. Only the original complete proximity hypothesis is used.

theorem OAI.KadisonKastler.exists_spatialMatrixAmplification_of_mem line 40

Source documentation

A matrix over a finite spatial image has an exact matrix preimage, with the same norm at the outer matrix level.

theorem exists_spatialMatrixAmplification_of_mem
    (M : VonNeumannAlgebra H) (E : MatrixUnitSystem κ (K →L[ℂ] K))
    (T : CStarMatrix ι ι (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
    (hT : ∀ i j, T i j ∈ spatialMatrixAlgebra M E) (hn : ‖T‖ ≤ 1) :
    ∃ X : CStarMatrix ι ι (CStarMatrix κ κ (H →L[ℂ] H)),
      (∀ i j a b, X i j a b ∈ M) ∧ ‖X‖ ≤ 1 ∧ spatialMatrixAmplification E X = T := by
…

Mentions: OAI.KadisonKastler.spatialMatrixAlgebra, OAI.KadisonKastler.spatialMatrixAmplification

theorem OAI.KadisonKastler.generated_matrix_spatial_union line 67
Source documentation
The amplified increasing spatial images generate precisely the matrix von Neumann algebra of the spatial product.
```
theorem generated_matrix_spatial_union
    (M : VonNeumannAlgebra H) (hK : PublishedKaplanskyDensity.{u})
    (hE : Monotone (fun n => (E n).algebra)) :
    generatedVonNeumannAlgebra
        (⨆ n, matrixOperatorAlgebra (ι := ι) (spatialMatrixAlgebra M (E n))) =
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.matrixOperatorAlgebra, OAI.KadisonKastler.spatialMatrixAlgebra
theorem OAI.KadisonKastler.amplified_spatial_test_approx line 79

theorem OAI.KadisonKastler.MatrixNearInclusion.spatialProduct line 139

Source documentation

Matrix unit-ball proximity is preserved by the spatial product with the von Neumann algebra generated by increasing finite matrix stages.

theorem MatrixNearInclusion.spatialProduct
    (hK : PublishedKaplanskyDensity.{u})
    {M N : VonNeumannAlgebra H} {γ : ℝ} (hγ : 0 ≤ γ)
    (h : MatrixNearInclusion M N γ)
    (hs : ∀ n, 0 < s n) (hE : Monotone (fun n => (E n).algebra)) :
    MatrixNearInclusion
      (spatialProductAlgebra M (generatedVonNeumannAlgebra (⨆ n, (E n).algebra)))
      (spatialProductAlgebra N (generatedVonNeumannAlgebra (⨆ n, (E n).algebra))) γ := by
…

Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.generatedVonNeumannAlgebra