OAI/RepresentationTheory/VertexAlgebra/RotationConjugateCommutant.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_conjugate_commutant line 38
2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.intervalAlgebra_rotation_mem line 67
3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_fixed_scalar line 92
4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.interval_invariant_subspace line 110
5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conformalHamiltonian_nonnegative line 138
6. lemma OAI.StronglyRationalVOA.ProperCircleArc.translate_add line 154
7. lemma OAI.StronglyRationalVOA.ProperCircleArc.translate_zero line 158
8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.intervalAlgebra_rotation_mem_iff line 165
9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_two_pi line 178
10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_periodic line 192
11. structure OAI.StronglyRationalVOA.SmoothCircleLift line 201

    Also declared: ComparatorChallenges/VertexAlgebraNet.lean:346 (same declaration text).

12. instance OAI.StronglyRationalVOA.SmoothCircleLift.(instance at line 207) line 207
13. lemma OAI.StronglyRationalVOA.SmoothCircleLift.ext line 208
14. def OAI.StronglyRationalVOA.SmoothCircleLift.identity line 216
15. def OAI.StronglyRationalVOA.SmoothCircleLift.compose line 221
16. def OAI.StronglyRationalVOA.SmoothCircleLift.inverse line 226
17. instance OAI.StronglyRationalVOA.SmoothCircleLift.(instance at line 234) line 234
18. lemma OAI.StronglyRationalVOA.SmoothCircleLift.one_apply line 242
19. lemma OAI.StronglyRationalVOA.SmoothCircleLift.mul_apply line 243
20. lemma OAI.StronglyRationalVOA.SmoothCircleLift.inv_apply_apply line 244
21. lemma OAI.StronglyRationalVOA.SmoothCircleLift.apply_inv_apply line 245
22. def OAI.StronglyRationalVOA.SmoothCircleLift.rotation line 247
23. lemma OAI.StronglyRationalVOA.SmoothCircleLift.rotation_apply line 254
24. lemma OAI.StronglyRationalVOA.SmoothCircleLift.rotation_zero line 255
25. lemma OAI.StronglyRationalVOA.SmoothCircleLift.rotation_add line 256
26. lemma OAI.StronglyRationalVOA.SmoothCircleLift.circle_periodic line 257
27. def OAI.StronglyRationalVOA.SmoothCircleLift.onCircle line 264
28. lemma OAI.StronglyRationalVOA.SmoothCircleLift.onCircle_coe line 265
29. lemma OAI.StronglyRationalVOA.SmoothCircleLift.onCircle_mul line 266
30. lemma OAI.StronglyRationalVOA.SmoothCircleLift.onCircle_one line 270
31. lemma OAI.StronglyRationalVOA.SmoothCircleLift.onCircle_inverse line 273
32. lemma OAI.StronglyRationalVOA.SmoothCircleLift.differentiable line 275
33. lemma OAI.StronglyRationalVOA.SmoothCircleLift.derivative_positive line 277
34. lemma OAI.StronglyRationalVOA.SmoothCircleLift.continuous_onCircle line 285
35. def OAI.StronglyRationalVOA.SmoothCircleLift.circleHomeomorph line 288
36. lemma OAI.StronglyRationalVOA.SmoothCircleLift.shift_periodic line 296
37. lemma OAI.StronglyRationalVOA.SmoothCircleLift.integer_shift line 301
38. lemma OAI.StronglyRationalVOA.SmoothCircleLift.deck_central line 306
39. lemma OAI.StronglyRationalVOA.SmoothCircleLift.deck_onCircle line 310
40. lemma OAI.StronglyRationalVOA.SmoothCircleLift.onCircle_eq_iff line 320
41. def OAI.StronglyRationalVOA.SmoothCircleLift.circleAction line 344
42. lemma OAI.StronglyRationalVOA.SmoothCircleLift.circleAction_kernel line 348
43. def OAI.StronglyRationalVOA.SmoothCircleDiffeomorphism line 366
44. instance OAI.StronglyRationalVOA.(instance at line 367) line 367
45. def OAI.StronglyRationalVOA.SmoothCircleLift.unitParameter line 375
46. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitParameter_smooth line 376
47. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitParameter_derivative line 378
48. def OAI.StronglyRationalVOA.SmoothCircleLift.unitLift line 383
49. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitLift_apply line 391
50. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitLift_inverse_one line 392
51. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitLift_density_one line 398
52. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismImplementer line 412
53. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_primary_closed_covariance line 415
54. lemma OAI.StronglyRationalVOA.SmoothCircleLift.derivative_periodic line 427
55. lemma OAI.StronglyRationalVOA.SmoothCircleLift.derivative_mul line 432
56. def OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity line 436
57. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_smooth line 438
58. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_periodic line 442
59. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_pos line 447
60. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_one line 450
61. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_mul line 456
62. lemma OAI.StronglyRationalVOA.SmoothCircleLift.pushDensity_inverse line 462
63. def OAI.StronglyRationalVOA.SmoothCircleLift.unitTest line 471
64. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitTest_smooth line 472
65. lemma OAI.StronglyRationalVOA.SmoothCircleLift.unitTest_periodic line 474
66. def OAI.StronglyRationalVOA.SmoothCircleLift.pushedTest line 478
67. lemma OAI.StronglyRationalVOA.SmoothCircleLift.angularTest_zero line 480
68. lemma OAI.StronglyRationalVOA.SmoothCircleLift.angularTest_one line 488
69. def OAI.StronglyRationalVOA.SmoothCircleLift.anomaly line 493
70. lemma OAI.StronglyRationalVOA.SmoothCircleLift.anomaly_endpoint line 496
71. lemma OAI.StronglyRationalVOA.SmoothCircleLift.anomaly_mul line 509
72. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphismSmoothImplementer line 518
73. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.diffeomorphism_primary_smooth line 521