OAI/Analysis/KadisonKastler/SpatialMatrixAmplification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix amplification of spatial matrix images

Finite matrices over a generated operator algebra generate the matrix von Neumann algebra. The proof uses the existing strong approximation theorem entry by entry. Flattening the two finite matrix indices then preserves the complete unit-ball approximation constant.

  1. def OAI.KadisonKastler.spatialMatrixAmplification line 42

    Source documentation

    Entrywise amplification of the finite spatial matrix representation.

    def spatialMatrixAmplification (E : MatrixUnitSystem κ (K →L[ℂ] K)) :
    CStarMatrix ι ι (CStarMatrix κ κ (H →L[ℂ] H)) →⋆ₐ[ℂ]
      CStarMatrix ι ι (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) :=
…
  2. theorem OAI.KadisonKastler.spatialMatrixAmplification_apply line 49
  3. theorem OAI.KadisonKastler.spatialMatrixAmplification_injective line 53
  4. theorem OAI.KadisonKastler.norm_spatialMatrixAmplification line 62
  5. theorem OAI.KadisonKastler.MatrixNearInclusion.spatialMatrixAmplification_approx line 71

    Source documentation

    Flattening lets the original complete approximation hypothesis control every finite amplification of a spatial matrix image.

    theorem MatrixNearInclusion.spatialMatrixAmplification_approx
    {M N : VonNeumannAlgebra H} {γ : ℝ} (h : MatrixNearInclusion M N γ)
    [Nonempty κ] [Nontrivial K] (E : MatrixUnitSystem κ (K →L[ℂ] K))
    (X : CStarMatrix ι ι (CStarMatrix κ κ (H →L[ℂ] H)))
    (hX : ∀ i j a b, X i j a b ∈ M) (hn : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix ι ι (CStarMatrix κ κ (H →L[ℂ] H)),
      (∀ i j a b, Y i j a b ∈ N) ∧ ‖Y‖ ≤ 1 ∧
      ‖spatialMatrixAmplification E X - spatialMatrixAmplification E Y‖ ≤ γ := by
…

    Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.spatialMatrixAmplification