OAI/RepresentationTheory/VertexAlgebra/ModuleSharpGrowth.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.ColumnGrowth line 12
  2. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.ZeroGrowth line 17
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.columnGrowth_zero line 21
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroGrowth_zero line 26
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.columnGrowth_add line 31
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroGrowth_add line 48
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.columnGrowth_smul line 60
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroGrowth_smul line 68
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.columnGrowth_mono line 76
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroGrowth_mono line 86
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.zeroGrowth_of_columnGrowth line 98
  12. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.SharpDegreeGrowth line 105
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.SharpGrowth line 108
  14. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpGrowthSubmodule line 111
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.finite_columnGrowth_uniform line 117
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointColumnControl_of_columns line 142
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.bothColumnGrowth line 161
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.bothSharpColumnGrowth line 187
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.vacuum_columnGrowth line 199
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.vacuum_sharpGrowth line 210
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_physicalMode line 216
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_columnGrowth line 224
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_zeroGrowth line 251
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_sharpGrowth line 261
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalProduct_degreeGrowth line 281
  26. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpDegreeGrowthSubmodule line 340
  27. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sharpDegreeGrowth_mono line 346
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_sharpDegreeGrowth line 350
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode_translation line 370
  30. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.translation_bothColumnGrowth line 383