SpatialMatrixGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial-product gap from matrix unit-ball approximation

The hypothesis is complete matrix proximity. Ordinary proximity is not asserted to remain unchanged under amplification.

theorem OAI.KadisonKastler.spatialMatrix_test_approx line 24

theorem OAI.KadisonKastler.MatrixNearInclusion.spatialProduct_approx line 45

Source documentation

Complete one-sided approximation extends to the spatial product with an increasing matrix-generated von Neumann algebra.

theorem MatrixNearInclusion.spatialProduct_approx
    (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))
    (a : SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (ha : a ∈ unitBall (spatialProductAlgebra M
      (generatedVonNeumannAlgebra (⨆ n, (E n).algebra)))) :
    ∃ b ∈ unitBall (spatialProductAlgebra N
        (generatedVonNeumannAlgebra (⨆ n, (E n).algebra))), ‖a - b‖ ≤ γ := by
…

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

theorem OAI.KadisonKastler.kkDistance_spatialProduct_le_of_matrixNearInclusion line 61

Source documentation

Two-sided complete matrix proximity controls the ordinary gap of the actual spatial products, with no loss in the constant.

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

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