OAI/Analysis/KadisonKastler/MultiplicationCorrectionFromRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.finiteCochainModuleDefect_as_average line 27
2. theorem OAI.KadisonKastler.cochain_module_defect_tendsto line 34
3. theorem OAI.KadisonKastler.quadraticCochainSolver_of_modular_rows line 53
4. theorem OAI.KadisonKastler.publishedMultiplicationCorrection_of_modular_rows line 67

   Source documentation

   A single modular row net suffices for quantitative multiplication correction.

   theorem publishedMultiplicationCorrection_of_modular_rows (M : VonNeumannAlgebra H)
       {ι : Type*} (ω : Ultrafilter ι) (n : ι → ℕ)
       (r : (i : ι) → Fin (n i) → Algebra M)
       (hr : ∀ i, ∑ k, r i k * star (r i k) = 1)
       (hav : ∀ (F : Algebra M →ₗ[ℂ] Algebra M) (c : ℝ), 0 ≤ c → CompletelyBoundedBy F c →
         ∃ z : Algebra M, ∀ y ξ η, Tendsto
           (fun i => inner ℂ η ((finiteRightAverage (r i) F y : H →L[ℂ] H) ξ))
           (ω : Filter ι) (𝓝 (inner ℂ η (((z * y : Algebra M) : H →L[ℂ] H) ξ)))) :
       PublishedMultiplicationCorrection M := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.finiteRightAverage, OAI.KadisonKastler.PublishedMultiplicationCorrection