OAI/RepresentationTheory/VertexAlgebra/GeneratorSharpGrowth.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.generator_sharpGrowth line 15
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_sharpMajorant line 53
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_cutoff_sq_of_grades line 93
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.finite_zeroGrowth_uniform line 115
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.norm_of_sharp_square line 140
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.reduced_commutator_coefficient_bound line 152
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator_sharp_bound line 171
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.nonzeroModes_sharp_bound line 217
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.zeroMode_sharpGrowth line 278
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowthSubmodule line 335
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_changeControl line 341
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_improved_zeroGrowth line 358
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positiveColumnNorm_sq_le line 389
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.generator_column_contraction line 403
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeCutoffNorm_le_column line 440
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeCutoffNorm_sq_le line 453
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.generator_quantities_contraction line 468