AsymptoticRowCochain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passage from asymptotically modular row averages to a quadratic cochain. The asymptotic modularity hypothesis is explicit; its general construction is not asserted by this adapter.

theorem OAI.KadisonKastler.cochain_coboundary_weak_limit line 25

theorem OAI.KadisonKastler.quadratic_cochain_of_asymptotic_rows line 40

Source documentation

Asymptotically right-modular normalized rows produce the exact local cochain estimate used by the Newton iteration.

theorem quadratic_cochain_of_asymptotic_rows (M : VonNeumannAlgebra H)
    (m : Algebra M →ₗ[ℂ] Algebra M →ₗ[ℂ] Algebra M)
    (hm : ∀ x y z, m (m x y) z = m x (m y z))
    (hstar : ∀ x y, star (m x y) = m (star y) (star x))
    {c : ℝ} (hc : 0 ≤ c) (hf : HaagerupBound (m - LinearMap.mul ℂ (Algebra M)) c)
    {ι : Type*} (ω : Ultrafilter ι) (n : ι → ℕ) (r : (i : ι) → Fin (n i) → Algebra M)
    (hr : ∀ i, ∑ k, r i k * star (r i k) = 1)
    (hmod : ∀ a b ξ η, Tendsto
      (fun i => inner ℂ η ((finiteCochainModuleDefect (r i)
        (m - LinearMap.mul ℂ (Algebra M)) a b : H →L[ℂ] H) ξ))
      (ω : Filter ι) (𝓝 0)) :
    ∃ D : Algebra M →ₗ[ℂ] Algebra M, CompletelyBoundedBy D c ∧
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.finiteCochainModuleDefect, OAI.KadisonKastler.CompletelyBoundedBy