OAI/Analysis/BoundedHochschild/ProjectionPositivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity detected on projections

The spectral approximation step in Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemma 3.5. Dyadic spectral projections suffice.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.positive_contraction_eval_nonneg_of_projection_nonneg line 26
  2. theorem OAI.BoundedHochschild.KadisonRingrose.eval_nonneg_of_projection_nonneg line 61

    Source documentation

    A bounded hermitian functional nonnegative on projections is positive.

    theorem eval_nonneg_of_projection_nonneg (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (F : StrongDual ℂ M) (hreal : ∀ a : M, IsSelfAdjoint a → (F a).im = 0)
    (hproj : ∀ p : M, IsStarProjection p → 0 ≤ F p) :
    ∀ a : M, 0 ≤ a → 0 ≤ F a := by
…