OAI/Analysis/TraceCone/GNS.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

The GNS representation of an extended trace

The square-integrable ideal carries the seminorm obtained by polarization of x ↦ τ (star x * x). Its Hilbert space completion supports bounded left multiplication by the algebra.

This is the trace representation used in the paper The trace cone classifies Razak–Jacelon stabilizations.

  1. def OAI.TraceConeClassification.ExtendedTrace.finiteSquareLeftMul line 37

    Source documentation

    Left multiplication preserves the actual square-integrable trace ideal.

    def finiteSquareLeftMul (τ : ExtendedTrace A) (a : A)
    (x : τ.finiteSquareAlgebra) : τ.finiteSquareAlgebra :=
…

    Mentions: OAI.TraceConeClassification.ExtendedTrace

  2. lemma OAI.TraceConeClassification.ExtendedTrace.traceSquare_ne_top line 44
  3. def OAI.TraceConeClassification.ExtendedTrace.squareValue line 47
  4. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_nonneg line 50
  5. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_zero line 53
  6. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_smul line 57
  7. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_real_smul line 73
  8. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_three line 78
  9. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_polar_real_nonneg line 107
  10. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_polar_add line 142
  11. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_polar_zero line 147
  12. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_polar_neg line 151
  13. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_polar_real line 157
  14. def OAI.TraceConeClassification.ExtendedTrace.quadraticForm line 166

    Source documentation

    The real quadratic form x ↦ τ(x*x), with finite values on n_τ.

    def quadraticForm : QuadraticForm ℝ τ.finiteSquareAlgebra :=
…
  15. def OAI.TraceConeClassification.ExtendedTrace.realInner line 171

    Source documentation

    Real polarization; its bilinearity follows from the trace identities above.

    def realInner : τ.finiteSquareAlgebra →ₗ[ℝ] τ.finiteSquareAlgebra →ₗ[ℝ] ℝ :=
…
  16. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_eq line 174
  17. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_self line 179
  18. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_symm line 184
  19. lemma OAI.TraceConeClassification.ExtendedTrace.squareValue_I line 188
  20. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_I_I line 193
  21. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_I_left line 198
  22. lemma OAI.TraceConeClassification.ExtendedTrace.realInner_I_self line 203
  23. lemma OAI.TraceConeClassification.ExtendedTrace.complex_smul_parts line 209
  24. def OAI.TraceConeClassification.ExtendedTrace.complexInner line 215

    Source documentation

    Polarization of τ(x*x), with the standard conjugate-linear first convention.

    def complexInner (x y : τ.finiteSquareAlgebra) : ℂ :=
…
  25. lemma OAI.TraceConeClassification.ExtendedTrace.complexInner_symm line 218
  26. lemma OAI.TraceConeClassification.ExtendedTrace.complexInner_self line 223
  27. lemma OAI.TraceConeClassification.ExtendedTrace.complexInner_add_left line 227
  28. lemma OAI.TraceConeClassification.ExtendedTrace.complexInner_smul_left line 234
  29. def OAI.TraceConeClassification.ExtendedTrace.PreTraceGNS line 249

    Source documentation

    Type synonym with the L² seminorm, not the original C*-norm.

    def PreTraceGNS (τ : ExtendedTrace A) : Type u := τ.finiteSquareAlgebra

    Mentions: OAI.TraceConeClassification.ExtendedTrace

  30. instance OAI.TraceConeClassification.ExtendedTrace.(instance at line 251) line 251
  31. instance OAI.TraceConeClassification.ExtendedTrace.(instance at line 252) line 252
  32. def OAI.TraceConeClassification.ExtendedTrace.toPreTraceGNS line 254
  33. def OAI.TraceConeClassification.ExtendedTrace.ofPreTraceGNS line 255
  34. def OAI.TraceConeClassification.ExtendedTrace.preTraceInnerCore line 258
  35. instance OAI.TraceConeClassification.ExtendedTrace.(instance at line 267) line 267
  36. instance OAI.TraceConeClassification.ExtendedTrace.(instance at line 269) line 269
  37. lemma OAI.TraceConeClassification.ExtendedTrace.preTraceGNS_inner line 273
  38. lemma OAI.TraceConeClassification.ExtendedTrace.preTraceGNS_norm_sq line 276
  39. abbrev OAI.TraceConeClassification.ExtendedTrace.TraceGNS line 281
  40. lemma OAI.TraceConeClassification.ExtendedTrace.finiteSquareLeftMul_val line 283
  41. def OAI.TraceConeClassification.ExtendedTrace.finiteSquareLeftMulLinear line 286
  42. lemma OAI.TraceConeClassification.ExtendedTrace.leftMul_squareValue_le line 291
  43. lemma OAI.TraceConeClassification.ExtendedTrace.leftMul_realInner line 304
  44. lemma OAI.TraceConeClassification.ExtendedTrace.leftMul_complexInner line 335
  45. def OAI.TraceConeClassification.ExtendedTrace.leftMulPreTrace line 345

    Source documentation

    Bounded left multiplication with the L² norm, proved from positivity.

    def leftMulPreTrace (a : A) : τ.PreTraceGNS →L[ℂ] τ.PreTraceGNS :=
…
  46. lemma OAI.TraceConeClassification.ExtendedTrace.leftMulPreTrace_apply line 352
  47. lemma OAI.TraceConeClassification.ExtendedTrace.leftMulPreTrace_mul line 355
  48. lemma OAI.TraceConeClassification.ExtendedTrace.leftMulPreTrace_inner line 363
  49. def OAI.TraceConeClassification.ExtendedTrace.traceGNSRep line 369
  50. def OAI.TraceConeClassification.ExtendedTrace.traceGNSLambda line 423
  51. lemma OAI.TraceConeClassification.ExtendedTrace.traceGNSLambda_dense line 430
  52. lemma OAI.TraceConeClassification.ExtendedTrace.traceGNSLambda_norm_sq line 442
  53. lemma OAI.TraceConeClassification.ExtendedTrace.traceGNSRep_covariance line 448
  54. theorem OAI.TraceConeClassification.ExtendedTrace.trace_gns_exists line 454