OAI/RepresentationTheory/VertexAlgebra/HighFieldGraph.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.highField_graph_invariant_firstOrderFlow line 18
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_invariant_of_commutes_flow line 95
  3. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_entries_commute_of_flow_invariant line 121
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.highField_firstOrder_graph_entries_commute line 146
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.highField_stress_graph_entries_commute line 167
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_primary_physical_commutator line 191
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.primarySpace line 233
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.pct_primary line 245
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_hermitian_primary_spanning line 250
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_le_primaryGeneratorFiltration line 302
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_primary_generating_filtration line 349
  12. def OAI.StronglyRationalVOA.SmoothCircleFunction.power line 411
  13. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.power_apply line 414
  14. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.power_real line 416
  15. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.derivative_power_balance line 421
  16. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_power_commutator_zero line 435
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.hasSum_primary_stress_commutator_zero line 461
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_weakCommutation_of_convolution line 485