OAI/RepresentationTheory/VertexAlgebra/StressPropagatorDerivative.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorDerivative_smoothSmear line 27
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_form_derivative line 39
  3. lemma OAI.StronglyRationalVOA.OperatorTransport.onSubmodule line 80
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_zero line 113
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_transport_form_derivative line 120
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_transport_form_constant line 156
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorEquiv line 178
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorEquiv_apply line 182
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorEquiv_symm_apply line 185
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_transport_smooth_covariance line 189
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_transport_closed_graph line 221
  12. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.parameter_inverse_smooth line 242
  13. structure OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift line 286
  14. instance OAI.StronglyRationalVOA.PositiveCircleGeometry.(instance at line 291) line 291
  15. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.strictMono line 294
  16. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.degreeOne line 296
  17. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.surjective line 300
  18. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.orderIso line 302
  19. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.orderIso_apply line 304
  20. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate line 308
  21. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_smooth line 309
  22. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_zero line 312
  23. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_one line 313
  24. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_add_one line 314
  25. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_derivative line 316
  26. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_derivative_pos line 321
  27. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.isotopy line 329
  28. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.isotopy_apply line 334
  29. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse line 342
  30. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_smooth line 343
  31. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.interpolate_inverse line 348
  32. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_interpolate line 350
  33. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_add_one line 352
  34. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.jacobian line 356
  35. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.jacobian_pos line 357
  36. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.jacobian_smooth line 358
  37. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.velocity line 361
  38. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.velocity_smooth line 362
  39. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_space_derivative line 365
  40. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_time_derivative line 372
  41. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.velocity_space_derivative line 387
  42. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.jacobian_space_derivative line 394
  43. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.jacobian_time_derivative line 399
  44. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density line 407
  45. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_smooth line 409
  46. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_space_derivative line 413
  47. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_time_derivative line 423
  48. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.derivative_periodic line 445
  49. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.velocity_periodic line 450
  50. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_periodic line 454
  51. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.inverse_zero line 458
  52. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_zero line 461
  53. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.velocity_stationary line 463
  54. lemma OAI.StronglyRationalVOA.joint_space_deriv_smooth line 482
  55. lemma OAI.StronglyRationalVOA.joint_iterated_space_deriv_smooth line 491
  56. lemma OAI.StronglyRationalVOA.summable_circle_decay line 497
  57. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_weighted_bound line 507