OAI/Analysis/KadisonKastler/CentralProjectionAveraging.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.swap_formula_fixes_projection line 17

   Source documentation

   Swapping the matched parts fixes every projection orthogonal to both.

   theorem swap_formula_fixes_projection (v : PartialIsometry M)
       (u : unitary (Algebra M))
       (hu : (u : Algebra M) = v.val + star v.val + (1 - (v.support.val + v.target.val)))
       (r : AlgebraProjection M)
       (hr : v.support.val * r.val = 0) (ht : v.target.val * r.val = 0) :
       (u : Algebra M) * r.val * star (u : Algebra M) = r.val := by
   …

   Mentions: OAI.KadisonKastler.Algebra

2. theorem OAI.KadisonKastler.exists_central_projection_average line 46

   Source documentation

   Matched positive and negative spectral parts give complementary upper bounds measured by one central projection.

   theorem exists_central_projection_average (p : AlgebraProjection M) :
       ∃ (A : FiniteInnerAverage M) (z : AlgebraProjection M),
         (∀ a : Algebra M, a * z.val = z.val * a) ∧
         A.apply p.val.val ≤ (1 / 2 : ℝ) • (1 + z.val.val) ∧
         A.apply (1 - p.val.val) ≤ (1 / 2 : ℝ) • (2 • (1 : H →L[ℂ] H) - z.val.val) := by
   …

   Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra