MonotoneProjectionLimits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strong limits of increasing projections agree with their algebraic least upper bound. This permits transport between faithful normal models without assuming continuity of the intervening star isomorphism.

theorem OAI.KadisonSimilarity.rangeSupport_of_isStarProjection line 17

theorem OAI.KadisonSimilarity.exists_monotone_projection_limit line 28

Source documentation

A monotone sequence of projections has a strong limit which is its least upper bound inside the concrete von Neumann algebra.

theorem exists_monotone_projection_limit (M : VonNeumannAlgebra H)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (hmono : ∀ i j, i ≤ j → p j * p i = p i) :
    ∃ q : M.toStarSubalgebra, IsStarProjection q ∧
      (∀ x : H, Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 ((q : H →L[ℂ] H) x))) ∧
      (∀ n, q * p n = p n) ∧
      ∀ r : M.toStarSubalgebra, IsStarProjection r → (∀ n, r * p n = p n) → r * q = q := by
…

theorem OAI.KadisonSimilarity.exists_antitone_projection_limit line 88

Source documentation

Decreasing projections have a strong limit below every member.

theorem exists_antitone_projection_limit (M : VonNeumannAlgebra H)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (hanti : ∀ i j, i ≤ j → p i * p j = p j) :
    ∃ q : M.toStarSubalgebra, IsStarProjection q ∧
      (∀ x : H, Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 ((q : H →L[ℂ] H) x))) ∧
      ∀ n, p n * q = q := by
…