OAI/RepresentationTheory/VertexAlgebra/StressCutoffNormalized.lean

GitHub source file

41 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 line 24
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_continuous line 35
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_commutator line 43
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_error line 58
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_difference line 74
  6. structure OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.StressPath line 94
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPath_cutoff_bound line 104
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPath_cutoff_commutator line 112
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPath_cutoff_difference line 123
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_stressPropagator line 139
  11. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator line 165
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_unitary line 168
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_limit line 172
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_star_limit line 176
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_factor line 180
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_star_factor line 197
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_injective line 224
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.inverseSobolev_zero line 228
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolev_interpolation_bound line 232
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.tendsto_sobolev_of_extra_bound line 254
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_inverse_next line 274
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_sub line 280
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.tendsto_smoothEnergyPower line 286
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.preserves_smoothEnergySpace_of_factor line 313
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_eq_of_factor line 336
  26. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_smooth line 347
  27. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_star_smooth line 355
  28. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorSmooth line 363
  29. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorSmooth_bound line 368
  30. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_evolution_factor line 376
  31. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_evolution_smooth line 390
  32. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoffEvolutionSmooth line 398
  33. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoffEvolutionSmooth_bound line 404
  34. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoffEvolutionSmooth_limit line 412
  35. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_normalized_norm line 426
  36. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_smooth_bound line 437
  37. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_derivative_bound line 447
  38. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressCutoff_evolution_sub_bound line 470
  39. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_sub_bound line 488
  40. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagator_smooth_continuous line 497
  41. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stressPropagatorSmooth_continuous_power line 515