OAI/RepresentationTheory/VertexAlgebra/ModuleEnergyMain.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.linearCurrentBoundSubmoduleline 16 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.weight_one_quasiPrimaryline 54 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.weight_one_linear_energyBoundline 69 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.virasoro_linear_energyBoundline 83 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.source_energy_theoremline 94