OrthogonalProjectionSums.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary orthogonal projection sums and their weak-star convergence.

lemma OAI.BoundedHochschild.KadisonRingrose.orthogonal_projection_finset_sum line 22

theorem OAI.BoundedHochschild.KadisonRingrose.exists_orthogonal_projection_sum line 39

Source documentation

The net of finite partial sums of any orthogonal family converges weak-star to its projection supremum.

theorem exists_orthogonal_projection_sum (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : I → M) (hp : ∀ i, IsStarProjection (p i))
    (horth : ∀ i j, i ≠ j → p i * p j = 0) :
    ∃ P : M, IsStarProjection P ∧ (∀ i, p i ≤ P) ∧
      (∀ r : M, IsStarProjection r → (∀ i, p i ≤ r) → P ≤ r) ∧
      PredualTendsto e (fun s : Finset I => ∑ i ∈ s, p i) atTop P := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto

lemma OAI.BoundedHochschild.KadisonRingrose.orthogonal_projection_sum_annihilator line 87

Source documentation

Common right annihilators are retained by the full orthogonal sum.

lemma orthogonal_projection_sum_annihilator (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (p : I → M) (a P : M)
    (ht : PredualTendsto e (fun s : Finset I => ∑ i ∈ s, p i) atTop P)
    (hpa : ∀ i, p i * a = 0) : P * a = 0 := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto