OAI/RepresentationTheory/VertexAlgebra/VirasoroLinearEnergy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_linear_energy line 19
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conformal_energyBound line 48
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physical_normal_product line 73
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normal_product_quadratic line 89
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normal_product_norms_hasFiniteSupport line 131
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positive_column line 155
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normal_product_nonneg line 178
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalProductTrace_nonneg line 186
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positive_column_le_grade_trace line 198
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalProductTrace_summable_of_onePoint line 215
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positive_column_le_weighted_trace line 226
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.pct_mem_grade line 240
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hermitianConjugation line 248
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hermitianConjugation_involutive line 251
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_hermitian_quasiPrimary_spanning line 260
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.quasiPrimary_decomposition line 310
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_blockGrowth line 335
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_generatorMajorant line 363
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.generatorMajorant_polynomial line 399
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyBound_of_polynomial_blocks line 489