OAI/RepresentationTheory/VertexAlgebra/MinimalComparator.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StronglyRationalVOA.HilbertCore._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space line 11

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

2. def OAI.StronglyRationalVOA.HilbertCore._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.equiv line 15

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

3. def OAI.StronglyRationalVOA.HilbertCore._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.operator line 20

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

4. def OAI.StronglyRationalVOA.SmoothCircleFunction._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.coefficient line 30

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

5. abbrev OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double line 43

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

6. def OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.graph line 45

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

7. def OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.projection line 48

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

8. def OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.inclusion line 56

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

9. def OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.coordinate line 60

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

10. def OAI.StronglyRationalVOA.ClosedGraphData._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.entry line 64

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

11. def OAI.StronglyRationalVOA.LocalOperatorAlgebra._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.LocalOperatorAlgebra.generated line 75

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

12. def OAI.StronglyRationalVOA.SmoothCircleFunction._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.onCircle line 90

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

13. def OAI.StronglyRationalVOA.ProperCircleArc._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier line 99

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

14. def OAI.StronglyRationalVOA.ProperCircleArc._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.complement line 102

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

15. def OAI.StronglyRationalVOA.BoundedFlow._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.BoundedFlow.flow line 121

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

16. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity line 128

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

17. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose line 134

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

18. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.inverse line 140

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

19. instance OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.instGroup line 149

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

20. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle line 181

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

21. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleHomeomorph line 194

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

22. def OAI.StronglyRationalVOA.SmoothCircleLift._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction line 219

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

23. def OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism line 239

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

24. instance OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.instGroupSmoothCircleDiffeomorphism line 241

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

25. instance OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.instTopologicalSpaceSmoothCircleDiffeomorphism line 250

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

26. def OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel line 259

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

27. def OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements line 263

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

28. def OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts line 265

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

29. def OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.rotationMatrix line 314

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

30. abbrev OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Group line 323

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

31. def OAI.StronglyRationalVOA.CircleMobiusGeometry._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.inclusion line 325

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

32. def OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism.action line 337

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

33. def OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.projectiveConjugation line 347

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

34. def OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.globalObservableAlgebra line 370

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

35. def OAI.StronglyRationalVOA._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.globalCyclicSpace line 375

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

36. def OAI.MinimalVertex.smearedMap line 388

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

37. def OAI.MinimalVertex.smoothSmearedField line 398

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

38. def OAI.MinimalVertex.closedSmoothField line 407

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

39. def OAI.MinimalVertex.localGraphData line 411

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

40. def OAI.MinimalVertex.localAlgebra line 417

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

41. def OAI.MinimalVertex.intervalAlgebra line 421

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

42. def OAI.MinimalVertex.CKLWStrongLocal line 425

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

43. def OAI.MinimalVertex.resolvent line 438

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

44. def OAI.MinimalVertex.boundedGenerator line 444

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

45. def OAI.MinimalVertex.approximatingFlow line 450

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

46. def OAI.MinimalVertex.flow line 461

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

47. def OAI.MinimalVertex.projectiveStandardAction line 469

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

48. structure OAI.MinimalVertex.IrreducibleConformalNetStructure line 477

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

49. theorem OAI.MinimalVertex.cloned_entry_eq line 519
50. theorem OAI.MinimalVertex.smearedMap_eq line 528
51. theorem OAI.MinimalVertex.smoothSmearedField_eq line 538
52. theorem OAI.MinimalVertex.closedSmoothField_eq line 544
53. theorem OAI.MinimalVertex.localGraphData_eq line 550
54. theorem OAI.MinimalVertex.intervalAlgebra_eq line 565
55. theorem OAI.MinimalVertex.CKLWStrongLocal_eq line 573
56. theorem OAI.MinimalVertex.resolvent_eq line 583
57. theorem OAI.MinimalVertex.boundedGenerator_eq line 593
58. theorem OAI.MinimalVertex.approximatingFlow_eq line 599
59. theorem OAI.MinimalVertex.flow_eq line 607
60. theorem OAI.MinimalVertex.projectiveStandardAction_eq line 623
61. theorem OAI.MinimalVertex.netStructure_of_original line 641
62. theorem OAI.MinimalVertex.main line 676

    Distinct definitions of this name: ComparatorChallenges/VertexAlgebraNet.lean:822 (different declaration text). Qualify references as OAI.MinimalVertex.main@path.