OAI/Analysis/BoundedHochschild/MatrixAverageLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedHochschild.KadisonRingrose.predualTendsto_congr_eventually line 20
2. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_of_predualTendsto line 26
3. lemma OAI.BoundedHochschild.KadisonRingrose.exists_finite_matrix_section_average line 48
4. theorem OAI.BoundedHochschild.KadisonRingrose.matrix_section_average_limit line 66

   Source documentation

   This retains the limit of the supplied averages, so any separately verified linear identity of those averages can be passed to the same limit.

   theorem matrix_section_average_limit (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
       (c : ℕ → HochschildComparison.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)) (C : ℝ) (hC : 0 ≤ C)
       (hF : ∀ k, ‖F k‖ ≤ C)
       (hmodule : ∀ k, ∀ i j : Fin k, MultimodularAt (F k) (countableMatrixUnit c i.val j.val)) :
       ∃ A : Cochain M (n + 1), ‖A‖ ≤ C ∧ MultimodularOver (countableMatrixAlgebra c) A ∧
         ∀ x, PredualTendsto e (fun k => F k x) (Ultrafilter.of (atTop : Filter ℕ) : Filter ℕ) (A x) := by
   …

   Mentions: OAI.HochschildComparison.PartialIso, OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.KadisonRingrose.MultimodularAt, OAI.BoundedHochschild.KadisonRingrose.countableMatrixUnit, OAI.BoundedHochschild.KadisonRingrose.MultimodularOver, OAI.BoundedHochschild.KadisonRingrose.countableMatrixAlgebra, OAI.BoundedHochschild.PredualTendsto