OAI/RepresentationTheory/VertexAlgebra/ModuleBands.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.StronglyRationalVOA.EnergyBand line 10
2. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.bandGrade line 15
3. instance OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.bandGradeFinite line 16
4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.mode_mem_band line 18
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.physicalMode_mem_band line 28
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.virasoro_mem_band line 33
7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyShift_on_band line 38
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyShift_pow_on_band line 44
9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.physical_normal_product_resplit line 54
10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.physicalMode_eq_zero_above_band line 78
11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.physical_normal_product_on_band line 86