OAI/RepresentationTheory/VertexAlgebra/EnergyCutoff.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.energyCutoff line 15
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.grade_le_energyCutoff line 21
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.exists_energyCutoff line 25
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.cutoffProjection line 34
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.cutoffProjection_apply line 37
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.cutoffProjection_of_mem line 41
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyShift_pow_norm_on_cutoff line 63
  8. def OAI.StronglyRationalVOA.CFTTypeVOA.mobiusGenerator line 85
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mobiusGenerator_mem_energyCutoff line 88
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mobiusGenerator_pow_mem_energyCutoff line 109
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusGenerator_skew line 123
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusGenerator_norm_cutoff line 131
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusGenerator_pow_norm line 154
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_mobiusEvolutionTerm line 173
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusEvolution_inner line 183
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLocalIsometry line 192
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_one_physical_commutator line 205
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_neg_one_physical_commutator line 234
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mobius_physical_commutator line 256
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_polynomial_cutoff line 277
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_diagonal_zero line 291
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mobius_commutator_power line 306
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobius_commutator_diagonal line 334
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energyCutoff_mono line 354
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.mobiusTaylor_mem_energyCutoff line 359
  26. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_mobiusInserted line 374
  27. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobius_diagonal_compression line 390
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusInserted_bound line 413
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.zeroMode_transfer line 466