MatrixBarLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Passage to the weak-star limit for the bar-operator identity. This module proves convergence of the defects; it does not assert that the finite-group defects vanish.

def OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarDefect line 20
def OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarDefect line 27
lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarDefect_tendsto line 35
lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarDefect_eq_zero_of_eventually line 53
Source documentation
An eventually vanishing finite-section defect has zero weak-star limit. The finite algebraic identity is a separate obligation.
```
lemma countableMatrixBarDefect_eq_zero_of_eventually
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (c : ℕ → PartialIso M) (hi : ∀ i, (c i).initial = 1)
    (ho : ∀ i j, i ≠ j → (c i).final * (c j).final = 0) {n : ℕ}
    (f : Cochain M (n + 1))
    (h : ∀ᶠ k in (matrixAverageUltrafilter : Filter ℕ),
      matrixSectionBarDefect c hi ho f k = 0) :
    countableMatrixBarDefect e c hi ho f = 0 := by
…
```
Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.KadisonRingrose.matrixAverageUltrafilter, OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarDefect, OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarDefect