OAI/RepresentationTheory/VertexAlgebra/ModuleMobiusEstimates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.mobiusGenerator line 14
2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.virasoro_neg_one_norm_on_band line 21
3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mode_norm_on_cutoff_of_band line 35
4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.virasoro_one_norm_cutoff line 47
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.virasoro_neg_one_norm_cutoff line 55
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusGenerator_mem_energyCutoff line 63
7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusGenerator_pow_mem_energyCutoff line 70
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusGenerator_skew line 79
9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusGenerator_norm_cutoff line 86
10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusGenerator_pow_norm line 97
11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.mobiusTaylor_mem_energyCutoff line 110