OAI/RepresentationTheory/VertexAlgebra/StressSmoothness.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.RealCircleCalculus.space_deriv_eq_fderiv line 28
  2. lemma OAI.StronglyRationalVOA.RealCircleCalculus.time_deriv_eq_fderiv line 34
  3. lemma OAI.StronglyRationalVOA.RealCircleCalculus.space_deriv_smooth line 40
  4. lemma OAI.StronglyRationalVOA.RealCircleCalculus.time_deriv_smooth line 44
  5. lemma OAI.StronglyRationalVOA.RealCircleCalculus.mixed_deriv line 48
  6. lemma OAI.StronglyRationalVOA.RealCircleCalculus.integral_derivative line 70
  7. lemma OAI.StronglyRationalVOA.RealCircleCalculus.periodic_deriv line 90
  8. def OAI.StronglyRationalVOA.RealCircleCalculus.anomalyDensity line 97
  9. def OAI.StronglyRationalVOA.RealCircleCalculus.anomalyFlux line 99
  10. def OAI.StronglyRationalVOA.RealCircleCalculus.anomalyEnergy line 102
  11. lemma OAI.StronglyRationalVOA.RealCircleCalculus.anomaly_density_smooth line 104
  12. lemma OAI.StronglyRationalVOA.RealCircleCalculus.anomaly_density_derivative line 111
  13. lemma OAI.StronglyRationalVOA.RealCircleCalculus.anomaly_flux_smooth line 159
  14. lemma OAI.StronglyRationalVOA.RealCircleCalculus.anomaly_flux_periodic line 165
  15. lemma OAI.StronglyRationalVOA.RealCircleCalculus.anomaly_energy_derivative line 172
  16. lemma OAI.StronglyRationalVOA.RealCircleCalculus.deriv_ofReal line 212
  17. lemma OAI.StronglyRationalVOA.RealCircleCalculus.iteratedDeriv_ofReal line 215
  18. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularVelocity line 227
  19. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularDensity line 228
  20. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularVelocity_smooth line 229
  21. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularDensity_smooth line 231
  22. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularVelocity_periodic line 234
  23. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularDensity_periodic line 238
  24. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularDensity_pos line 242
  25. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.realAngularDensity_PDE line 245
  26. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.angular_cocycle_coefficient line 265
  27. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.normalizedAnomaly line 289
  28. def OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.anomalyShift line 292
  29. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.anomalyShift_zero line 294
  30. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.anomalyShift_derivative line 296
  31. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.unitParameter line 315
  32. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.unitParameter_smooth line 316
  33. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.unitParameter_periodic line 318
  34. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.unitParameter_pos line 322
  35. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening line 323
  36. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_density_one line 330
  37. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_realDensity_zero line 334
  38. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_realDensity_one line 340
  39. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flatteningAnomaly_one line 342
  40. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flatteningAnomaly_zero line 350
  41. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flatteningShift line 361
  42. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.SmoothLift.density_power line 369
  43. def OAI.StronglyRationalVOA.SmoothCircleFunction.constant line 377
  44. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.constant_apply line 381
  45. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_constant_zero line 382
  46. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_zero_constant line 388
  47. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_constant line 390
  48. lemma OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_constant line 404
  49. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smooth_constant_bound line 414
  50. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.constant_stress_core line 427
  51. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.constant_stress_bound line 433
  52. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.constant_stress_extension line 439
  53. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_one_constant_stress line 459
  54. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorSmooth_zero line 477
  55. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_density_form_covariance line 482
  56. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stress_density_smooth_covariance line 506