OAI/RepresentationTheory/VertexAlgebra/SymmetricWeakCommute.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.SymmetricOperator.symmetric_weak_commute line 18
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_entries_commute_of_local_energy line 35
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryLocalEnergyEstimate line 117
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_physical_bound line 125
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_hermitian line 131
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_selfAdjoint line 134
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.closedSmoothField_symmetric line 141
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_power_graph_stressFlow line 150
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_timeAverage_smooth line 166
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_power_selfAdjoint_of_localEstimate line 178
  11. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.power_tsupport_subset line 198
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_core_closable line 211
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_power_graph_locality_of_localEstimate line 224
  14. lemma OAI.StronglyRationalVOA.LocalCovariance.shifted_power_graph_bound line 276
  15. lemma OAI.StronglyRationalVOA.LocalCovariance.bound_of_unitary_covariance line 316
  16. structure OAI.StronglyRationalVOA.PositiveCircleGeometry.Field line 352
  17. instance OAI.StronglyRationalVOA.PositiveCircleGeometry.(instance at line 357) line 357
  18. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.totalTime line 361
  19. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.normalizedCoordinate line 363
  20. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.inverse_continuous line 365
  21. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.totalTime_pos line 368
  22. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_hasDerivAt line 373
  23. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_derivative_pos line 381
  24. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_strictMono line 385
  25. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_add_one line 390
  26. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.circleLift line 399
  27. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_smooth line 404
  28. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinate_surjective line 412
  29. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinateOrderIso line 415
  30. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.coordinateOrderIso_apply line 420
  31. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.inverse_coordinate_smooth line 423
  32. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.frequency line 433
  33. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.frequency_pos line 434
  34. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.frequency_le line 436
  35. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flatten_identity line 449
  36. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.stressScalar line 457
  37. def OAI.StronglyRationalVOA.PositiveCircleGeometry.quadraticField line 467
  38. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.quadratic_derivative line 473
  39. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.quadratic_logDerivative_bound line 479
  40. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.quadratic_frequency_bound line 488
  41. def OAI.StronglyRationalVOA.TimeOrdered.term line 509