OAI/RepresentationTheory/VertexAlgebra/LoweringNormSq.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.lowering_norm_sq_of_commutator line 18
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.raising_norm_sq_of_commutator line 75
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_adjoint line 92
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grades_orthogonal line 101
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.centralCharge_eq line 112
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.centralCharge_nonneg line 122
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_orthogonalFamily line 132
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.norm_sq_eq_sum_grades line 138
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energy_norm_sq_eq_sum_grades line 147
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_norm_sq_identity line 162
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_norm_sq_le_adjoint line 178
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_positive_norm_sq line 190
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_negative_norm_sq line 246
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_level_coefficient_le line 273
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.virasoro_norm_on_grade line 293
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mode_images_orthogonal line 334
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mode_norm_sq_eq_sum_grades line 350
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.zeroMode_norm_sq_of_commutator line 376
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modeBlock_norm_sq_bound line 448