OAI/RepresentationTheory/VertexAlgebra/FiniteSums.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.finite_sum_power_contraction line 19
  2. theorem OAI.StronglyRationalVOA.finite_weighted_poly_uniform line 69
  3. theorem OAI.StronglyRationalVOA.finsum_nat_split line 103
  4. abbrev OAI.StronglyRationalVOA.StateField line 135

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:11 (different declaration text). Qualify references as OAI.StronglyRationalVOA.StateField@path.

  5. def OAI.StronglyRationalVOA.mode line 140

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:15 (different declaration text). Qualify references as OAI.StronglyRationalVOA.mode@path.

  6. theorem OAI.StronglyRationalVOA.mode_zero line 145
  7. theorem OAI.StronglyRationalVOA.mode_add line 150
  8. theorem OAI.StronglyRationalVOA.mode_smul line 156
  9. theorem OAI.StronglyRationalVOA.mode_lower_truncation line 163
  10. theorem OAI.StronglyRationalVOA.mode_shift_hasFiniteSupport line 173
  11. def OAI.StronglyRationalVOA.JacobiIdentity line 187

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:19 (different declaration text). Qualify references as OAI.StronglyRationalVOA.JacobiIdentity@path.

  12. structure OAI.StronglyRationalVOA.VertexAlgebra line 196

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

  13. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_commutator line 210
  14. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_commutator_nat line 227
  15. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_iterate line 244
  16. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_normal_product line 262
  17. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_normal_product_hasFiniteSupport line 287
  18. theorem OAI.StronglyRationalVOA.VertexAlgebra.mode_normal_product_resplit line 309
  19. inductive OAI.StronglyRationalVOA.VertexAlgebra.ModeWord line 376
  20. def OAI.StronglyRationalVOA.VertexAlgebra.generatorFiltration line 382
  21. theorem OAI.StronglyRationalVOA.VertexAlgebra.generatorFiltration_mono line 385
  22. theorem OAI.StronglyRationalVOA.VertexAlgebra.modeWord_mem_generatorFiltration line 391
  23. theorem OAI.StronglyRationalVOA.VertexAlgebra.vacuum_mem_generatorFiltration line 395
  24. theorem OAI.StronglyRationalVOA.VertexAlgebra.generator_mode_mem line 401
  25. theorem OAI.StronglyRationalVOA.VertexAlgebra.modeWord_mode_mem line 414
  26. theorem OAI.StronglyRationalVOA.VertexAlgebra.generatorFiltration_mode_mem line 438
  27. inductive OAI.StronglyRationalVOA.VertexAlgebra.NegativeWord line 454
  28. def OAI.StronglyRationalVOA.VertexAlgebra.negativeFiltration line 460
  29. theorem OAI.StronglyRationalVOA.VertexAlgebra.negativeFiltration_mono line 463
  30. theorem OAI.StronglyRationalVOA.VertexAlgebra.NegativeWord.modeWord line 469
  31. theorem OAI.StronglyRationalVOA.VertexAlgebra.NegativeWord.weight_le line 475
  32. theorem OAI.StronglyRationalVOA.VertexAlgebra.negativeWord_mem_negativeFiltration line 481
  33. theorem OAI.StronglyRationalVOA.VertexAlgebra.negativeFiltration_le line 485