OAI/RepresentationTheory/VertexAlgebra/DiffeomorphismStressSmooth.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_stress_smooth line 38
  2. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushedTest_mul line 57
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismDefect line 68
  4. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismSmoothDefect line 72
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_primary line 76
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_positive_stress line 107
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_stress line 150
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_primary_test line 177
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_test line 189
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismSmoothDefect_coe line 214
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismSmoothDefect_symm_coe line 217
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_closed line 221
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_defect_scalar line 240
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.scalarUnitary_norm line 273
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_projective_mul line 283
  16. def OAI.StronglyRationalVOA.scalarPhaseSubgroup line 300

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

  17. instance OAI.StronglyRationalVOA.scalarPhaseSubgroup_normal line 318

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

  18. abbrev OAI.StronglyRationalVOA.ProjectiveUnitaryGroup line 328

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

  19. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.liftProjectiveRepresentation line 335
  20. lemma OAI.StronglyRationalVOA.SmoothCircleLift.rotation_inv line 353
  21. lemma OAI.StronglyRationalVOA.SmoothCircleLift.derivative_rotation line 356
  22. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_deck line 358
  23. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushedTest_deck line 365
  24. lemma OAI.StronglyRationalVOA.SmoothCircleLift.anomaly_deck line 370
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positiveStress_commutation_extend line 377
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_deck_primary line 405
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_deck_stress line 420
  28. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_deck_test line 438
  29. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_deck_closed line 460
  30. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_deck_scalar line 479
  31. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismProjectiveRepresentation line 508
  32. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_normalized_path_difference line 527