OAI/RepresentationTheory/VertexAlgebra/EnergyShiftPow.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyShift_pow_norm_mono line 19
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyBound_add line 29
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.polynomialEnergyBounds line 53
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_le_generatorFiltration line 73
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.c2_grade_le_generatorFiltration line 109
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_energy_generating_filtration line 120
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_decomposition line 168
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.grade_le_primaryDescendantSpan line 195
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primaryDescendantSpan_eq_top line 212
  10. theorem OAI.StronglyRationalVOA.additive_cutoff_log_bound line 226
  11. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_tsum_left line 309
  12. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_tsum_right line 313
  13. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_tsum_prod line 319
  14. lemma OAI.StronglyRationalVOA.LocalSkewFlow.tsum_prod_antidiagonal line 334
  15. lemma OAI.StronglyRationalVOA.LocalSkewFlow.exp_antidiagonal line 344
  16. def OAI.StronglyRationalVOA.LocalSkewFlow.skewExpTerm line 364
  17. def OAI.StronglyRationalVOA.LocalSkewFlow.skewExp line 367
  18. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewExpTerm_norm_bound line 370
  19. lemma OAI.StronglyRationalVOA.LocalSkewFlow.summable_norm_skewExpTerm line 390
  20. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skew_pow_inner line 398
  21. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_skewExpTerm line 410
  22. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_skewExp line 423
  23. lemma OAI.StronglyRationalVOA.LocalSkewFlow.norm_skewExp line 458
  24. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewExp_add line 467
  25. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewExp_smul line 474
  26. lemma OAI.StronglyRationalVOA.LocalSkewFlow.summable_shifted_pow_geometric line 481
  27. lemma OAI.StronglyRationalVOA.LocalSkewFlow.shifted_pow_geometric_tail_uniform line 497