OAI/RepresentationTheory/VertexAlgebra/ModuleSharpMajorant.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.homogeneousC2_le_sharpDegreeGrowth line 16
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.grade_sharpGrowth line 67
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroModeOnCutoff line 97
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroModeCutoffNorm line 100
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroMode_norm_le line 102
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroModeCutoffNorm_mono line 106
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpColumnQuantity line 115
  8. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpZeroQuantity line 118
  9. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.rawSharpMajorant line 121
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpMajorant line 128
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpColumnQuantity_nonneg line 131
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpZeroQuantity_nonneg line 135
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.one_le_rawSharpMajorant line 139
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.rawSharpMajorant_le line 153
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.one_le_sharpMajorant line 157
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpMajorant_mono line 161
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.root_sharpQuantity_le line 167
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.generator_sharpGrowth line 186
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.exists_sharpMajorant line 216