ProjectionChainSuprema.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Trace-free suprema of chains of projections in a von Neumann algebra.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_projection_chain_supremum_with_limit line 19

Source documentation

A bounded weak-star limit gives the supremum of a projection chain, including its common annihilators. No trace is needed.

theorem exists_projection_chain_supremum_with_limit
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (S : Set M) (hne : S.Nonempty)
    (hchain : IsChain (· ≤ ·) S) (hproj : ∀ q ∈ S, IsStarProjection q) :
    ∃ p : M, IsStarProjection p ∧ (∀ q ∈ S, q ≤ p) ∧
      (∀ r : M, IsStarProjection r → (∀ q ∈ S, q ≤ r) → p ≤ r) ∧
      (∀ a : M, (∀ q ∈ S, q * a = 0) → p * a = 0) ∧
      ∃ U : Ultrafilter S, (U : Filter S) ≤ atTop ∧
        PredualTendsto e (fun q : S => (q : M)) (U : Filter S) p := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto