OAI/RepresentationTheory/VertexAlgebra/BoundedMultiplierSingle.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_single line 18
  2. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_preservesFiniteCore line 27
  3. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_graph line 41
  4. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_adjoint line 47
  5. theorem OAI.StronglyRationalVOA.HilbertScale.real_boundedMultiplier_selfAdjoint line 64
  6. theorem OAI.StronglyRationalVOA.HilbertScale.finiteCore_dense line 77
  7. theorem OAI.StronglyRationalVOA.StrongOperatorLimit.zero_of_dense line 93
  8. theorem OAI.StronglyRationalVOA.HilbertScale.boundedMultiplier_strong_zero line 122
  9. def OAI.StronglyRationalVOA.HilbertScale.coreDiagonal line 148
  10. theorem OAI.StronglyRationalVOA.HilbertScale.coreDiagonal_apply line 151
  11. theorem OAI.StronglyRationalVOA.HilbertScale.coreDiagonal_single line 154
  12. theorem OAI.StronglyRationalVOA.HilbertScale.coreDiagonal_mem_finiteCore line 158
  13. def OAI.StronglyRationalVOA.HilbertScale.coreMultiplier line 179
  14. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_coe line 182
  15. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_apply line 185
  16. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_mul line 188
  17. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_one line 195
  18. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_eq_bounded line 204
  19. def OAI.StronglyRationalVOA.HilbertScale.resolventWeight line 210
  20. def OAI.StronglyRationalVOA.HilbertScale.complementWeight line 213
  21. theorem OAI.StronglyRationalVOA.HilbertScale.resolventWeight_nonneg line 216
  22. theorem OAI.StronglyRationalVOA.HilbertScale.resolventWeight_le_one line 222
  23. theorem OAI.StronglyRationalVOA.HilbertScale.complementWeight_nonneg line 229
  24. theorem OAI.StronglyRationalVOA.HilbertScale.complementWeight_le_one line 235
  25. theorem OAI.StronglyRationalVOA.HilbertScale.resolventWeight_add_complementWeight line 243
  26. theorem OAI.StronglyRationalVOA.HilbertScale.complementWeight_tendsto_zero line 249
  27. def OAI.StronglyRationalVOA.HilbertScale.resolvent line 256
  28. def OAI.StronglyRationalVOA.HilbertScale.complement line 262
  29. theorem OAI.StronglyRationalVOA.HilbertScale.resolvent_apply line 267
  30. theorem OAI.StronglyRationalVOA.HilbertScale.complement_apply line 270
  31. theorem OAI.StronglyRationalVOA.HilbertScale.resolvent_add_complement line 273
  32. theorem OAI.StronglyRationalVOA.HilbertScale.resolvent_selfAdjoint line 280
  33. theorem OAI.StronglyRationalVOA.HilbertScale.resolvent_norm line 284
  34. theorem OAI.StronglyRationalVOA.HilbertScale.complement_strong_zero line 288
  35. theorem OAI.StronglyRationalVOA.HilbertScale.resolvent_strong_one line 295
  36. theorem OAI.StronglyRationalVOA.inner_tsum_left line 306
  37. theorem OAI.StronglyRationalVOA.inner_tsum_right line 311
  38. theorem OAI.StronglyRationalVOA.summable_inner_left line 316
  39. theorem OAI.StronglyRationalVOA.RapidCoefficients.int_mul line 323
  40. theorem OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_bound line 343
  41. theorem OAI.StronglyRationalVOA.CFTTypeVOA.energyShift_physical_commutator line 363
  42. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyShift_adjoint line 378
  43. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_symmetric line 385
  44. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_energy_commutator line 406
  45. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_cancel line 444
  46. theorem OAI.StronglyRationalVOA.HilbertScale.coreMultiplier_inv_cancel line 455
  47. def OAI.StronglyRationalVOA.HilbertScale.energyNormalized line 466
  48. def OAI.StronglyRationalVOA.HilbertScale.energyExtension line 472
  49. theorem OAI.StronglyRationalVOA.HilbertScale.energyNormalized_bound line 477
  50. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_core line 487
  51. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_weighted line 496
  52. theorem OAI.StronglyRationalVOA.HilbertScale.energyExtension_norm line 504
  53. theorem OAI.StronglyRationalVOA.HilbertScale.weighted_resolvent_core line 512