OAI/RepresentationTheory/VertexAlgebra/HilbertRegularization.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.HilbertScale.regularized line 19
  2. theorem OAI.StronglyRationalVOA.HilbertScale.regularized_core line 23
  3. def OAI.StronglyRationalVOA.HilbertScale.coreOperator line 32
  4. theorem OAI.StronglyRationalVOA.HilbertScale.coreOperator_formalAdjoint line 37
  5. theorem OAI.StronglyRationalVOA.HilbertScale.coreOperator_closable line 41
  6. theorem OAI.StronglyRationalVOA.HilbertScale.regularized_graph_closure line 48
  7. theorem OAI.StronglyRationalVOA.HilbertScale.weighted_resolvent_difference line 77
  8. theorem OAI.StronglyRationalVOA.HilbertScale.regularized_defect_pairing line 90
  9. theorem OAI.StronglyRationalVOA.HilbertScale.regularized_defect line 135
  10. theorem OAI.StronglyRationalVOA.HilbertScale.coreOperator_essentialSelfAdjoint line 169
  11. theorem OAI.StronglyRationalVOA.OperatorTransport.monotone line 206
  12. theorem OAI.StronglyRationalVOA.OperatorTransport.closable line 212
  13. theorem OAI.StronglyRationalVOA.OperatorTransport.closure line 216
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coreEnergy_mem line 233
  15. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coreEnergyCoordinates line 240
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coreEnergyCoordinates_coe line 261
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coreEnergyCoordinates_energyShift line 265
  18. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.spectralCoreMap line 278
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.spectralCoreMap_apply line 282
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.spectralCoreOperator_transport line 286
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrder_essentialSelfAdjoint line 315
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedCore_essentialSelfAdjoint line 368
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.current_closedSmearedOperator_selfAdjoint line 388
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightTwo_closedSmearedOperator_selfAdjoint line 398
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_closedSmearedOperator_selfAdjoint line 408
  26. def OAI.StronglyRationalVOA.SmoothCircleFunction.IsReal line 423
  27. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_real line 425
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_closedSmoothField_selfAdjoint line 452
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.current_closedSmoothField_selfAdjoint line 457
  30. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightTwo_closedSmoothField_selfAdjoint line 463
  31. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_sobolev_bound line 479