OAI/Analysis/BoundedHochschild/TracialModulus.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Bounded-ball continuity, tracial null spaces and quotient seminorms.

  1. def OAI.TracialUltrapower.BallSequential line 20
  2. def OAI.TracialUltrapower.BallModulus line 26
  3. theorem OAI.TracialUltrapower.ballSequential_iff_modulus line 30
  4. theorem OAI.TracialUltrapower.BallModulus.map_tendsto line 53
  5. def OAI.TracialUltrapower.nullSubmodule line 73
  6. theorem OAI.TracialUltrapower.mem_nullSubmodule line 83
  7. theorem OAI.TracialUltrapower.nullSubmodule_map_invariant line 88
  8. def OAI.TracialUltrapower.quotientMap line 98
  9. theorem OAI.TracialUltrapower.quotientMap_mk line 104
  10. theorem OAI.TracialUltrapower.norm_quotientMap_le line 109
  11. def OAI.TracialUltrapower.quotientContinuousMap line 133
  12. theorem OAI.TracialUltrapower.norm_quotientContinuousMap_le line 138
  13. theorem OAI.TracialUltrapower.isClosed_nullSubmodule line 150
  14. def OAI.TracialUltrapower.sequenceTwoNorm line 191
  15. theorem OAI.TracialUltrapower.tendsto_sequenceTwoNorm line 194
  16. theorem OAI.TracialUltrapower.sequenceTwoNorm_nonneg line 208
  17. theorem OAI.TracialUltrapower.sequenceTwoNorm_eq_of_sub_mem line 211
  18. def OAI.TracialUltrapower.quotientTwoNorm line 226
  19. theorem OAI.TracialUltrapower.quotientTwoNorm_mk line 230
  20. theorem OAI.TracialUltrapower.quotientTwoNorm_nonneg line 233
  21. theorem OAI.TracialUltrapower.quotientMap_ballModulus line 240
  22. theorem OAI.TracialUltrapower.quotientTwoNorm_eq_zero_iff line 261
  23. def OAI.TracialUltrapower.traceHilbertMap line 287
  24. theorem OAI.TracialUltrapower.traceHilbertMap_apply line 293
  25. theorem OAI.TracialUltrapower.nullSubmodule_mul_left line 298
  26. theorem OAI.TracialUltrapower.nullSubmodule_mul_right line 308
  27. theorem OAI.TracialUltrapower.nullSubmodule_star line 319
  28. def OAI.TracialUltrapower.nullIdeal line 327
  29. theorem OAI.TracialUltrapower.isClosed_nullIdeal line 334