OAI/RepresentationTheory/VertexAlgebra/HilbertCore.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.HilbertCore.space line 16
  2. def OAI.StronglyRationalVOA.HilbertCore.equiv line 20
  3. theorem OAI.StronglyRationalVOA.HilbertCore.equiv_coe line 25
  4. theorem OAI.StronglyRationalVOA.HilbertCore.equiv_symm_coe line 26
  5. theorem OAI.StronglyRationalVOA.HilbertCore.dense line 30
  6. def OAI.StronglyRationalVOA.HilbertCore.operator line 35
  7. theorem OAI.StronglyRationalVOA.HilbertCore.operator_apply line 39
  8. theorem OAI.StronglyRationalVOA.HilbertCore.formalAdjoint line 42
  9. theorem OAI.StronglyRationalVOA.HilbertCore.closable line 53
  10. def OAI.StronglyRationalVOA.RapidCoefficients line 63

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

  11. theorem OAI.StronglyRationalVOA.RapidCoefficients.conj line 69
  12. theorem OAI.StronglyRationalVOA.RapidCoefficients.neg_index line 73
  13. theorem OAI.StronglyRationalVOA.RapidCoefficients.add line 78
  14. theorem OAI.StronglyRationalVOA.RapidCoefficients.smul line 87
  15. theorem OAI.StronglyRationalVOA.RapidCoefficients.summable_norm_smul line 91
  16. def OAI.StronglyRationalVOA.SummableLinearFamily.tsumMap line 110

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

  17. theorem OAI.StronglyRationalVOA.SummableLinearFamily.adjoint_tsum line 120
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.PolynomialEnergyBound.physical line 139
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.summable_norm_physicalSmear line 157
  20. def OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap line 168
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_apply line 175
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_adjointPhysicalSmear line 184
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedCore_closable line 207
  24. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmearedOperator line 226
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmearedOperator_isClosed line 231
  26. structure OAI.StronglyRationalVOA.SmoothCircleFunction line 243

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

  27. instance OAI.StronglyRationalVOA.SmoothCircleFunction.(instance at line 249) line 249
  28. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.period_pos line 251
  29. def OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient line 253
  30. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.periodic_iteratedDeriv line 256
  31. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.continuous_iteratedDeriv line 264
  32. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.differentiable_iteratedDeriv line 267
  33. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_deriv_step line 272
  34. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_iteratedDeriv line 290
  35. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_norm_le line 301
  36. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_polynomial_decay line 320
  37. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.rapid_coefficients line 336
  38. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmearedField line 380
  39. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmearedField_closable line 385
  40. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField line 391
  41. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_isClosed line 395
  42. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_graph line 400
  43. abbrev OAI.StronglyRationalVOA.ClosedGraphData.Double line 414
  44. def OAI.StronglyRationalVOA.ClosedGraphData.graph line 417
  45. theorem OAI.StronglyRationalVOA.ClosedGraphData.graph_closed line 421
  46. def OAI.StronglyRationalVOA.ClosedGraphData.projection line 427
  47. def OAI.StronglyRationalVOA.ClosedGraphData.inclusion line 431
  48. def OAI.StronglyRationalVOA.ClosedGraphData.coordinate line 435
  49. def OAI.StronglyRationalVOA.ClosedGraphData.entry line 440
  50. theorem OAI.StronglyRationalVOA.ClosedGraphData.projection_selfAdjoint line 443
  51. theorem OAI.StronglyRationalVOA.ClosedGraphData.coordinate_eq_adjoint line 448
  52. theorem OAI.StronglyRationalVOA.ClosedGraphData.adjoint_inclusion line 454
  53. theorem OAI.StronglyRationalVOA.ClosedGraphData.adjoint_coordinate line 457
  54. theorem OAI.StronglyRationalVOA.ClosedGraphData.star_entry line 461
  55. def OAI.StronglyRationalVOA.ClosedGraphData.diagonalAction line 469
  56. theorem OAI.StronglyRationalVOA.ClosedGraphData.diagonalAction_adj line 473
  57. theorem OAI.StronglyRationalVOA.ClosedGraphData.coordinate_diagonalAction line 484
  58. theorem OAI.StronglyRationalVOA.ClosedGraphData.diagonalAction_inclusion line 490
  59. theorem OAI.StronglyRationalVOA.ClosedGraphData.commutes_projection_of_reduces line 497