OAI/RepresentationTheory/VertexAlgebra/ModuleSmearedFields.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.PolynomialEnergyBound.physical line 13
2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.summable_norm_physicalSmear line 33
3. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.smearedMap line 44
4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.smearedMap_apply line 51
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.summable_adjointPhysicalSmear line 60
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.smearedCore_closable line 83
7. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.closedSmearedOperator line 102
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.closedSmearedOperator_isClosed line 107
9. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.smoothSmearedField line 114
10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.smoothSmearedField_closable line 119
11. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.closedSmoothField line 125
12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.closedSmoothField_isClosed line 129