OAI/RepresentationTheory/VertexAlgebra/GraphEquiv.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.OperatorTransport.graphEquiv line 19
  2. theorem OAI.StronglyRationalVOA.OperatorTransport.graph_eq line 22
  3. theorem OAI.StronglyRationalVOA.OperatorTransport.closed line 27
  4. theorem OAI.StronglyRationalVOA.OperatorTransport.dense line 32
  5. theorem OAI.StronglyRationalVOA.OperatorTransport.adjoint line 38
  6. theorem OAI.StronglyRationalVOA.OperatorTransport.selfAdjoint line 56
  7. theorem OAI.StronglyRationalVOA.OperatorTransport.domRestrict line 62
  8. theorem OAI.StronglyRationalVOA.OperatorTransport.hasCore line 84
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.finiteCore_comap_energyCoordinates line 110
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator line 145
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_closed line 149
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_dense line 152
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_selfAdjoint line 156
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_hasCore line 162
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coe_mem_energyOperator line 170
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conformalHamiltonian line 175
  17. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower line 179
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyOperator_grade line 182
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_coe line 203
  20. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergySpace line 235
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.core_le_smoothEnergySpace line 237
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergySpace_dense line 242
  23. def OAI.StronglyRationalVOA.SymmetricOperator.shift line 257
  24. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_apply line 261
  25. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_graph line 264
  26. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_closed line 276
  27. theorem OAI.StronglyRationalVOA.SymmetricOperator.real_expectation line 284
  28. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_I_norm_sq line 292
  29. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_I_lower_bound line 299
  30. theorem OAI.StronglyRationalVOA.SymmetricOperator.range_closed_of_lower_bound line 308
  31. theorem OAI.StronglyRationalVOA.SymmetricOperator.orthogonal_range_shift line 333
  32. theorem OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_of_deficiency_zero line 350
  33. theorem OAI.StronglyRationalVOA.SymmetricOperator.formalAdjoint_closure line 393
  34. theorem OAI.StronglyRationalVOA.SymmetricOperator.regularizer_adjoint line 425
  35. theorem OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_of_regularizers line 442
  36. def OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier line 503
  37. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_apply line 510
  38. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_norm line 515