OAI/RepresentationTheory/VertexAlgebra/ColumnControl.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.ColumnControl line 15
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnControl_subset line 19
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.AdjointColumnControl line 33
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointColumnControl_subset line 37
  5. def OAI.StronglyRationalVOA.CFTTypeVOA.normalLeft line 51
  6. def OAI.StronglyRationalVOA.CFTTypeVOA.normalRightHigh line 55
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.normalRightLow line 59
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalLeft_mem_cutoff line 63
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalRightHigh_mem_cutoff line 74
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalRightLow_mem_cutoff line 83
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalLeft_sq_le line 95
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalRightHigh_sq_le line 116
  13. theorem OAI.StronglyRationalVOA.SharpColumns.norm_add_add_sub_sq_le line 155
  14. theorem OAI.StronglyRationalVOA.SharpColumns.sum_columns_sq_le line 160
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normalRightLow_column_sq_le line 177
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.normal_product_cutoff_split line 212
  17. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpCorrectionMass line 248
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sharpCorrectionMass_nonneg line 252
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.singular_correction_column_sq_le line 256
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnControl_mono line 293
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnControl_mode_sq_le line 298
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalProduct_columnControl line 306
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.normalProduct_zero_sq_le line 345
  24. theorem OAI.StronglyRationalVOA.SharpColumns.norm_add_sq_le_two line 374
  25. def OAI.StronglyRationalVOA.CFTTypeVOA.ColumnGrowth line 385
  26. def OAI.StronglyRationalVOA.CFTTypeVOA.ZeroGrowth line 390
  27. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnGrowth_zero line 394
  28. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_zero line 399
  29. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnGrowth_add line 404
  30. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_add line 421
  31. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnGrowth_smul line 433
  32. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_smul line 441
  33. theorem OAI.StronglyRationalVOA.CFTTypeVOA.columnGrowth_mono line 449
  34. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_mono line 459
  35. theorem OAI.StronglyRationalVOA.CFTTypeVOA.zeroGrowth_of_columnGrowth line 471
  36. def OAI.StronglyRationalVOA.CFTTypeVOA.SharpDegreeGrowth line 478
  37. def OAI.StronglyRationalVOA.CFTTypeVOA.SharpGrowth line 481
  38. def OAI.StronglyRationalVOA.CFTTypeVOA.sharpGrowthSubmodule line 484
  39. theorem OAI.StronglyRationalVOA.CFTTypeVOA.finite_columnGrowth_uniform line 490