OAI/RepresentationTheory/VertexAlgebra/ModuleColumnOperators.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumn line 14
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumn_apply line 21
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumnNorm line 25
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumnNorm_nonneg line 27
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumn_norm_sq line 30
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.sum_positive_modes_sq_le line 37
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.positiveColumnNorm_mono line 44
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.positive_mode_norm_le_column line 62
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.finsum_positive_modes_sq_eq line 75
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.negative_mode_norm_le_column line 89
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.shifted_column_sq_le line 108
  12. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode line 159
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode_inner line 163
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode_mem_cutoff line 179
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode_zero_above_cutoff line 191
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointPhysicalMode_eq line 204