OAI/RepresentationTheory/VertexAlgebra/MobiusStandardTopology.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.continuous_entry line 9
2. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.constant_continuous line 11
3. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.cosine_continuous line 14
4. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.sine_continuous line 17
5. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.density_smooth_standard line 20
6. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.density_derivative_continuous line 24
7. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.continuous_of_implements line 47
8. def OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveMatrices line 83
9. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLift_continuous line 84
10. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.dot_continuous line 98
11. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.dot_periodic line 101
12. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.dot_one line 106
13. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.one_mem_positiveMatrices line 111
14. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveMatrices_mem_nhds_one line 113
15. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.standardAction_continuousAt_one line 133
16. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.group_continuous_mul_right line 145
17. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.standardAction_continuous line 153
18. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.projectiveStandardAction_continuous line 163