OAI/RepresentationTheory/VertexAlgebra/RegularizerFactorAdd.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_factor_add line 16
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_factor_continuous line 26
  3. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_factor_integral line 42
  4. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_factor_derivative line 56
  5. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev line 82
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_apply line 87
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_selfAdjoint line 93
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_graph line 102
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_on_graph line 109
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_dense line 114
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_eq_conj line 121
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_inverse_graph line 127
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_defect line 136
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.core_flow_energyGraph line 174
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_zero_graph line 194
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrderSmear_flow_energyGraph line 202
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrderSmear_flow_smoothEnergySpace line 226
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_weakCommutation line 261
  19. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear line 280
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_graph line 300
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_eq_extension line 306
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_symmetric line 316
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_weakCommutation line 328
  24. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower line 369
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_graph line 372
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_smoothEnergyPower line 376
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_coe line 380
  28. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularized_heisenberg_pairing line 398
  29. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_invariant_of_core line 430
  30. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_inner line 442
  31. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_inverse line 448
  32. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularized_commutation_on_dense_core line 459