OAI/RepresentationTheory/VertexAlgebra/LocalNormalMap.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap_bound line 37
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_sobolev_bound line 44
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap_eq_smoothSmear line 55
  4. def OAI.StronglyRationalVOA.SmoothCircleFunction.modulate line 76
  5. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.modulate_coefficient line 86
  6. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.modulate_support line 92
  7. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.modulate_translate_support line 105
  8. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.exists_normal_cutoff line 115
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.modulatedSum_commutes line 137
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localNormalMap_commutes line 160
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normal_product_graph_invariant line 175
  12. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState line 224
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_localState_graph line 230
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.normal_product line 254
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.span line 288
  16. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.differentiated_support_circle line 331
  17. def OAI.StronglyRationalVOA.SmoothCircleFunction.translationTest line 337
  18. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translationTest_coefficient line 339
  19. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translationTest_support line 343
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_translation line 359
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.LocalState.translation line 374
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_realLocal_graph line 387
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.localState_of_real line 420
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_localState line 451
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_localState line 459
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.vacuum_smearedMap line 471
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.vacuum_closed_graph line 484
  28. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.vacuum_localState line 532