OAI/RepresentationTheory/VertexAlgebra/SummableNormSobolev.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_sobolevSmear line 19
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_energyGraph line 34
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_mem_smoothEnergySpace line 54
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_sobolev_bound line 65
  5. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_diagonal_graph line 93
  6. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_graph line 137
  7. theorem OAI.StronglyRationalVOA.OperatorTransport.symm_transport line 162
  8. theorem OAI.StronglyRationalVOA.OperatorTransport.closable_iff line 168
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.coreEnergyCoordinates_energyPower line 184
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension line 198
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_apply line 204
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.spectralCoreMap_bound line 209
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_energyGraph line 220
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyPower_domain_le_coreClosure line 242
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_graph line 254
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightedSmearedMap line 284
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightedSmearedMap_apply line 292
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergySpace_le_closedSmearedDomain line 297
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmearedOperator_preserves_smoothEnergySpace line 308
  20. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_im_lower_bound line 351
  21. theorem OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_formal line 369
  22. theorem OAI.StronglyRationalVOA.SymmetricOperator.shift_bijective line 376
  23. def OAI.StronglyRationalVOA.SymmetricOperator.resolvent line 414
  24. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_graph line 426
  25. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_shift line 432
  26. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_norm_le line 442
  27. theorem OAI.StronglyRationalVOA.SymmetricOperator.resolvent_adjoint line 452
  28. theorem OAI.StronglyRationalVOA.SymmetricOperator.boundedPerturbation_shift_surjective line 473
  29. def OAI.StronglyRationalVOA.HilbertScale.inverseEnergy line 503
  30. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_apply line 510
  31. theorem OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_core line 513