OAI/Analysis/OperatorAlgebra/ExpectationFiniteDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The constructed conditional expectation supplies the finite hypertrace witness. All conjugations below are the actual unitaries of the represented algebra, and the errors are measured in the norm of vector functionals.

  1. def OAI.WeakPureInfiniteness.subalgebraUnitaryIsometry line 17
  2. lemma OAI.WeakPureInfiniteness.conjugatedOperator_subalgebraUnitary line 20
  3. lemma OAI.WeakPureInfiniteness.hypertrace_subalgebraUnitary_invariant line 27
  4. theorem OAI.WeakPureInfiniteness.expectation_finite_density line 45

    Source documentation

    Finite normal positive approximations with norm-small unitary defects, obtained from the actual expectation and a tracial state.

    theorem expectation_finite_density (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