OAI/RepresentationTheory/VertexAlgebra/MulLeftPow.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.LocalSkewFlow.mulLeft_pow_apply line 18
  2. lemma OAI.StronglyRationalVOA.LocalSkewFlow.mulRight_pow_apply line 24
  3. def OAI.StronglyRationalVOA.LocalSkewFlow.commutatorOperator line 32
  4. lemma OAI.StronglyRationalVOA.LocalSkewFlow.commutatorOperator_apply line 35
  5. lemma OAI.StronglyRationalVOA.LocalSkewFlow.commutatorOperator_pow line 38
  6. lemma OAI.StronglyRationalVOA.LocalSkewFlow.commutatorOperator_pow_normalized line 51
  7. def OAI.StronglyRationalVOA.LocalSkewFlow.insertedExpTerm line 78
  8. def OAI.StronglyRationalVOA.LocalSkewFlow.insertedExp line 81
  9. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_insertedExpTerm line 84
  10. lemma OAI.StronglyRationalVOA.LocalSkewFlow.inner_skewExp_inserted line 105
  11. lemma OAI.StronglyRationalVOA.LocalSkewFlow.insertedExpTerm_norm_bound line 135
  12. lemma OAI.StronglyRationalVOA.LocalSkewFlow.summable_norm_insertedExpTerm line 156
  13. lemma OAI.StronglyRationalVOA.LocalSkewFlow.insertedExpTerm_tail_bound line 177
  14. lemma OAI.StronglyRationalVOA.LocalSkewFlow.norm_tsum_tail_le line 197
  15. def OAI.StronglyRationalVOA.LocalSkewFlow.skewTaylor line 216
  16. lemma OAI.StronglyRationalVOA.LocalSkewFlow.coe_skewTaylor line 219
  17. lemma OAI.StronglyRationalVOA.LocalSkewFlow.coe_apply_skewTaylor line 230
  18. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewTaylor_add_tail line 241
  19. lemma OAI.StronglyRationalVOA.LocalSkewFlow.apply_skewTaylor_add_tail line 248
  20. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewExp_tail_bound line 255
  21. lemma OAI.StronglyRationalVOA.LocalSkewFlow.skewTaylor_norm_bound line 273
  22. lemma OAI.StronglyRationalVOA.LocalSkewFlow.insertedExp_tail_norm_bound line 292
  23. def OAI.StronglyRationalVOA.MobiusCoefficients.step line 319
  24. def OAI.StronglyRationalVOA.MobiusCoefficients.InRange line 324
  25. def OAI.StronglyRationalVOA.MobiusCoefficients.Nonnegative line 327
  26. def OAI.StronglyRationalVOA.MobiusCoefficients.total line 329
  27. lemma OAI.StronglyRationalVOA.MobiusCoefficients.step_single line 331
  28. lemma OAI.StronglyRationalVOA.MobiusCoefficients.total_single line 337
  29. lemma OAI.StronglyRationalVOA.MobiusCoefficients.total_step line 340
  30. lemma OAI.StronglyRationalVOA.MobiusCoefficients.step_apply line 350
  31. lemma OAI.StronglyRationalVOA.MobiusCoefficients.step_range line 359
  32. lemma OAI.StronglyRationalVOA.MobiusCoefficients.step_nonnegative line 389
  33. def OAI.StronglyRationalVOA.MobiusCoefficients.coeff line 410
  34. lemma OAI.StronglyRationalVOA.MobiusCoefficients.coeff_range line 412
  35. lemma OAI.StronglyRationalVOA.MobiusCoefficients.coeff_nonnegative line 421
  36. lemma OAI.StronglyRationalVOA.MobiusCoefficients.total_coeff line 428
  37. lemma OAI.StronglyRationalVOA.MobiusCoefficients.coeff_le_total line 437
  38. lemma OAI.StronglyRationalVOA.MobiusCoefficients.coeff_one_zero line 451
  39. def OAI.StronglyRationalVOA.MobiusCoefficients.mean line 455
  40. lemma OAI.StronglyRationalVOA.MobiusCoefficients.summable_mean line 457
  41. lemma OAI.StronglyRationalVOA.MobiusCoefficients.mean_pos line 470
  42. def OAI.StronglyRationalVOA.MobiusCoefficients.representation line 483
  43. lemma OAI.StronglyRationalVOA.MobiusCoefficients.representation_single line 485
  44. lemma OAI.StronglyRationalVOA.MobiusCoefficients.representation_step line 489
  45. lemma OAI.StronglyRationalVOA.MobiusCoefficients.representation_coeff line 500
  46. lemma OAI.StronglyRationalVOA.MobiusCoefficients.diagonal_representation line 511