OAI/Geometry/KahlerSplitting/FlowVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.picard_initial_variation line 33
  2. theorem OAI.UniversalCoverSplitting.commuting_field_picard_equation line 52
  3. theorem OAI.UniversalCoverSplitting.picard_endpoint_preserves_commuting_field line 88
  4. theorem OAI.UniversalCoverSplitting.exists_small_holomorphic_picard_family line 119
  5. theorem OAI.UniversalCoverSplitting.picard_endpoint_hasDerivAt line 155
  6. theorem OAI.UniversalCoverSplitting.exists_holomorphic_flow_representatives line 172
  7. theorem OAI.UniversalCoverSplitting.picard_family_fderiv_preserves line 213
  8. theorem OAI.UniversalCoverSplitting.exists_holomorphic_flow_preserving_representatives line 251
  9. structure OAI.UniversalCoverSplitting.HolomorphicFlowData line 299
  10. theorem OAI.UniversalCoverSplitting.exists_holomorphicFlowData line 313