FiniteProjectionAbsoluteContinuity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of finite projection comparison

The projection argument behind Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemma 5.2. Projections separately subequivalent to an orthogonal sequence admit decreasing dominating projections with zero weak-star limit. No tracial functional is used.

theorem OAI.BoundedHochschild.KadisonRingrose.finite_subequivalent_orthogonal_tails line 30

Source documentation

In a finite algebra, projections dominated in comparison by an orthogonal sequence have weak-star-null decreasing projection envelopes.

theorem finite_subequivalent_orthogonal_tails (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (p q : ℕ → M)
    (hp : ∀ n, IsStarProjection (p n)) (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0)
    (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q n) :
    ∃ R : ℕ → M, (∀ n, IsStarProjection (R n)) ∧ Antitone R ∧
      (∀ n, p n ≤ R n) ∧ PredualTendsto e R atTop 0 := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.PredualTendsto