OAI/RepresentationTheory/VertexAlgebra/ModuleSpectralNorms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyShift_on_grade line 13
2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.energyShift_pow_on_grade line 19
3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.exists_band_of_mem line 33
4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.energyShift_pow_norm_on_grade line 46
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.grade_orthogonalFamily line 57
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.norm_sq_eq_sum_grades line 62
7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.energy_norm_sq_eq_sum_grades line 70
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mode_images_orthogonal line 83
9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mode_norm_sq_eq_sum_grades line 91
10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.energyShift_pow_norm_mono line 116