FiniteIncreasingComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Increasing limits of subequivalent projections

Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemma 5.1: an increasing supremum of projections subequivalent to a fixed finite projection is still subequivalent to it. The proof aligns successive partial isometries inside the finite corner and then takes their chain supremum.

theorem OAI.BoundedHochschild.KadisonRingrose.finite_increasing_subequivalence line 27

Source documentation

Increasing limits preserve subequivalence to a finite projection.

theorem finite_increasing_subequivalence (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {q : M} (hq : IsStarProjection q) (hfinite : FiniteCorner q)
    (p : ℕ → M) (hmono : Monotone p)
    (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q) :
    ∃ v : PartialIso M, v.final ≤ q ∧ (∀ n, p n ≤ v.initial) ∧
      ∀ r : M, IsStarProjection r → (∀ n, p n ≤ r) → v.initial ≤ r := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner

theorem OAI.BoundedHochschild.KadisonRingrose.finite_subequivalence_at_supremum line 62

Source documentation

Ringrose's Lemma 5.1 with the supremum specified in advance.

theorem finite_subequivalence_at_supremum (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {q s : M} (hq : IsStarProjection q) (hfinite : FiniteCorner q)
    (hs : IsStarProjection s) (p : ℕ → M) (hmono : Monotone p)
    (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q)
    (hupper : ∀ n, p n ≤ s)
    (hleast : ∀ r : M, IsStarProjection r → (∀ n, p n ≤ r) → s ≤ r) :
    ∃ v : PartialIso M, v.initial = s ∧ v.final ≤ q := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner