OAI/Analysis/KadisonKastler/CompleteCorrectionProducts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.correctionProducts line 13
2. theorem OAI.KadisonKastler.correctionProducts_zero line 18
3. theorem OAI.KadisonKastler.correctionProducts_succ line 22
4. theorem OAI.KadisonKastler.correctionProducts_increment line 26
5. theorem OAI.KadisonKastler.correctionProducts_complete_bounds line 34

   Source documentation

   The displacement is bounded by twice the sum of the step sizes. The hypothesis on the partial sums closes the simultaneous bound by two.

   theorem correctionProducts_complete_bounds (S : ℕ → A →L[ℂ] A) (r : ℕ → ℝ)
       (hr : ∀ n, 0 ≤ r n)
       (hsmall : ∀ n, 2 * ∑ i ∈ Finset.range n, r i ≤ 1)
       (hS : ∀ n, CompletelyBoundedBy ((S n).toLinearMap - LinearMap.id) (r n))
       (n : ℕ) :
       CompletelyBoundedBy ((correctionProducts S n).toLinearMap - LinearMap.id)
         (2 * ∑ i ∈ Finset.range n, r i) ∧
       CompletelyBoundedBy (correctionProducts S n).toLinearMap 2 := by
   …

   Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.correctionProducts

6. theorem OAI.KadisonKastler.correctionProducts_star line 75

   Source documentation

   The products preserve the involution if each factor does.

   theorem correctionProducts_star (S : ℕ → A →L[ℂ] A)
       (hS : ∀ n x, S n (star x) = star (S n x)) (n : ℕ) (x : A) :
       correctionProducts S n (star x) = star (correctionProducts S n x) := by
   …

   Mentions: OAI.KadisonKastler.correctionProducts