OAI/Geometry/KahlerSplitting/Picard.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalCoverSplitting.FlowTime line 27
  2. def OAI.UniversalCoverSplitting.pathExtend line 31
  3. theorem OAI.UniversalCoverSplitting.pathExtend_apply line 35
  4. def OAI.UniversalCoverSplitting.pathPrimitive line 38
  5. theorem OAI.UniversalCoverSplitting.pathPrimitive_apply line 43
  6. theorem OAI.UniversalCoverSplitting.pathPrimitive_norm_le line 46
  7. def OAI.UniversalCoverSplitting.pathPrimitiveL line 58
  8. theorem OAI.UniversalCoverSplitting.pathPrimitiveL_apply line 71
  9. theorem OAI.UniversalCoverSplitting.pathPrimitiveL_norm_le line 74
  10. abbrev OAI.UniversalCoverSplitting.FlowPath line 86
  11. abbrev OAI.UniversalCoverSplitting.FlowParameter line 87
  12. def OAI.UniversalCoverSplitting.picardIntegral line 89
  13. def OAI.UniversalCoverSplitting.picardEquation line 92
  14. def OAI.UniversalCoverSplitting.picardBase line 96
  15. theorem OAI.UniversalCoverSplitting.picardEquation_base line 99
  16. def OAI.UniversalCoverSplitting.pathShear line 102
  17. def OAI.UniversalCoverSplitting.picardLinearTerm line 113
  18. theorem OAI.UniversalCoverSplitting.contDiffAt_picardEquation_one line 118
  19. theorem OAI.UniversalCoverSplitting.hasFDerivAt_picardEquation_base line 136
  20. theorem OAI.UniversalCoverSplitting.exists_holomorphic_picard_family line 165
  21. theorem OAI.UniversalCoverSplitting.hasFDerivAt_picardIntegral line 232
  22. theorem OAI.UniversalCoverSplitting.picard_variation_equation line 250
  23. theorem OAI.UniversalCoverSplitting.picard_linear_unique line 266
  24. def OAI.UniversalCoverSplitting.picardRealExtension line 288
  25. theorem OAI.UniversalCoverSplitting.picardRealExtension_hasDerivAt line 291
  26. theorem OAI.UniversalCoverSplitting.picardRealExtension_eq line 300
  27. def OAI.UniversalCoverSplitting.picardTimeVariation line 305
  28. theorem OAI.UniversalCoverSplitting.picardTimeVariation_equation line 316