OAI/RepresentationTheory/VertexAlgebra/StressEvolution.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.TimeOrdered.term_continuous line 20
  2. lemma OAI.StronglyRationalVOA.TimeOrdered.term_derivative line 28
  3. lemma OAI.StronglyRationalVOA.TimeOrdered.term_bound line 36
  4. lemma OAI.StronglyRationalVOA.TimeOrdered.term_summable line 64
  5. def OAI.StronglyRationalVOA.TimeOrdered.evolution line 68
  6. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_zero line 71
  7. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_derivative line 78
  8. lemma OAI.StronglyRationalVOA.TimeOrdered.norm_growth line 108
  9. lemma OAI.StronglyRationalVOA.TimeOrdered.zero_of_derivative_bound line 127
  10. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_unitary line 139
  11. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_mem_unitary line 172
  12. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_norm line 176
  13. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_star_norm line 181
  14. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_apply_derivative line 186
  15. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_energy_bound line 194
  16. lemma OAI.StronglyRationalVOA.TimeOrdered.duhamel_bound line 222
  17. lemma OAI.StronglyRationalVOA.TimeOrdered.linear_ode_unique line 257
  18. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_reverse line 269
  19. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_star_energy_bound line 288
  20. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_regularizer_factor line 307
  21. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_opNorm line 335
  22. lemma OAI.StronglyRationalVOA.TimeOrdered.evolution_difference_regularized line 342
  23. lemma OAI.StronglyRationalVOA.TimeOrdered.exists_evolution_limit line 368
  24. lemma OAI.StronglyRationalVOA.TimeOrdered.unitary_of_strong_and_star_limit line 400
  25. lemma OAI.StronglyRationalVOA.TimeOrdered.exists_unitary_evolution_limit line 442
  26. lemma OAI.StronglyRationalVOA.TimeOrdered.regularizer_factor_of_limits line 484
  27. def OAI.StronglyRationalVOA.HilbertScale.energyCutoff line 512
  28. lemma OAI.StronglyRationalVOA.HilbertScale.energyCutoff_apply line 515