OAI/RepresentationTheory/VertexAlgebra/GraphCommutants.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Vertex algebra, energy bounds and closed smeared-field operators.

  1. theorem OAI.StronglyRationalVOA.ClosedGraphData.entry_commutes_of_graph_invariant line 18
  2. def OAI.StronglyRationalVOA.LocalOperatorAlgebra.generated line 53
  3. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.subset_generated line 62
  4. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.generated_mono line 67
  5. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.generated_le line 71
  6. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.coe_generated_commutant line 81
  7. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.generated_le_commutant_iff line 91
  8. def OAI.StronglyRationalVOA.SmoothCircleFunction.onCircle line 116
  9. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.onCircle_coe line 120
  10. structure OAI.StronglyRationalVOA.ProperCircleArc line 127

    Also declared: ComparatorChallenges/VertexAlgebraNet.lean:305 (same declaration text).

  11. def OAI.StronglyRationalVOA.ProperCircleArc.carrier line 135
  12. def OAI.StronglyRationalVOA.ProperCircleArc.complement line 139
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localGraphData line 154
  14. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localAlgebra line 163
  15. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.intervalAlgebra line 167
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.CKLWStrongLocal line 173
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localAlgebra_isotone line 178
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_graphData_mem line 187
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.CKLWStrongLocal_iff_graphData line 196
  20. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.gradeEmbedding line 220
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.completed_grades_orthogonal line 224
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.completed_isHilbertSum line 235
  23. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyCoordinates line 252
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyCoordinates_grade line 256
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyCoordinates_coe line 264
  26. abbrev OAI.StronglyRationalVOA.HilbertScale.Space line 291
  27. def OAI.StronglyRationalVOA.HilbertScale.domain line 294
  28. def OAI.StronglyRationalVOA.HilbertScale.diagonal line 313
  29. theorem OAI.StronglyRationalVOA.HilbertScale.diagonal_apply line 324
  30. theorem OAI.StronglyRationalVOA.HilbertScale.mem_graph_iff line 327
  31. theorem OAI.StronglyRationalVOA.HilbertScale.diagonal_closed line 345
  32. theorem OAI.StronglyRationalVOA.HilbertScale.single_mem_domain line 358
  33. theorem OAI.StronglyRationalVOA.HilbertScale.diagonal_single line 368
  34. theorem OAI.StronglyRationalVOA.HilbertScale.domain_dense line 374
  35. theorem OAI.StronglyRationalVOA.HilbertScale.diagonal_formalAdjoint line 386
  36. theorem OAI.StronglyRationalVOA.HilbertScale.adjoint_coordinate line 395
  37. theorem OAI.StronglyRationalVOA.HilbertScale.adjoint_le_diagonal line 410
  38. theorem OAI.StronglyRationalVOA.HilbertScale.adjoint_diagonal line 423
  39. def OAI.StronglyRationalVOA.HilbertScale.finiteCore line 431
  40. theorem OAI.StronglyRationalVOA.HilbertScale.single_mem_finiteCore line 435
  41. theorem OAI.StronglyRationalVOA.HilbertScale.finiteCore_le_domain line 440
  42. theorem OAI.StronglyRationalVOA.HilbertScale.diagonal_hasCore line 448
  43. theorem OAI.StronglyRationalVOA.HilbertScale.real_diagonal_selfAdjoint line 477
  44. def OAI.StronglyRationalVOA.OperatorTransport.transport line 491
  45. theorem OAI.StronglyRationalVOA.OperatorTransport.mem_graph_iff line 507