OAI/Geometry/KahlerSplitting/FormDerivatives.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalCoverSplitting.differentiableAt_intervalIntegral_of_continuous_deriv line 38
  2. theorem OAI.UniversalCoverSplitting.differentiableOn_weighted_curveIntegral line 66
  3. theorem OAI.UniversalCoverSplitting.differentiableOn_partial_deriv line 95
  4. theorem OAI.UniversalCoverSplitting.differentiableOn_partial_deriv_open line 131
  5. theorem OAI.UniversalCoverSplitting.differentiableOn_fderiv_apply_open line 144
  6. theorem OAI.UniversalCoverSplitting.holomorphic_twoDim_contDiffOn_nat line 181
  7. theorem OAI.UniversalCoverSplitting.holomorphic_twoDim_contDiffOn line 192
  8. def OAI.UniversalCoverSplitting.pullbackMetric line 204
  9. def OAI.UniversalCoverSplitting.pullbackKahler line 210
  10. theorem OAI.UniversalCoverSplitting.pullbackKahler_apply line 215
  11. theorem OAI.UniversalCoverSplitting.chart_derivative_twoDim line 229
  12. theorem OAI.UniversalCoverSplitting.pullbackKahler_eq_chart line 239
  13. theorem OAI.UniversalCoverSplitting.pullbackKahler_closed line 262
  14. theorem OAI.UniversalCoverSplitting.KahlerMetric.contDiff_metricInChart line 310
  15. theorem OAI.UniversalCoverSplitting.exists_smooth_chart_twoDim line 318
  16. theorem OAI.UniversalCoverSplitting.pullbackMetric_apply_eq_chart line 339
  17. theorem OAI.UniversalCoverSplitting.pullbackMetric_smooth line 351
  18. theorem OAI.UniversalCoverSplitting.pullbackKahler_smooth line 374
  19. def OAI.UniversalCoverSplitting.realPullbackKahler line 390
  20. theorem OAI.UniversalCoverSplitting.realPullbackKahler_as_bilinear line 394
  21. theorem OAI.UniversalCoverSplitting.realPullbackKahler_smooth line 405
  22. theorem OAI.UniversalCoverSplitting.realPullbackKahler_closed line 424
  23. theorem OAI.UniversalCoverSplitting.realPullbackKahler_apply line 439
  24. theorem OAI.UniversalCoverSplitting.KahlerMetric.moving_flux_nonpos line 452
  25. theorem OAI.UniversalCoverSplitting.KahlerMetric.radial_angular_density line 476