OAI/Analysis/TraceCone/StrongDensity.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TraceConeClassification.HilbertTuple line 21
2. abbrev OAI.TraceConeClassification.diagonalOp line 23
3. lemma OAI.TraceConeClassification.diagonalOp_apply line 26
4. lemma OAI.TraceConeClassification.diagonalOp_star line 29
5. abbrev OAI.TraceConeClassification.diagonalHom line 38
6. abbrev OAI.TraceConeClassification.tupleInclusion line 41
7. lemma OAI.TraceConeClassification.tupleInclusion_apply line 45
8. lemma OAI.TraceConeClassification.tuple_decomposition line 50
9. lemma OAI.TraceConeClassification.diagonalOp_inclusion line 55
10. abbrev OAI.TraceConeClassification.matrixEntry line 61
11. lemma OAI.TraceConeClassification.matrixEntry_apply line 65
12. lemma OAI.TraceConeClassification.diagonal_bicommutant line 68
13. theorem OAI.TraceConeClassification.bicommutant_strong_density line 75

    Source documentation

    The finite-vector form of strong-operator density in the bicommutant.

    theorem bicommutant_strong_density
        (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
        (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
        (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, ∀ i, ‖a (ξ i) - T (ξ i)‖ < ε := by
    …

14. lemma OAI.TraceConeClassification.bicommutant_approximating_sequence line 87
15. theorem OAI.TraceConeClassification.bicommutant_selfadjoint_strong_density line 102

    Source documentation

    Self-adjoint strong density is needed before the contractive functional-calculus step.

    theorem bicommutant_selfadjoint_strong_density
        (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
        (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
        (hsa : IsSelfAdjoint T) (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, IsSelfAdjoint a ∧ ∀ i, ‖a (ξ i) - T (ξ i)‖ < ε := by
    …

16. def OAI.TraceConeClassification.densityG line 114

    Source documentation

    Rational functions used to obtain bounded approximants without bounded input norms.

    def densityG (t : ℝ) : ℝ := (1 + t^2)⁻¹

17. def OAI.TraceConeClassification.densityH line 115
18. def OAI.TraceConeClassification.densityF line 116
19. def OAI.TraceConeClassification.densityK line 117
20. lemma OAI.TraceConeClassification.density_den_pos line 119
21. lemma OAI.TraceConeClassification.densityG_cont line 120
22. lemma OAI.TraceConeClassification.densityH_cont line 122
23. lemma OAI.TraceConeClassification.densityF_cont line 125
24. lemma OAI.TraceConeClassification.densityK_cont line 126
25. lemma OAI.TraceConeClassification.densityG_bound line 131
26. lemma OAI.TraceConeClassification.densityH_bound line 134
27. lemma OAI.TraceConeClassification.densityF_bound line 138
28. lemma OAI.TraceConeClassification.density_FK line 144
29. def OAI.TraceConeClassification.densityg line 156
30. def OAI.TraceConeClassification.densityh line 157
31. def OAI.TraceConeClassification.densityf line 158
32. lemma OAI.TraceConeClassification.densityg_norm line 160
33. lemma OAI.TraceConeClassification.densityh_norm line 162
34. lemma OAI.TraceConeClassification.densityf_norm line 164
35. lemma OAI.TraceConeClassification.densityf_eq line 166
36. lemma OAI.TraceConeClassification.density_selfadjoint line 168
37. lemma OAI.TraceConeClassification.densityg_mul line 170
38. lemma OAI.TraceConeClassification.mul_densityg line 178
39. lemma OAI.TraceConeClassification.densityh_mul line 182
40. lemma OAI.TraceConeClassification.mul_densityh line 194
41. lemma OAI.TraceConeClassification.densityh_difference line 199
42. lemma OAI.TraceConeClassification.density_FK_operator line 209
43. lemma OAI.TraceConeClassification.densityh_apply_difference line 224
44. theorem OAI.TraceConeClassification.kaplansky_selfadjoint line 245

    Source documentation

    Contractive self-adjoint Kaplansky approximation, with actual construction from the double commutant and no bound assumed on the initial approximants.

    theorem kaplansky_selfadjoint
        (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hclosed : IsClosed (A : Set (H →L[ℂ] H)))
        (T : H →L[ℂ] H)
        (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
        (hsa : IsSelfAdjoint T) (hnorm : ‖T‖ ≤ 1)
        (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, IsSelfAdjoint a ∧ ‖a‖ ≤ 1 ∧ ∀ i, ‖a (ξ i) - T (ξ i)‖ < ε := by
    …

45. lemma OAI.TraceConeClassification.tuple_inner_inclusion line 277
46. lemma OAI.TraceConeClassification.tuple_inclusion_inner line 284
47. lemma OAI.TraceConeClassification.tuple_inclusion_norm line 288
48. lemma OAI.TraceConeClassification.matrixEntry_star line 293
49. lemma OAI.TraceConeClassification.matrixEntry_norm line 307
50. lemma OAI.TraceConeClassification.matrixEntry_continuous line 317
51. lemma OAI.TraceConeClassification.matrixEntry_zero line 323
52. lemma OAI.TraceConeClassification.matrixEntry_add line 326
53. lemma OAI.TraceConeClassification.matrixEntry_smul line 329
54. lemma OAI.TraceConeClassification.matrixEntry_one line 332
55. lemma OAI.TraceConeClassification.matrixEntry_mul line 338
56. lemma OAI.TraceConeClassification.matrixEntry_diagonal line 345
57. def OAI.TraceConeClassification.matrixSubalgebra line 350
58. lemma OAI.TraceConeClassification.matrixSubalgebra_closed line 369
59. lemma OAI.TraceConeClassification.diagonal_mem_matrixSubalgebra line 375
60. lemma OAI.TraceConeClassification.diagonal_matrix_bicommutant line 381
61. def OAI.TraceConeClassification.blockOp line 390
62. lemma OAI.TraceConeClassification.blockOp_apply line 394
63. lemma OAI.TraceConeClassification.blockOp_star line 398
64. lemma OAI.TraceConeClassification.matrixEntry_blockOp line 411
65. lemma OAI.TraceConeClassification.blockOp_mem_matrixSubalgebra line 419
66. lemma OAI.TraceConeClassification.blockOp_eq_diagonal line 425
67. def OAI.TraceConeClassification.offDiagonalOp line 431
68. lemma OAI.TraceConeClassification.offDiagonal_selfadjoint line 434
69. lemma OAI.TraceConeClassification.offDiagonal_apply_zero line 438
70. lemma OAI.TraceConeClassification.offDiagonal_apply_one line 440
71. lemma OAI.TraceConeClassification.offDiagonal_norm line 443
72. lemma OAI.TraceConeClassification.offDiagonal_bicommutant line 456
73. theorem OAI.TraceConeClassification.kaplansky_strong_star line 481

    Source documentation

    Contractive strong-star density obtained by self-adjoint matrix amplification.

    theorem kaplansky_strong_star
        (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hclosed : IsClosed (A : Set (H →L[ℂ] H)))
        (T : H →L[ℂ] H)
        (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
        (hnorm : ‖T‖ ≤ 1) (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, ‖a‖ ≤ 1 ∧ ∀ i,
          ‖a (ξ i) - T (ξ i)‖ < ε ∧ ‖star a (ξ i) - star T (ξ i)‖ < ε := by
    …

74. def OAI.TraceConeClassification.ofWOTHom line 507
75. def OAI.TraceConeClassification.weakClosure line 515
76. lemma OAI.TraceConeClassification.weakClosure_mem line 519
77. lemma OAI.TraceConeClassification.weakClosure_closed line 523
78. lemma OAI.TraceConeClassification.weakClosure_cfc line 527
79. def OAI.TraceConeClassification.nonunitalSelfAdjointOrbit line 533
80. lemma OAI.TraceConeClassification.weakClosure_selfadjoint_orthogonal line 539
81. lemma OAI.TraceConeClassification.weakClosure_selfadjoint_strong_density line 574
82. lemma OAI.TraceConeClassification.nonunital_kaplansky_selfadjoint line 605
83. def OAI.TraceConeClassification.nonunitalMatrixSubalgebra line 633
84. lemma OAI.TraceConeClassification.nonunitalMatrixSubalgebra_closed line 651
85. lemma OAI.TraceConeClassification.diagonal_mem_nonunitalMatrixSubalgebra line 657
86. lemma OAI.TraceConeClassification.blockOp_mem_nonunitalMatrixSubalgebra line 663
87. lemma OAI.TraceConeClassification.blockOp_WOT_continuous line 670
88. lemma OAI.TraceConeClassification.offDiagonal_WOT_continuous line 678
89. lemma OAI.TraceConeClassification.offDiagonal_weakClosure line 685
90. theorem OAI.TraceConeClassification.nonunital_kaplansky_strong_star line 697

    Source documentation

    Literal norm-bounded strong-star density in the weak operator closure, valid also for degenerate nonunital representations.

    theorem nonunital_kaplansky_strong_star
        (A : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
        (hclosed : IsClosed (A : Set (H →L[ℂ] H))) (T : H →L[ℂ] H)
        (hT : ContinuousLinearMapWOT.ofCLM T ∈ closure
          (ContinuousLinearMapWOT.ofCLM '' (A : Set (H →L[ℂ] H))))
        (hnorm : ‖T‖ ≤ 1) (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, ‖a‖ ≤ 1 ∧ ∀ i,
          ‖a (ξ i) - T (ξ i)‖ < ε ∧ ‖star a (ξ i) - star T (ξ i)‖ < ε := by
    …

91. lemma OAI.TraceConeClassification.matrixEntry_decomposition line 725
92. lemma OAI.TraceConeClassification.matrix_weakClosure line 731
93. theorem OAI.TraceConeClassification.nonunital_matrix_kaplansky line 746

    Source documentation

    Matrix-level version for approximating positive Choi square roots; every approximating entry remains in the fixed hereditary algebra.

    theorem nonunital_matrix_kaplansky
        (m : ℕ) (A : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
        (hclosed : IsClosed (A : Set (H →L[ℂ] H)))
        (T : HilbertTuple m H →L[ℂ] HilbertTuple m H)
        (hT : ∀ i j, matrixEntry m T i j ∈ weakClosure A) (hnorm : ‖T‖ ≤ 1)
        (n : ℕ) (ξ : Fin n → HilbertTuple m H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a : HilbertTuple m H →L[ℂ] HilbertTuple m H,
          (∀ i j, matrixEntry m a i j ∈ A) ∧ ‖a‖ ≤ 1 ∧ ∀ i,
            ‖a (ξ i) - T (ξ i)‖ < ε ∧ ‖star a (ξ i) - star T (ξ i)‖ < ε :=
    …

    Mentions: OAI.TraceConeClassification.HilbertTuple, OAI.TraceConeClassification.matrixEntry, OAI.TraceConeClassification.weakClosure

94. lemma OAI.TraceConeClassification.weakClosure_strong_star_density line 766

    Source documentation

    Strong-star approximation on finitely many vectors, without a norm bound on the approximants. No closed-range assumption is necessary.

    lemma weakClosure_strong_star_density (A : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
        (T : H →L[ℂ] H) (hT : T ∈ weakClosure A)
        (n : ℕ) (ξ : Fin n → H) (ε : ℝ) (hε : 0 < ε) :
        ∃ a ∈ A, ∀ i, ‖a (ξ i)-T (ξ i)‖ < ε ∧ ‖star a (ξ i)-star T (ξ i)‖ < ε := by
    …

    Mentions: OAI.TraceConeClassification.weakClosure