QuotientMomentLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passing coordinate moment limits to the actual tracial quotient.

def OAI.KadisonSimilarity.FiniteQuotientMoments line 19
Source documentation
All bounded finite words in the centered coefficient family vanish.
```
def FiniteQuotientMoments (A : ℕ → (ℕ →ᵇ B)) (u : ℕ → unitary B) : Prop :=
…
```
def OAI.KadisonSimilarity.AllQuotientMoments line 27
Source documentation
Every admissible mixed word in an indexed coefficient family vanishes.
```
def AllQuotientMoments {I : Type*} (A : I → (ℕ →ᵇ B)) (u : ℕ → unitary B) : Prop :=
…
```

theorem OAI.KadisonSimilarity.finiteQuotientMoments_of_limits line 36

Source documentation

The quotient step uses only the coordinate limits, with no factor or freeness assumption.

theorem finiteQuotientMoments_of_limits (hω : (ω : Filter ℕ) ≤ atTop)
    (A : ℕ → (ℕ →ᵇ B)) (u : ℕ → unitary B)
    (hu : ∀ m K N : ℕ, ∀ a : BoundedWord (Fin m) K N, admissibleTail a.2.val →
      Tendsto (fun n => τ (mixedEval
        (fun i : Fin m => (1 / 2 : ℂ) • (A i.val n - τ (A i.val n) • 1))
        (asPartialUnitary (u n)) a.1 a.2.val)) atTop (𝓝 0)) :
    FiniteQuotientMoments τ h1 ω tr A u := by
…

Mentions: OAI.KadisonSimilarity.FiniteQuotientMoments