OAI/Analysis/BoundedHochschild/OrthogonalProjectionTails.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak-star null tails of a sequence of orthogonal projections.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_orthogonal_projection_tails line 21

    Source documentation

    The tails of an orthogonal projection sum are projections converging weak-star to zero, and each tail dominates all of its summands.

    theorem exists_orthogonal_projection_tails (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (q : ℕ → M) (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0) :
    ∃ T : ℕ → M, (∀ n, IsStarProjection (T n)) ∧ Antitone T ∧
      (∀ n i, n ≤ i → q i ≤ T n) ∧ PredualTendsto e T atTop 0 := by
…

    Mentions: OAI.BoundedHochschild.PredualTendsto