OAI/RepresentationTheory/VertexAlgebra/SmoothConjugateInner.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.SymmetricOperator.smoothConjugate_inner_left line 33
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.smoothConjugate_adjoint line 44
  3. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_power line 60
  4. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.translate_tsupport_subset line 64
  5. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.exists_translation_radius line 73
  6. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.translate line 101
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.commutant_preserves_graph line 115
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.conjugation_preserves_field_graph line 126
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_preserves_primary_graph line 141
  10. lemma OAI.StronglyRationalVOA.SymmetricOperator.onSubmodule_closure_graph_invariant line 167
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_scale line 184
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_linearCombination line 191
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.field_graph_invariant_linearCombination line 203
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_difference_graph_invariant line 239
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_difference_entry_mem line 273
  16. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.compact_translation_radius line 294
  17. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.exists_real_cutoff line 316
  18. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.power_tsupport_circle_subset line 410
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_real_entry_mem line 424
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_real_graph_invariant line 455
  21. def OAI.StronglyRationalVOA.SmoothCircleFunction.rePart line 473
  22. def OAI.StronglyRationalVOA.SmoothCircleFunction.imPart line 477
  23. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.rePart_real line 480
  24. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.imPart_real line 481
  25. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.rePart_support line 482
  26. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.imPart_support line 490
  27. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.rePart_add_imPart line 498
  28. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.field_graph_invariant_add_smul line 506