OAI/Analysis/KadisonKastler/ProjectionNormalWords.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KadisonKastler.NonzeroHaarExponent line 15
2. inductive OAI.KadisonKastler.ProjectionNormalWord line 17
3. def OAI.KadisonKastler.projectionNormalTail line 25
4. def OAI.KadisonKastler.projectionNormalEval line 30
5. def OAI.KadisonKastler.projectionNormalSpan line 36
6. theorem OAI.KadisonKastler.projectionNormalEval_mem line 39
7. theorem OAI.KadisonKastler.one_mem_projectionNormalSpan line 43
8. theorem OAI.KadisonKastler.centered_mem_projectionNormalSpan line 46
9. theorem OAI.KadisonKastler.projectionNormalTail_mem line 49
10. theorem OAI.KadisonKastler.centered_mul_projectionNormalEval_mem line 56
11. theorem OAI.KadisonKastler.haarPower_mul_projectionNormalEval_mem line 87
12. theorem OAI.KadisonKastler.centered_mul_projectionNormalSpan_mem line 111
13. theorem OAI.KadisonKastler.haarPower_mul_projectionNormalSpan_mem line 122
14. theorem OAI.KadisonKastler.centered_projection_quadratic line 135
15. theorem OAI.KadisonKastler.adjoin_projection_haar_le_normalSpan line 143

    Source documentation

    The algebra generated by the projection and all integer unitary powers is contained in the explicit finite normal-word span.

    theorem adjoin_projection_haar_le_normalSpan (p : B) (hp : IsIdempotentElem p)
        (v : unitary B) (t : ℂ) :
        (Algebra.adjoin ℂ (insert p (Set.range (haarPower v)))).toSubmodule ≤
          projectionNormalSpan (p - t • (1 : B)) v := by
    …

    Mentions: OAI.KadisonKastler.haarPower, OAI.KadisonKastler.projectionNormalSpan

16. def OAI.KadisonKastler.projectionNormalPairs line 172
17. theorem OAI.KadisonKastler.centeredHaarWord_projectionNormalPairs line 176
18. theorem OAI.KadisonKastler.projectionNormalPairs_property line 187
19. theorem OAI.KadisonKastler.projectionNormalPairs_chain line 200
20. theorem OAI.KadisonKastler.FreeHaarMoments.trace_base_mul_mixed_normalWord_zero line 212
21. theorem OAI.KadisonKastler.FreeHaarMoments.exists_affine_pairing_of_normalSpan line 230

    Source documentation

    Every finite normal-word combination has the same Base pairings as an affine expression in its centered projection.

    theorem exists_affine_pairing_of_normalSpan (h : FreeHaarMoments τ A v)
        {q x : B} (hq : q ∈ A) (hqτ : τ.toLinearMap q = 0)
        (hx : x ∈ projectionNormalSpan q v) :
        ∃ α β : ℂ, ∀ b ∈ A,
          τ.toLinearMap (b * x) = τ.toLinearMap (b * (α • q + β • (1 : B))) := by
    …

    Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.projectionNormalSpan

22. theorem OAI.KadisonKastler.FreeHaarMoments.exists_affine_projection_pairing line 261

    Source documentation

    The generated projection--Haar algebra has Base pairings in exactly the two-dimensional span of the projection and identity.

    theorem exists_affine_projection_pairing (h : FreeHaarMoments τ A v)
        {p x : B} (hp : IsStarProjection p) (hpA : p ∈ A)
        (hx : x ∈ Algebra.adjoin ℂ (insert p (Set.range (haarPower v)))) :
        ∃ α β : ℂ, ∀ b ∈ A,
          τ.toLinearMap (b * x) = τ.toLinearMap (b * (α • p + β • (1 : B))) := by
    …

    Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarPower

23. theorem OAI.KadisonKastler.FreeHaarMoments.expectation_eq_affine_projection line 280

    Source documentation

    Hence an actual trace-pairing projection onto Base maps the generated algebra into span {p, 1}.

    theorem expectation_eq_affine_projection (h : FreeHaarMoments τ A v)
        (E : B →ₗ[ℂ] B) (hE : ∀ x, E x ∈ A)
        (hpair : ∀ b ∈ A, ∀ x, τ.toLinearMap (b * E x) = τ.toLinearMap (b * x))
        {p x : B} (hp : IsStarProjection p) (hpA : p ∈ A)
        (hx : x ∈ Algebra.adjoin ℂ (insert p (Set.range (haarPower v)))) :
        ∃ α β : ℂ, E x = α • p + β • (1 : B) := by
    …

    Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarPower