OAI/RepresentationTheory/VertexAlgebra/CoefficientSummableBound.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_summable_bound line 29
  2. lemma OAI.StronglyRationalVOA.coefficientSeminorm_tendsto_zero line 39
  3. structure OAI.StronglyRationalVOA.SmoothCircleFamily line 51
  4. instance OAI.StronglyRationalVOA.SmoothCircleFamily.(instance at line 55) line 55
  5. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.time_smooth line 57
  6. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.space_iterated_smooth line 59
  7. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.time_derivative_smooth line 62
  8. def OAI.StronglyRationalVOA.SmoothCircleFamily.timeDerivative line 66
  9. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.coefficient_derivative line 75
  10. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.coefficient_bound_compact line 118
  11. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.seminorm_continuous line 133
  12. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.seminorm_derivative line 150
  13. lemma OAI.StronglyRationalVOA.SmoothCircleFamily.seminorm_bound_stationary line 192
  14. def OAI.StronglyRationalVOA.SmoothCircleFamily.toStressPath line 206
  15. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.ext line 220
  16. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angular_shift line 228
  17. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularVelocity line 231
  18. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularVelocity_real line 241
  19. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularVelocity_stationary line 244
  20. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularStressPath line 247
  21. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularDensity line 250
  22. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularDensity_real line 259
  23. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularVelocity_space_derivative line 261
  24. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularDensity_space_derivative line 267
  25. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angularDensity_transport line 274
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_density_closed_covariance line 297
  27. def OAI.StronglyRationalVOA.SmoothCircleFunction.cocycleDensity line 326
  28. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_cocycleDensity line 328
  29. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_weakCommutator_central line 348
  30. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_weakCommutator_central_of_algebraic line 374
  31. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_stress_weakCommutator line 414
  32. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_stress_smoothCommutator line 501
  33. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_density_form_derivative line 514