OAI/RepresentationTheory/VertexAlgebra/CoefficientDifferentiated.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_differentiated line 15
  2. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.differentiated_support line 33
  3. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.differentiated_mul_zero line 43
  4. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_weighted_convolution_zero line 54
  5. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_polynomial_convolution_zero line 74
  6. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_choose_convolution_zero line 93
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode_energy_eigenvalue line 117
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode_commutator_finite line 128
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_cross_orthogonal line 152
  10. theorem OAI.StronglyRationalVOA.summable_inner_diagonal line 179
  11. theorem OAI.StronglyRationalVOA.inner_tsum_diagonal line 192
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_smeared_inner_homogeneous line 214
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_smeared_commutator_zero line 253
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_weak_commutation line 289
  15. def OAI.StronglyRationalVOA.ClosedGraphData.doubleUnitary line 353
  16. theorem OAI.StronglyRationalVOA.ClosedGraphData.doubleUnitary_apply line 357
  17. theorem OAI.StronglyRationalVOA.ClosedGraphData.doubleUnitary_symm_apply line 361
  18. theorem OAI.StronglyRationalVOA.ClosedGraphData.mem_graph_transport line 365
  19. theorem OAI.StronglyRationalVOA.ClosedGraphData.projection_transport line 371
  20. theorem OAI.StronglyRationalVOA.ClosedGraphData.coordinate_doubleUnitary line 388
  21. theorem OAI.StronglyRationalVOA.ClosedGraphData.doubleUnitary_inclusion line 393
  22. theorem OAI.StronglyRationalVOA.ClosedGraphData.entry_transport line 398
  23. theorem OAI.StronglyRationalVOA.ClosedGraphData.commute_transport line 409
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrder_strongCommutation line 436
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_strongCommutation_of_firstOrder line 511