OAI/Analysis/KadisonKastler/ProjectionSwapAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_unitary_swap_orthogonal_formula line 18

   Source documentation

   Orthogonal equivalent projections are exchanged by an ambient unitary.

   theorem exists_unitary_swap_orthogonal_formula (v : PartialIsometry M)
       (ho : v.support.val * v.target.val = 0) :
       ∃ u : unitary (Algebra M),
         (u : Algebra M) * v.support.val * star (u : Algebra M) = v.target.val ∧
         (u : Algebra M) = v.val + star v.val + (1 - (v.support.val + v.target.val)) := by
   …

   Mentions: OAI.KadisonKastler.Algebra

2. theorem OAI.KadisonKastler.exists_unitary_swap_orthogonal line 74

   Source documentation

   Orthogonal equivalence extends by the identity on the remaining space.

   theorem exists_unitary_swap_orthogonal (p q : AlgebraProjection M)
       (ho : p.val * q.val = 0) (he : p.Equivalent q) :
       ∃ u : unitary (Algebra M), (u : Algebra M) * p.val * star (u : Algebra M) = q.val := by
   …

   Mentions: OAI.KadisonKastler.Algebra

3. theorem OAI.KadisonKastler.exists_projection_half_average line 82

   Source documentation

   A projection subequivalent to its complement can be averaged below one-half.

   theorem exists_projection_half_average (p : AlgebraProjection M)
       (he : p.Subequivalent (⟨1 - p.val, p.property.one_sub⟩ : AlgebraProjection M)) :
       ∃ A : FiniteInnerAverage M,
         A.apply p.val.val ≤ (1 / 2 : ℂ) • (1 : H →L[ℂ] H) := by
   …

   Mentions: OAI.KadisonKastler.FiniteInnerAverage