OAI/Analysis/KadisonKastler/CompleteCorrectionLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_complete_correction_limit line 18

   Source documentation

   Complete estimates on the successive differences produce an actual continuous linear limit and the same complete estimate on its displacement.

   theorem exists_complete_correction_limit
       (L : ℕ → A →L[ℂ] A) (c : ℕ → ℝ)
       (hc : ∀ n, 0 ≤ c n) (hsum : Summable c)
       (hstep : ∀ n, CompletelyBoundedBy
         ((L (n + 1)).toLinearMap - (L n).toLinearMap) (c n)) :
       ∃ T : A →L[ℂ] A, Tendsto L atTop (𝓝 T) ∧
         CompletelyBoundedBy (T.toLinearMap - (L 0).toLinearMap) (∑' n, c n) := by
   …

   Mentions: OAI.KadisonKastler.CompletelyBoundedBy

2. theorem OAI.KadisonKastler.correction_of_summable_steps line 56

   Source documentation

   Summably small corrections which asymptotically intertwine a product converge to an exact invertible star-preserving intertwiner.

   theorem correction_of_summable_steps
       (m : A →ₗ[ℂ] A →ₗ[ℂ] A) (L : ℕ → A →L[ℂ] A)
       (hzero : L 0 = ContinuousLinearMap.id ℂ A) (c d : ℕ → ℝ)
       (hc : ∀ n, 0 ≤ c n) (hsum : Summable c) (hsmall : (∑' n, c n) < 1)
       (hstep : ∀ n, CompletelyBoundedBy
         ((L (n + 1)).toLinearMap - (L n).toLinearMap) (c n))
       (hstar : ∀ n x, L n (star x) = star (L n x))
       (hd : Tendsto d atTop (𝓝 0))
       (hm : ∀ n x y, ‖L n (m x y) - L n x * L n y‖ ≤ d n * ‖x‖ * ‖y‖) :
       ∃ T : A ≃ₗ[ℂ] A,
         (∀ x y, T (m x y) = T x * T y) ∧
         (∀ x, T (star x) = star (T x)) ∧
   …

   Mentions: OAI.KadisonKastler.CompletelyBoundedBy