OAI/RepresentationTheory/VertexAlgebra/TimeAverageGraph.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_graph_commute line 17
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_timeDifference_commute line 24
  3. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeDifference_norm line 29
  4. def OAI.StronglyRationalVOA.SymmetricOperator.iteratedGraph line 41
  5. lemma OAI.StronglyRationalVOA.SymmetricOperator.iteratedGraph_regularizer line 46
  6. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_iterated_graph line 61
  7. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_factor line 67
  8. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeDifference_selfAdjoint line 79
  9. lemma OAI.StronglyRationalVOA.SymmetricOperator.contraction_pow_initial_bound line 90
  10. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_pow_strong_one line 105
  11. lemma OAI.StronglyRationalVOA.SymmetricOperator.bounded_regularization line 123
  12. lemma OAI.StronglyRationalVOA.SymmetricOperator.bounded_symmetric_of_core line 149
  13. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularization_selfAdjoint line 163
  14. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularization_preserves_closure line 179
  15. def OAI.StronglyRationalVOA.SymmetricOperator.onSubmodule line 210
  16. lemma OAI.StronglyRationalVOA.SymmetricOperator.onSubmodule_graph line 214
  17. lemma OAI.StronglyRationalVOA.SymmetricOperator.onSubmodule_mem_graph line 224
  18. lemma OAI.StronglyRationalVOA.SymmetricOperator.closure_eq_of_intermediate line 228
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_core line 244
  20. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_inverse_factor line 277
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.core_timeAverage_energyGraph line 294
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrderSmear_timeAverage_energyGraph line 311
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.firstOrderSmear_timeAverage_smoothEnergySpace line 334
  24. lemma OAI.StronglyRationalVOA.SymmetricOperator.end_pow_bound line 364
  25. lemma OAI.StronglyRationalVOA.SymmetricOperator.commuting_core_power_bound line 378
  26. def OAI.StronglyRationalVOA.SymmetricOperator.restricted line 400
  27. lemma OAI.StronglyRationalVOA.SymmetricOperator.restricted_coe line 404
  28. lemma OAI.StronglyRationalVOA.SymmetricOperator.restricted_pow_coe line 407
  29. lemma OAI.StronglyRationalVOA.SymmetricOperator.restricted_commutes_of_graph line 417
  30. lemma OAI.StronglyRationalVOA.SymmetricOperator.local_energy_regularization line 435
  31. lemma OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_of_local_energy line 486