UniformProjectionSums.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform summation of orthogonal projections

The positive case of the gliding-block argument in Ringrose, Theorem 4.7: uniform decay on orthogonal sequences implies uniform complete additivity.

lemma OAI.BoundedHochschild.KadisonRingrose.disjoint_finset_sequence line 22
lemma OAI.BoundedHochschild.KadisonRingrose.orthogonal_projection_finset_sum_le line 46

theorem OAI.BoundedHochschild.KadisonRingrose.uniform_orthogonal_sum_remainder line 59

Source documentation

Uniform orthogonal-sequence decay forces uniformly small remainders of arbitrary orthogonal sums. Only the positive, completely additive case is used.

theorem uniform_orthogonal_sum_remainder
    (K : Set (StrongDual ℂ M))
    (hadd : ∀ F ∈ K, CompletelyAdditive F)
    (hdecay : ∀ q : ℕ → M, (∀ n, IsStarProjection (q n)) →
      (∀ m n, m ≠ n → q m * q n = 0) → ∀ ε : ℝ, 0 < ε →
        ∀ᶠ n in atTop, ∀ F ∈ K, ‖F (q n)‖ < ε)
    (I : Type u) (p : I → M) (hp : ∀ i, IsStarProjection (p i))
    (ho : ∀ i j, i ≠ j → p i * p j = 0)
    (P : M) (hP : IsStarProjection P) (hu : ∀ i, p i ≤ P)
    (hl : ∀ r : M, IsStarProjection r → (∀ i, p i ≤ r) → P ≤ r)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ s : Finset I, ∀ F ∈ K, (F (P - ∑ i ∈ s, p i)).re < ε := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyAdditive