OAI/RepresentationTheory/VertexAlgebra/StressCutoffNormalized2.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_normalized_limit line 26
  2. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorDerivative line 36
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorDerivative_continuous line 41
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_derivative_limit line 46
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_evolution_derivative line 64
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_evolution_continuous line 76
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_integral_limit line 81
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_integral line 108
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_derivative line 127
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorDerivative_graph line 140
  11. lemma OAI.StronglyRationalVOA.SymmetricOperator.form_pairing_derivative line 158
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_smul line 181
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_smul line 191
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_sub line 204
  15. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField line 218
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField_norm line 222
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField_sub line 230
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField_smul line 238
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_eq_normalized line 246
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField_continuous line 253
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalizedField_derivative line 268
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_inner_orthogonal line 293
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inner_smearedMap_homogeneous line 308
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_stress_weakCommutator line 319
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_weakCommutator line 389
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_weakCommutator_of_algebraic line 412
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_stress_smoothCommutator line 452
  28. def OAI.StronglyRationalVOA.SmoothCircleFunction.add line 471
  29. def OAI.StronglyRationalVOA.SmoothCircleFunction.scale line 473
  30. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.add_apply line 475
  31. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.scale_apply line 476
  32. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_add line 477
  33. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.coefficient_scale line 488
  34. def OAI.StronglyRationalVOA.SmoothCircleFunction.primaryTransport line 494
  35. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.primaryTransport_apply line 497
  36. lemma OAI.StronglyRationalVOA.SmoothCircleFunction.hasSum_primaryTransport line 502