OAI/RepresentationTheory/VertexAlgebra/ObservableScalars.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.smul line 38
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.add line 46
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localState_zero line 57
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localStateSpace line 60
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.translation_mem_grade line 65
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.negative_mode line 69
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.virasoro_negative line 93
  8. lemma OAI.StronglyRationalVOA.ProperCircleArc.isOpen_carrier line 112
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_le_localStateSpace line 120
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.all_state_localState line 146
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.all_state_entry_mem line 149
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localAlgebra_eq_primaryAlgebra line 161
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localAlgebra_locality line 168
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.cklwStrongLocal line 175
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hamiltonian_kernel line 185
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_graph_le_hamiltonian line 209
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.local_commutant_preserves_graph line 234
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_core_graph line 249
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_character line 256
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.global_commutant_vacuum line 268
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.global_commutant_scalar line 279
  22. lemma OAI.StronglyRationalVOA.ProperCircleArc.exists_mem line 310
  23. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.finite_arc_cutoffs line 319
  24. def OAI.StronglyRationalVOA.SmoothCircleFunction.sumTests line 342
  25. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.sumTests_apply line 346
  26. def OAI.StronglyRationalVOA.SmoothCircleFunction.reciprocal line 348
  27. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.reciprocal_apply line 352
  28. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.finite_arc_partition line 354
  29. def OAI.StronglyRationalVOA.ProperCircleArc.translate line 411
  30. lemma OAI.StronglyRationalVOA.ProperCircleArc.translate_contains line 413
  31. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_sumTests line 424
  32. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.finite_test_graph_invariant line 439
  33. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_interval_graph line 462
  34. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.interval_commutant_all_graphs line 480
  35. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.interval_commutant_scalar line 503
  36. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_vacuum line 531
  37. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_conjugate_graph line 534