OAI/RepresentationTheory/VertexAlgebra/PrimaryStressWeak.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_stress_weakCommutation line 18
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_weakCommutation_of_algebraic line 45
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.highField_graph_invariant_firstOrderFlow_of_weak line 83
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_power_stress_graph_entries_commute line 166
  5. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_invariant_of_regularizers line 205
  6. lemma OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_of_selfAdjoint_regularizers line 228
  7. lemma OAI.StronglyRationalVOA.SymmetricOperator.graph_entries_commute_of_regularizers line 242
  8. def OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral line 272
  9. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_apply line 287
  10. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_norm line 290
  11. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_matrix_derivative line 297
  12. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_graph line 315
  13. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_commutes_flow line 331
  14. lemma OAI.StronglyRationalVOA.SymmetricOperator.inner_timeIntegral_right line 342
  15. lemma OAI.StronglyRationalVOA.SymmetricOperator.inner_timeIntegral_left line 347
  16. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_adjoint line 355
  17. def OAI.StronglyRationalVOA.SymmetricOperator.timeAverage line 367
  18. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_selfAdjoint line 370
  19. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_norm line 377
  20. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_graph line 387
  21. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_initial_bound line 392
  22. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_strong_one line 416
  23. lemma OAI.StronglyRationalVOA.intervalIntegral_mem_closedSubmodule line 438
  24. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_preserves_graph line 451
  25. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_preserves_graph line 466
  26. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeIntegral_commutes line 482
  27. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_commutes line 492
  28. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_timeAverage_commutes line 497
  29. def OAI.StronglyRationalVOA.SymmetricOperator.timeDifference line 504
  30. lemma OAI.StronglyRationalVOA.SymmetricOperator.timeAverage_graph' line 507