OAI/Analysis/OperatorAlgebra/TracialSpatialApproximation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite-rank spatial vectors preserving prescribed trace tests. This is the finite tracial part of the injectivity argument. It does not assert semidiscreteness for an arbitrary von Neumann algebra.

  1. lemma OAI.WeakPureInfiniteness.finiteVectorDensity_root_left line 20
  2. theorem OAI.WeakPureInfiniteness.expectation_normalized_spatial_vectors line 33

    Source documentation

    A trace-preserving finite family and a nearly central finite family are realized by the same positive, finite-rank, unit Hilbert--Schmidt vector.

    theorem expectation_normalized_spatial_vectors (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (a : I → selfAdjoint M.toStarSubalgebra) (u : J → unitary M.toStarSubalgebra)
    {δ : ℝ} (hδ : 0 < δ) (hδhalf : δ ≤ 1 / 2) :
    ∃ z : NuclearUltrapower.HilbertSchmidt H, ‖z‖ = 1 ∧
      0 ≤ NuclearUltrapower.hsOperator z ∧
      (∃ F : Submodule ℂ H, FiniteDimensional ℂ F ∧
        ∀ y, NuclearUltrapower.hsOperator z y ∈ F) ∧
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator

  3. theorem OAI.WeakPureInfiniteness.expectation_spatial_finite_approximation line 112

    Source documentation

    The finite tracial approximation with a single prescribed error tolerance.

    theorem expectation_spatial_finite_approximation (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (a : I → selfAdjoint M.toStarSubalgebra) (u : J → unitary M.toStarSubalgebra)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ z : NuclearUltrapower.HilbertSchmidt H, ‖z‖ = 1 ∧
      0 ≤ NuclearUltrapower.hsOperator z ∧
      (∃ F : Submodule ℂ H, FiniteDimensional ℂ F ∧
        ∀ y, NuclearUltrapower.hsOperator z y ∈ F) ∧
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator

  4. theorem OAI.WeakPureInfiniteness.expectation_spatial_norm_approximation line 157

    Source documentation

    The same finite witness, with the intertwining error measured in norm rather than squared norm. This is the form used for tensor coefficients.

    theorem expectation_spatial_norm_approximation (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (a : I → selfAdjoint M.toStarSubalgebra) (u : J → unitary M.toStarSubalgebra)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ z : NuclearUltrapower.HilbertSchmidt H, ‖z‖ = 1 ∧
      0 ≤ NuclearUltrapower.hsOperator z ∧
      (∃ F : Submodule ℂ H, FiniteDimensional ℂ F ∧
        ∀ y, NuclearUltrapower.hsOperator z y ∈ F) ∧
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator

  5. lemma OAI.WeakPureInfiniteness.tracial_complex_coefficient_error_le line 183
  6. theorem OAI.WeakPureInfiniteness.expectation_complex_spatial_approximation line 198

    Source documentation

    Complex tests require two self-adjoint tests, with the same finite-rank vector serving both and the prescribed unitary family.

    theorem expectation_complex_spatial_approximation (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (a : I → M.toStarSubalgebra) (u : J → unitary M.toStarSubalgebra)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ z : NuclearUltrapower.HilbertSchmidt H, ‖z‖ = 1 ∧
      0 ≤ NuclearUltrapower.hsOperator z ∧
      (∃ F : Submodule ℂ H, FiniteDimensional ℂ F ∧
        ∀ y, NuclearUltrapower.hsOperator z y ∈ F) ∧
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator