OAI/RepresentationTheory/VertexAlgebra/GraphInvariantOf.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.ClosedGraphData.graph_invariant_of_entry_commutes line 31
  2. lemma OAI.StronglyRationalVOA.ClosedGraphData.entry_commutes_iff_graph_reduces line 46
  3. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_eigenvector line 67
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_eq_hamiltonianFlow line 98
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.rotation_derivative line 116
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_graph_iff line 126
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_graph_iff_inverse line 130
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_add_graph line 136
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_domain_le line 149
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOne_graph_iff line 159
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_mem line 174
  12. def OAI.StronglyRationalVOA.SymmetricOperator.conjugation line 191
  13. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_norm line 193
  14. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_opNorm line 198
  15. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_continuous line 201
  16. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_inner line 208
  17. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_matrix_derivative line 212
  18. def OAI.StronglyRationalVOA.SymmetricOperator.conjugationIntegral line 228
  19. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugationIntegral_apply line 250
  20. lemma OAI.StronglyRationalVOA.SymmetricOperator.inner_conjugationIntegral line 253
  21. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugationIntegral_generator_graph line 264
  22. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugationIntegral_preserves_graph line 305
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conjugationIntegral_energy_domain line 335
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conjugationIntegral_smooth line 376
  25. def OAI.StronglyRationalVOA.SmoothRotationKernel.bump line 392
  26. def OAI.StronglyRationalVOA.SmoothRotationKernel.kernel line 394
  27. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.nonneg line 395
  28. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.integral line 397
  29. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.continuous line 399
  30. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.support line 401
  31. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.tsupport line 403
  32. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.normed_smooth line 405
  33. def OAI.StronglyRationalVOA.SmoothRotationKernel.jet line 407
  34. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_zero line 409
  35. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_continuous line 410
  36. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_derivative line 412
  37. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_support line 417
  38. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_compactSupport line 431
  39. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_bounded line 433
  40. def OAI.StronglyRationalVOA.SmoothRotationKernel.bound line 437
  41. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.norm_le_bound line 438
  42. lemma OAI.StronglyRationalVOA.SmoothRotationKernel.jet_vanish line 440
  43. def OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate line 454
  44. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_apply line 458
  45. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_norm_apply line 469
  46. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_norm line 481
  47. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_strong line 484
  48. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_smooth line 497
  49. lemma OAI.StronglyRationalVOA.SymmetricOperator.conjugation_adjoint line 512
  50. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_integrable line 517
  51. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_inner_right line 522