OAI/RepresentationTheory/VertexAlgebra/InverseEnergySelf.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_selfAdjoint line 18
  2. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_graph line 27
  3. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_diagonal line 35
  4. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_inverse_graph line 42
  5. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_defect line 54
  6. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_preserves_regularizer_range line 106
  7. def OAI.StronglyRationalVOA.SymmetricOperator.BoundedGraphCore line 138
  8. theorem OAI.StronglyRationalVOA.SymmetricOperator.graph_of_parametrized_adjoint line 141
  9. theorem OAI.StronglyRationalVOA.SymmetricOperator.formalAdjoint_graph_pairing line 158
  10. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_graph_invariant line 169
  11. theorem OAI.StronglyRationalVOA.SymmetricOperator.graph_invariant_of_commutes_resolvent line 212
  12. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_coreWeighted line 234
  13. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_boundedGraphCore line 242
  14. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_weakCommutation line 263
  15. theorem OAI.StronglyRationalVOA.SymmetricOperator.graph_entries_commute line 293
  16. theorem OAI.StronglyRationalVOA.HilbertScale.coreOperator_strongCommutation line 328
  17. def OAI.StronglyRationalVOA.SmoothCircleFunction.toContinuousMap line 388
  18. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.toContinuousMap_coe line 391
  19. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.fourierCoeff_toContinuousMap line 394
  20. def OAI.StronglyRationalVOA.FourierAnalysis.coefficientCLM line 412
  21. theorem OAI.StronglyRationalVOA.FourierAnalysis.coefficientCLM_apply line 432
  22. theorem OAI.StronglyRationalVOA.FourierAnalysis.coefficient_character_mul line 436
  23. theorem OAI.StronglyRationalVOA.FourierAnalysis.hasSum_coefficient_product line 448
  24. def OAI.StronglyRationalVOA.SmoothCircleFunction.mul line 470
  25. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.mul_apply line 473
  26. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.toContinuousMap_mul line 475
  27. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_mul line 482
  28. def OAI.StronglyRationalVOA.SmoothCircleFunction.differentiated line 496
  29. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.differentiated_apply line 503
  30. theorem OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_deriv_zero line 508