OAI/Geometry/KahlerSplitting/MovingStokes.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.alternatingEvalCLM line 32
  2. abbrev OAI.UniversalCoverSplitting.Real3 line 39
  3. def OAI.UniversalCoverSplitting.realBasis3 line 41
  4. def OAI.UniversalCoverSplitting.stokesCoefficient line 43
  5. def OAI.UniversalCoverSplitting.stokesCoefficientDeriv line 46
  6. theorem OAI.UniversalCoverSplitting.stokesCoefficient_hasFDerivAt line 50
  7. theorem OAI.UniversalCoverSplitting.sum_stokesCoefficientDeriv_eq_extDeriv line 56
  8. theorem OAI.UniversalCoverSplitting.sum_faces_eq_zero_of_closed_twoForm line 63
  9. theorem OAI.UniversalCoverSplitting.first_face_integral_le_of_closed line 100
  10. def OAI.UniversalCoverSplitting.movingPolar line 135
  11. theorem OAI.UniversalCoverSplitting.movingPolar_contDiffOn line 138
  12. theorem OAI.UniversalCoverSplitting.movingPolar_fderiv_apply line 151
  13. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_zero line 171
  14. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_one line 178
  15. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_two line 185
  16. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_zero' line 192
  17. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_one' line 199
  18. theorem OAI.UniversalCoverSplitting.movingPolar_deriv_two' line 206
  19. def OAI.UniversalCoverSplitting.movingKahlerForm line 220
  20. theorem OAI.UniversalCoverSplitting.movingKahlerForm_zero line 224
  21. theorem OAI.UniversalCoverSplitting.movingKahlerForm_one line 248
  22. theorem OAI.UniversalCoverSplitting.movingKahlerForm_one_zero_radius line 275
  23. theorem OAI.UniversalCoverSplitting.movingKahlerForm_one_nonneg line 281
  24. theorem OAI.UniversalCoverSplitting.movingKahlerForm_two_eq line 311
  25. theorem OAI.UniversalCoverSplitting.moving_disk_face_monotone line 337