OAI/RepresentationTheory/VertexAlgebra/AdjointMass.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Vertex algebra, energy bounds and closed smeared-field operators.

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointMass line 17
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointMass_nonneg line 20
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointColumnControl_of_columns line 22
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.bothColumnGrowth line 41
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.bothSharpColumnGrowth line 67
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.vacuum_columnGrowth line 82
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.vacuum_sharpGrowth line 93
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_physicalMode line 99
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_columnGrowth line 107
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_zeroGrowth line 134
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_sharpGrowth line 150
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalProduct_degreeGrowth line 170
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpDegreeGrowthSubmodule line 235
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sharpDegreeGrowth_mono line 241
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_sharpDegreeGrowth line 245
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode_translation line 265
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.translation_bothColumnGrowth line 278
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.homogeneousC2_le_sharpDegreeGrowth line 347
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_sharpGrowth line 398
  20. def OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeOnCutoff line 434
  21. def OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeCutoffNorm line 437
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroMode_norm_le line 439
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeCutoffNorm_mono line 443
  24. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpColumnQuantity line 452
  25. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpZeroQuantity line 455
  26. def OAI.StronglyRationalVOA.CFTTypeVOA.rawSharpMajorant line 458
  27. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpMajorant line 465
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sharpColumnQuantity_nonneg line 468
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sharpZeroQuantity_nonneg line 472
  30. theorem OAI.StronglyRationalVOA.CFTTypeVOA.one_le_rawSharpMajorant line 476
  31. theorem OAI.StronglyRationalVOA.CFTTypeVOA.rawSharpMajorant_le line 490
  32. theorem OAI.StronglyRationalVOA.CFTTypeVOA.one_le_sharpMajorant line 494
  33. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sharpMajorant_mono line 498
  34. theorem OAI.StronglyRationalVOA.CFTTypeVOA.root_sharpQuantity_le line 504