OAI/Analysis/OperatorAlgebra/ExpectationDensityRoots.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakPureInfiniteness.densityRoot_finite_support line 16
2. theorem OAI.WeakPureInfiniteness.expectation_finite_density_roots line 37

   Source documentation

   A finite tracial expectation supplies positive finite-rank density roots of norm at most one, approximately invariant under the prescribed unitaries.

   theorem expectation_finite_density_roots (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 < ε) :
       ∃ (n : ℕ) (w : Fin n → ℝ) (x : Fin n → H),
         (∀ k, 0 ≤ w k) ∧ (∑ k, w k = 1) ∧ (∀ k, ‖x k‖ ≤ 1) ∧
         (∀ i, |(τ.functional (a i)).re -
           ∑ k, w k * (inner ℂ (x k) (((a i : M.toStarSubalgebra) : H →L[ℂ] H) (x k))).re| < ε) ∧
   …

   Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive