OAI/RepresentationTheory/VertexAlgebra/LocalNormalSeries.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.local_normal_series_matrix line 37
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modulated_product_uniform_bound line 93
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_normal_left_shift line 132
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_norm_normal_right_shift line 149
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_normalAt_cutoff_shift line 172
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_vertex_normal_cutoff line 220
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_modulated_left_matrix_shift line 235
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.hasSum_modulated_right_matrix_shift line 255
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.local_normal_series_matrix_shift line 281
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.summable_modulated_product_shift line 337
  11. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modulatedSum line 348
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modulatedSum_apply line 364
  13. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPowerLinear line 377
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPowerLinear_apply line 380
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPowerLinear_dense line 382
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_inverse_add line 387
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_norm_add line 392
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smooth_linear_eq_of_core line 398
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modulatedSum_sobolev_bound line 436
  20. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap line 466
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap_matrix line 471
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap_core line 486
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smooth_linear_add_bound line 527