OAI/RepresentationTheory/VertexAlgebra/MobiusExistence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.derivative_pos_of_rel line 9
  2. def OAI.StronglyRationalVOA.CircleMobiusGeometry.dot line 47
  3. def OAI.StronglyRationalVOA.CircleMobiusGeometry.cross line 50
  4. def OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLiftFun line 53
  5. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLiftFun_rel line 55
  6. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.dot_smooth line 67
  7. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.cross_smooth line 72
  8. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLiftFun_smooth line 77
  9. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLiftFun_period line 80
  10. def OAI.StronglyRationalVOA.SmoothCircleLift.ofFunction line 96
  11. lemma OAI.StronglyRationalVOA.SmoothCircleLift.ofFunction_apply line 123
  12. def OAI.StronglyRationalVOA.CircleMobiusGeometry.positiveLift line 129
  13. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.implements_positiveLift line 133