OAI/RepresentationTheory/VertexAlgebra/VacuumMemNegative.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.VertexAlgebra.vacuum_mem_negativeFiltration line 16
  2. theorem OAI.StronglyRationalVOA.VertexAlgebra.negative_generator_mode_mem line 22
  3. def OAI.StronglyRationalVOA.VertexAlgebra.translation line 35

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:41 (different declaration text). Qualify references as OAI.StronglyRationalVOA.VertexAlgebra.translation@path.

  4. def OAI.StronglyRationalVOA.VertexAlgebra.c2 line 41

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:46 (different declaration text). Qualify references as OAI.StronglyRationalVOA.VertexAlgebra.c2@path.

  5. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_neg_two_mem_c2 line 45
  6. def OAI.StronglyRationalVOA.VertexAlgebra.C2Cofinite line 49

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:49 (different declaration text). Qualify references as OAI.StronglyRationalVOA.VertexAlgebra.C2Cofinite@path.

  7. def OAI.StronglyRationalVOA.VertexAlgebra.IsIdeal line 52

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:51 (different declaration text). Qualify references as OAI.StronglyRationalVOA.VertexAlgebra.IsIdeal@path.

  8. def OAI.StronglyRationalVOA.VertexAlgebra.IsSimple line 57

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:55 (different declaration text). Qualify references as OAI.StronglyRationalVOA.VertexAlgebra.IsSimple@path.

  9. def OAI.StronglyRationalVOA.ModuleJacobiIdentity line 64

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:63 (different declaration text). Qualify references as OAI.StronglyRationalVOA.ModuleJacobiIdentity@path.

  10. structure OAI.StronglyRationalVOA.WeakModule line 75

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:72 (different declaration text). Qualify references as OAI.StronglyRationalVOA.WeakModule@path.

  11. def OAI.StronglyRationalVOA.WeakModule.IsInvariant line 87

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:85 (different declaration text). Qualify references as OAI.StronglyRationalVOA.WeakModule.IsInvariant@path.

  12. def OAI.StronglyRationalVOA.WeakModule.CompletelyReducible line 91

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:88 (different declaration text). Qualify references as OAI.StronglyRationalVOA.WeakModule.CompletelyReducible@path.

  13. theorem OAI.StronglyRationalVOA.WeakModule.mode_commutator line 97
  14. structure OAI.StronglyRationalVOA.CFTTypeVOA line 116

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:97 (different declaration text). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA@path.

  15. def OAI.StronglyRationalVOA.CFTTypeVOA.virasoroMode line 144

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:126 (different declaration text). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA.virasoroMode@path.

  16. def OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode line 148

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:129 (different declaration text). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode@path.

  17. def OAI.StronglyRationalVOA.CFTTypeVOA.energyShift line 152

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:132 (different declaration text). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA.energyShift@path.

  18. def OAI.StronglyRationalVOA.CFTTypeVOA.IsQuasiPrimary line 155
  19. def OAI.StronglyRationalVOA.CFTTypeVOA.gradingEquiv line 159

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:134 (different declaration text). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA.gradingEquiv@path.

  20. def OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent line 163
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_apply line 168
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_mem line 171
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_of_mem line 174
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_of_mem_ne line 178
  25. def OAI.StronglyRationalVOA.CFTTypeVOA.gradeSupport line 184
  26. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sum_gradeComponents line 189
  27. theorem OAI.StronglyRationalVOA.CFTTypeVOA.homogeneous_induction line 205
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_commutator line 213
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_vacuum line 223
  30. theorem OAI.StronglyRationalVOA.CFTTypeVOA.conformal_eq_virasoro_vacuum line 228
  31. theorem OAI.StronglyRationalVOA.CFTTypeVOA.conformal_quasiPrimary line 233
  32. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_two_conformal line 242
  33. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode_conformal line 255
  34. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_zero_on_grade line 262
  35. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_energy line 266
  36. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_eigenvalue line 282
  37. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mem_grade_of_energy line 292
  38. theorem OAI.StronglyRationalVOA.CFTTypeVOA.eq_zero_of_energy_not_grade line 305
  39. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energy_mode_commutator_general line 315
  40. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energy_mode_commutator line 345
  41. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energy_preserves_c2 line 357
  42. def OAI.StronglyRationalVOA.CFTTypeVOA.c2Energy line 376
  43. theorem OAI.StronglyRationalVOA.CFTTypeVOA.exists_c2_weight_cutoff line 382
  44. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mode_energy_eigenvalue line 406
  45. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mode_mem_grade line 419
  46. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mode_eq_zero_of_negative_energy line 429
  47. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physical_normal_product_resplit line 439
  48. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physical_normal_product_on_grade line 461
  49. def OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousC2 line 495
  50. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_c2Product_mem line 502