OAI/RepresentationTheory/VertexAlgebra/SmoothSmearShift.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_shift_bound line 39
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_modulated_product line 57
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.normalAt line 101
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.normalAt_left_finite line 105
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.normalAt_right_finite line 116
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.normalAt_step line 127
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.normalAt_vertex_product line 147
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.normalAt_choose line 169
  9. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_choose_cutoff line 219
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_normalAt_cutoff line 240
  11. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothCoreVector line 294
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_core line 296
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_smoothSmear_product_core line 299
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_smoothSmear_product_matrix line 320
  15. lemma OAI.StronglyRationalVOA.summable_norm_normal_triangle line 348
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normal_diagonal_polynomial_bound line 410
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_normal_left line 432
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_normal_right line 453
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_modulated_left_matrix line 483
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_modulated_right_matrix line 503
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_normalAt_completion line 525