OAI/RepresentationTheory/VertexAlgebra/Locality.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.locality line 33
  2. lemma OAI.StronglyRationalVOA.ProperCircleArc.disjoint_complement line 63
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryGraphData line 79
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryGraphData_subset line 83
  5. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryAlgebra line 89
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryAlgebra_le_localAlgebra line 92
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryAlgebra_isotone line 95
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryAlgebra_locality line 100
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryAlgebra_interval_locality line 109
  10. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.exists_even_power_difference line 119
  11. def OAI.StronglyRationalVOA.HilbertScale.rotation line 200
  12. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_apply line 203
  13. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_opNorm line 205
  14. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_zero line 207
  15. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_add line 210
  16. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_adjoint line 216
  17. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_norm line 222
  18. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_single line 237
  19. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_continuous line 240
  20. lemma OAI.StronglyRationalVOA.HilbertScale.rotation_graph line 269
  21. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation line 285
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_coordinates line 289
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_zero line 294
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_add line 299
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_norm line 303
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_continuous line 306
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_energy_graph line 308
  28. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_grade line 314
  29. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_core line 318
  30. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_smooth line 324
  31. def OAI.StronglyRationalVOA.SmoothCircleFunction.translate line 341
  32. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_apply line 344
  33. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_real line 346
  34. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_onCircle line 348
  35. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_coefficient line 355
  36. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_physicalMode_grade line 393
  37. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_smearedMap_grade line 407
  38. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_smearedCore_graph line 428
  39. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_closedSmoothField_graph line 452
  40. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_zero line 475
  41. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_add line 478
  42. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_inverse line 489
  43. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_closedSmoothField_graph_iff line 492
  44. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_inner line 502
  45. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_adjoint line 509
  46. lemma OAI.StronglyRationalVOA.ClosedGraphData.coordinate_ext line 521
  47. lemma OAI.StronglyRationalVOA.ClosedGraphData.inclusion_coordinate_sum line 525
  48. lemma OAI.StronglyRationalVOA.ClosedGraphData.projection_commutes_of_entry_commutes line 530