InfiniteProjectionAveraging.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact averaging of projections with two infinite sides

theorem OAI.KadisonKastler.exists_unitary_conjugacy_of_equivalent_complements line 18

Source documentation

Complementary equivalences assemble to a unitary in the original algebra.

theorem exists_unitary_conjugacy_of_equivalent_complements
    (p q : AlgebraProjection M) (hpq : p.Equivalent q)
    (hc : AlgebraProjection.Equivalent
      (⟨1 - p.val, p.property.one_sub⟩ : AlgebraProjection M)
      (⟨1 - q.val, q.property.one_sub⟩ : AlgebraProjection M)) :
    ∃ u : unitary (Algebra M), (u : Algebra M) * p.val * star (u : Algebra M) = q.val := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_unitary_swap_of_infinite_sides line 61

Source documentation

A projection and its infinite complement can be interchanged in a separably represented factor.

theorem exists_unitary_swap_of_infinite_sides [TopologicalSpace.SeparableSpace H]
    (hM : ScalarCenter M) (p : AlgebraProjection M)
    (hp : ¬ FiniteProjectionIn M p.val)
    (hc : ¬ FiniteProjectionIn M (1 - p.val)) :
    ∃ u : unitary (Algebra M),
      (u : Algebra M) * p.val * star (u : Algebra M) = 1 - p.val := by
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_half_average_of_infinite_sides line 81

Source documentation

The identity and a swapping unitary give the exact scalar one-half average.

theorem exists_half_average_of_infinite_sides [TopologicalSpace.SeparableSpace H]
    (hM : ScalarCenter M) (p : AlgebraProjection M)
    (hp : ¬ FiniteProjectionIn M p.val)
    (hc : ¬ FiniteProjectionIn M (1 - p.val)) :
    ∃ A : FiniteInnerAverage M,
      A.apply p.val.val = (1 / 2 : ℂ) • (1 : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.FiniteInnerAverage