OAI/RepresentationTheory/VertexAlgebra/BlockGrowth.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.BlockGrowth line 15
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockGrowth_zero line 19
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockGrowth_add line 24
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockGrowth_smul line 41
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockGrowth_mono_weight line 47
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_blockGrowth line 57
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.finite_blockGrowth_uniform line 86
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalProduct_blockGrowth line 114
  9. def OAI.StronglyRationalVOA.CFTTypeVOA.blockGrowthSubmodule line 161
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.vacuum_blockGrowth line 168
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousC2_le_blockGrowth line 175
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroMode_commutator line 213
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator line 236
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator_apply line 241
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator_eq_sum line 248
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator_eq_sum_reduced line 277
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.selfCommutator_bound line 306
  18. def OAI.StronglyRationalVOA.CFTTypeVOA.generatorMajorant line 359
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.one_le_generatorMajorant line 364
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.root_modeBlock_le_generatorMajorant line 373
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.generator_blockGrowth line 400
  22. structure OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure line 416

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:161 (same statement text; different proof or body). Qualify references as OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure@path.

  23. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.IsHermitian line 436
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.pct_virasoro line 439
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.pct_quasiPrimary line 444
  26. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_adjoint line 451
  27. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mode_norm_sq_difference line 486
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mode_norm_sq_le_adjoint line 499