OAI/RepresentationTheory/VertexAlgebra/GradeComponentC.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_c2_mem line 16
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousC2_eq line 30
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.negativeWord_mem_grade line 42
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousNegativeFiltration line 54
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.gradeComponent_negativeFiltration_mem line 59
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousNegativeFiltration_eq line 79
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.generatorFiltration_le_negativeFiltration line 92
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.generatorFiltration_eq_negativeFiltration line 151
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_mem_grade line 159
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_eq_zero_of_lt line 165
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_neg_one_eq_translation line 172
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.translation_mem_generatorFiltration line 178
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.homogeneousC2_le_generatorFiltration line 186
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energyShift_on_grade line 197
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energyShift_pow_on_grade line 203
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.IsPrimary line 214
  17. inductive OAI.StronglyRationalVOA.CFTTypeVOA.PrimaryDescendant line 218
  18. def OAI.StronglyRationalVOA.CFTTypeVOA.primaryDescendantSpan line 225
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.PrimaryDescendant.mem_grade line 228
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.primary_mem_primaryDescendantSpan line 234
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_mem_primaryDescendantSpan line 238
  22. def OAI.StronglyRationalVOA.CFTTypeVOA.lowerVirasoroSpace line 250
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.lowerVirasoroSpace_le_grade line 253
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_mem_lowerVirasoroSpace line 259
  25. def OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeOnGrade line 271
  26. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroModeOnGrade_apply line 277
  27. def OAI.StronglyRationalVOA.CFTTypeVOA.gradedTraceCoefficient line 283
  28. def OAI.StronglyRationalVOA.CFTTypeVOA.OrdinaryOnePointConvergence line 288
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalProduct_mem_grade line 293
  30. def OAI.StronglyRationalVOA.CFTTypeVOA.normalProductOnGrade line 298
  31. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalProductOnGrade_apply line 302
  32. def OAI.StronglyRationalVOA.CFTTypeVOA.normalProductTrace line 311
  33. def OAI.StronglyRationalVOA.CFTTypeVOA.IsAdmissible line 316

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

  34. def OAI.StronglyRationalVOA.CFTTypeVOA.IsRational line 325

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

  35. theorem OAI.StronglyRationalVOA.re_trace_nonneg_of_quadratic line 336
  36. theorem OAI.StronglyRationalVOA.quadratic_le_re_trace line 353
  37. def OAI.StronglyRationalVOA.CFTTypeVOA.PolynomialEnergyBound line 386

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

  38. def OAI.StronglyRationalVOA.CFTTypeVOA.PolynomialEnergyBounds line 392

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

  39. theorem OAI.StronglyRationalVOA.CFTTypeVOA.vacuum_energyBound line 396
  40. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energyShift_pow_norm_on_grade line 404
  41. def OAI.StronglyRationalVOA.CFTTypeVOA.modeBlock line 413
  42. theorem OAI.StronglyRationalVOA.CFTTypeVOA.modeBlock_apply line 419
  43. def OAI.StronglyRationalVOA.CFTTypeVOA.BlockControl line 424
  44. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockControl_mono line 428
  45. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockControl_zero line 433
  46. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockControl_add line 437
  47. theorem OAI.StronglyRationalVOA.CFTTypeVOA.blockControl_smul line 445
  48. def OAI.StronglyRationalVOA.CFTTypeVOA.correctionMass line 455
  49. theorem OAI.StronglyRationalVOA.CFTTypeVOA.correctionMass_nonneg line 458
  50. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalProduct_blockControl line 464