OAI/RepresentationTheory/VertexAlgebra/SmoothEnergyPower.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_zero line 30
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_constant_stress line 33
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorSmoothEquiv line 53
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_smul line 61
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_constant line 72
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_density_smooth_covariance line 83
  7. def OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.smoothCircle line 112
  8. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.smoothCircle_apply line 116
  9. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.smoothCircle_real line 117
  10. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_angular_zero line 118
  11. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_angular_one line 123
  12. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_primary_zero line 129
  13. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.flattening_primary_one line 138
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_positive_local_bound line 151
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_strictPositive_localEnergy line 189
  16. lemma OAI.StronglyRationalVOA.RealCircleCalculus.average_bounds line 206
  17. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.Field.frequency_sub_stressScalar_bound line 220
  18. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.quadratic_uniform_anomaly line 246
  19. lemma OAI.StronglyRationalVOA.LocalCovariance.continuous_power_affine line 272
  20. def OAI.StronglyRationalVOA.SmoothCircleFunction.ofRealPeriodic line 287
  21. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.ofRealPeriodic_apply line 291
  22. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.ofRealPeriodic_real line 293
  23. def OAI.StronglyRationalVOA.SmoothCircleFunction.quadraticFamily line 295
  24. def OAI.StronglyRationalVOA.SmoothCircleFunction.powerFamily line 298
  25. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.quadraticFamily_zero line 301
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_sub line 309
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_add line 321
  28. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_add_functions line 328
  29. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_family_continuous line 336
  30. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.quadratic_stress_powers_continuous line 343
  31. lemma OAI.StronglyRationalVOA.PositiveCircleGeometry.quadratic_smoothCircle line 357
  32. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_square_localEnergy line 374
  33. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_squarePower_selfAdjoint line 424
  34. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_squarePower_graph_locality line 436
  35. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.real_reconstruct line 463
  36. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.power_tsupport_eq line 473
  37. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.tsupport_lift_subset line 479
  38. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.disjoint_lift line 485
  39. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_realSquare_localEnergy line 493
  40. structure OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField line 502
  41. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.field line 515
  42. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.closed line 517
  43. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.PrimaryTestField.selfAdjoint line 519