OAI/RepresentationTheory/VertexAlgebra/ModulePositiveEnergy.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.lowering_ne_zeroline 15 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.weight_nonnegline 26 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.grade_eq_bot_of_negativeline 50 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.grade_eq_bot_of_nonrealline 57 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.physicalMode_eq_zero_of_negativeline 65