OAI/Analysis/FactorGeneration/TraceTopology.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.Tracial.bounded_trace_limit line 21
2. theorem OAI.Generator.Tracial.trace_ball_isClosed line 36

   Source documentation

   The trace image of an operator-norm ball is norm closed in H.

   theorem trace_ball_isClosed (C : ℝ) :
       IsClosed {ξ : H | ∃ b : M.toStarSubalgebra, ‖b‖ ≤ C ∧
         (b : H →L[ℂ] H) τ.vector = ξ} := by
   …

3. theorem OAI.Generator.Tracial.trace_ball_convex line 46
4. theorem OAI.Generator.Tracial.bounded_representative_of_closed_convexHull line 61

   Source documentation

   Every point of the actual closed convex hull has an algebra representative with the same operator norm bound.

   theorem bounded_representative_of_closed_convexHull (s : Set H) (C : ℝ)
       (hs : ∀ ξ ∈ s, ∃ b : M.toStarSubalgebra, ‖b‖ ≤ C ∧
         (b : H →L[ℂ] H) τ.vector = ξ)
       {ξ : H} (hξ : ξ ∈ closure (convexHull ℝ s)) :
       ∃ b : M.toStarSubalgebra, ‖b‖ ≤ C ∧ (b : H →L[ℂ] H) τ.vector = ξ := by
   …

5. def OAI.Generator.Tracial.baseVector line 72
6. def OAI.Generator.Tracial.conjugateLinear line 77
7. theorem OAI.Generator.Tracial.conjugateLinear_mul line 83
8. theorem OAI.Generator.Tracial.conjugateLinear_one line 88
9. theorem OAI.Generator.Tracial.conjugate_norm_le line 91
10. theorem OAI.Generator.Tracial.conjugate_norm₂_le line 101
11. theorem OAI.Generator.Tracial.conjugate_norm₂ line 112
12. def OAI.Generator.Tracial.algebraOrbit line 118
13. def OAI.Generator.Tracial.traceOrbitHull line 121
14. theorem OAI.Generator.Tracial.traceOrbitHull_eq line 124
15. theorem OAI.Generator.Tracial.traceOrbitHull_nonempty line 128
16. theorem OAI.Generator.Tracial.traceOrbitHull_representative line 133
17. theorem OAI.Generator.Tracial.conjugate_mem_convexHull line 140
18. theorem OAI.Generator.Tracial.conjugate_mem_traceOrbitHull line 151
19. theorem OAI.Generator.Tracial.baseVector_injective line 178
20. theorem OAI.Generator.Tracial.convex_minimum_unique line 186
21. theorem OAI.Generator.Tracial.traceOrbitHull_minimum line 198
22. theorem OAI.Generator.Tracial.trace_conjugate line 220
23. theorem OAI.Generator.Tracial.traceOrbitHull_trace line 226
24. theorem OAI.Generator.Tracial.traceOrbitHull_distance line 239