OAI/RepresentationTheory/VertexAlgebra/ModuleSharpContraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroModeCutoffNorm_le_column line 13
2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroModeCutoffNorm_sq_le line 26
3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.generator_quantities_contraction line 40
4. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.CutoffPowerControl line 89
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffPowerControl_add line 92
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffPowerControl_sum line 105
7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffPowerControl_one line 121
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.sharpMajorant_power_contraction line 128