OAI/RepresentationTheory/VertexAlgebra/ConstrainedSquareBound.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.StronglyRationalVOA.SharpCombinatorics.constrained_square_bound line 14
  2. theorem OAI.StronglyRationalVOA.SharpCombinatorics.card_tuple_sum_le line 55
  3. theorem OAI.StronglyRationalVOA.SharpCombinatorics.sum_tuple_succ line 80
  4. def OAI.StronglyRationalVOA.SharpCombinatorics.path line 90
  5. theorem OAI.StronglyRationalVOA.SharpCombinatorics.sum_path_sq_le line 97
  6. instance OAI.StronglyRationalVOA.CFTTypeVOA.energyCutoff_finite line 132
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumn line 143
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumn_apply line 150
  9. def OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumnNorm line 154
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumnNorm_nonneg line 156
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumn_norm_sq line 159
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.sum_positive_modes_sq_le line 166
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode_zero_above_cutoff line 173
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode_mem_cutoff line 183
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.positiveColumnNorm_mono line 198
  16. lemma OAI.StronglyRationalVOA.negative_binomial line 215
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.positive_mode_norm_le_column line 230
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.finsum_positive_modes_sq_eq line 243
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.negative_mode_norm_le_column line 261
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.shifted_column_sq_le line 280
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.virasoro_one_pow_mem_grade line 338
  22. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode line 351
  23. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode_inner line 355
  24. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode_mem_cutoff line 371
  25. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode_zero_above_cutoff line 383
  26. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.adjointPhysicalMode_eq line 396
  27. theorem OAI.StronglyRationalVOA.SharpColumns.sum_injective_le line 412
  28. theorem OAI.StronglyRationalVOA.SharpColumns.row_sq_le line 434
  29. theorem OAI.StronglyRationalVOA.SharpColumns.finite_sum_sq_le_card line 479
  30. theorem OAI.StronglyRationalVOA.SharpColumns.triangular_column_sq_le line 487