ProjectionSequenceLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sequential projection suprema and infima with their actual weak-star limits.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_increasing_projection_limit line 18

Source documentation

An increasing sequence of projections converges weak-star to its supremum.

theorem exists_increasing_projection_limit (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : ℕ → M) (hp : ∀ n, IsStarProjection (p n)) (hm : Monotone p) :
    ∃ s : M, IsStarProjection s ∧ IsLUB (Set.range p) s ∧
      PredualTendsto e p atTop s := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto

theorem OAI.BoundedHochschild.KadisonRingrose.exists_decreasing_projection_limit line 46

Source documentation

A decreasing sequence of projections converges weak-star to its infimum.

theorem exists_decreasing_projection_limit (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : ℕ → M) (hp : ∀ n, IsStarProjection (p n)) (hm : Antitone p) :
    ∃ s : M, IsStarProjection s ∧ IsGLB (Set.range p) s ∧
      PredualTendsto e p atTop s := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto