OAI/Analysis/FactorGeneration/HilbertLimits.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Multiplication and adjoint limits in L2, with the necessary uniform operator norm bounds stated explicitly.

  1. theorem OAI.Generator.Tracial.tendsto_vector_iff_norm₂ line 22
  2. theorem OAI.Generator.Tracial.norm₂_limit_unique line 30
  3. theorem OAI.Generator.Tracial.norm₂_limit_star line 41
  4. theorem OAI.Generator.Tracial.norm₂_limit_mul line 46
  5. theorem OAI.Generator.Tracial.norm₂_limit_trace line 63
  6. def OAI.Generator.vectorOrbitMap line 80
  7. def OAI.Generator.vectorOrbitClosure line 85
  8. instance OAI.Generator.vectorOrbitClosure_complete line 88
  9. theorem OAI.Generator.mem_vectorOrbitClosure line 92
  10. theorem OAI.Generator.vectorOrbitClosure_invariant line 96
  11. theorem OAI.Generator.vectorOrbitProjection_commutes line 106
  12. theorem OAI.Generator.commutant_orbitClosure_eq_top line 113
  13. theorem OAI.Generator.commutant_orbit_dense line 136
  14. abbrev OAI.Generator.Tracial.traceCyclicSpace line 157
  15. def OAI.Generator.Tracial.traceCyclicVector line 159
  16. def OAI.Generator.Tracial.traceCyclicOperator line 161
  17. theorem OAI.Generator.Tracial.traceCyclicOperator_apply line 165
  18. theorem OAI.Generator.Tracial.traceCyclicOperator_star line 168
  19. def OAI.Generator.Tracial.traceCyclicHom line 178
  20. theorem OAI.Generator.Tracial.traceCyclicHom_injective line 188
  21. theorem OAI.Generator.Tracial.traceCyclicHom_norm line 196
  22. theorem OAI.Generator.Tracial.traceCyclicHom_isometry line 201
  23. theorem OAI.Generator.Tracial.traceCyclicVector_norm line 204
  24. theorem OAI.Generator.Tracial.traceCyclicHom_trace line 206
  25. theorem OAI.Generator.Tracial.traceCyclicHom_norm₂ line 209
  26. theorem OAI.Generator.Tracial.traceCyclicHom_cyclic line 212
  27. theorem OAI.Generator.Tracial.traceCyclicSpace_separable line 220
  28. def OAI.Generator.Tracial.cyclicBallMap line 235
  29. theorem OAI.Generator.Tracial.cyclicBallMap_continuous line 239
  30. theorem OAI.Generator.Tracial.cyclicBallMap_injective line 245
  31. theorem OAI.Generator.Tracial.cyclicBallMap_isClosedEmbedding line 254
  32. def OAI.Generator.Tracial.cyclicWeakOperatorBall line 260
  33. theorem OAI.Generator.Tracial.cyclicWeakOperatorBall_eq_range line 263
  34. theorem OAI.Generator.Tracial.cyclicWeakOperatorBall_isCompact line 272
  35. theorem OAI.Generator.Tracial.cyclicWeakOperatorBall_isClosed line 278
  36. theorem OAI.Generator.Tracial.traceVector_weak_continuous line 293
  37. def OAI.Generator.Tracial.traceFunctionalSlice line 299
  38. theorem OAI.Generator.Tracial.traceFunctionalSlice_convex line 302
  39. theorem OAI.Generator.Tracial.traceFunctionalSlice_isClosed line 321
  40. theorem OAI.Generator.Tracial.unitBall_functional_sublevel_isClosed line 337
  41. theorem OAI.Generator.Tracial.unitBall_functional_continuous_of_norm₂ line 362
  42. theorem OAI.Generator.bounded_operators_tendsto_of_dense line 388
  43. theorem OAI.Generator.Tracial.norm₂_limit_strong line 424
  44. theorem OAI.Generator.Tracial.norm₂_limit_strong_star line 440
  45. theorem OAI.Generator.Tracial.bounded_strong_iff_norm₂ line 451