OAI/RepresentationTheory/VertexAlgebra/ModuleCutoffs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyCutoff line 14
  2. instance OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyCutoff_finite line 16
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.grade_le_energyCutoff line 21
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyCutoff_mono line 25
  5. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.bandComponent line 31
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.bandComponent_mem line 33
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffProjection line 36
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffProjection_apply line 39
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffProjection_on_grade line 43
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffProjection_of_mem line 57
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.cutoffProjection_mem line 67
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.band_orthogonalFamily line 78
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.norm_sq_eq_sum_cutoff line 86
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.energy_norm_sq_eq_sum_cutoff line 95
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.energyShift_pow_norm_on_cutoff line 110
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mode_norm_sq_eq_sum_cutoff line 124
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.physicalMode_zero_above_cutoff line 149
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.physicalMode_mem_cutoff line 158