OAI/RepresentationTheory/VertexAlgebra/BoundedFlows.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.BoundedFlow.flow line 16
  2. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_unitary line 18
  3. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_norm line 24
  4. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_derivative line 27
  5. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_zero line 32
  6. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_add line 34
  7. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_generator_commute line 38
  8. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_commute line 41
  9. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_time_bound line 45
  10. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_initial_bound line 54
  11. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_difference line 58
  12. lemma OAI.StronglyRationalVOA.StrongLimit.equicontinuous_of_norm_bound line 83
  13. lemma OAI.StronglyRationalVOA.StrongLimit.exists_of_dense_core line 94
  14. lemma OAI.StronglyRationalVOA.StrongLimit.mul_tendsto line 133
  15. lemma OAI.StronglyRationalVOA.SymmetricOperator.resolvent_on_graph line 152
  16. lemma OAI.StronglyRationalVOA.SymmetricOperator.resolvent_commute line 161
  17. lemma OAI.StronglyRationalVOA.SymmetricOperator.imaginary_modulus line 179
  18. def OAI.StronglyRationalVOA.SymmetricOperator.regularizer line 182
  19. def OAI.StronglyRationalVOA.SymmetricOperator.boundedGenerator line 188
  20. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_graph line 194
  21. lemma OAI.StronglyRationalVOA.SymmetricOperator.boundedGenerator_selfAdjoint line 216
  22. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_norm_le line 228
  23. lemma OAI.StronglyRationalVOA.SymmetricOperator.boundedGenerator_commute line 244
  24. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_on_graph line 254
  25. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_error line 271
  26. abbrev OAI.StronglyRationalVOA.SymmetricOperator.sampleRadius line 302
  27. lemma OAI.StronglyRationalVOA.SymmetricOperator.sampleRadius_ge line 303
  28. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_strong line 307
  29. lemma OAI.StronglyRationalVOA.SymmetricOperator.boundedGenerator_strong line 325
  30. def OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow line 331
  31. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_norm line 334
  32. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_opNorm line 339
  33. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_difference line 345
  34. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_core_cauchy line 358
  35. lemma OAI.StronglyRationalVOA.SymmetricOperator.exists_flow_limit line 376
  36. def OAI.StronglyRationalVOA.SymmetricOperator.flow line 383
  37. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_tendsto line 386
  38. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_norm line 390
  39. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_zero line 395
  40. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_add line 402
  41. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_initial_bound line 412
  42. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_continuous_zero line 422
  43. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_continuous line 442
  44. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_graph line 453
  45. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_graph line 468
  46. lemma OAI.StronglyRationalVOA.BoundedFlow.flow_second_order line 479
  47. lemma OAI.StronglyRationalVOA.StrongLimit.intervalIntegral_tendsto line 504