OAI/Geometry/Kahler/HartogsJets.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.logarithmicBarrier line 14
  2. def OAI.PinchedHartogs.barrierX line 15
  3. def OAI.PinchedHartogs.barrierQ line 16
  4. def OAI.PinchedHartogs.barrierThird line 17
  5. def OAI.PinchedHartogs.barrierFourth line 18
  6. lemma OAI.PinchedHartogs.barrier_den_ne_zero line 20
  7. lemma OAI.PinchedHartogs.logarithmicBarrier_hasDerivAt line 23
  8. lemma OAI.PinchedHartogs.barrierX_hasDerivAt line 31
  9. lemma OAI.PinchedHartogs.barrierQ_hasDerivAt line 39
  10. lemma OAI.PinchedHartogs.barrierThird_hasDerivAt line 46
  11. lemma OAI.PinchedHartogs.barrierX_contDiffAt line 53
  12. lemma OAI.PinchedHartogs.barrierQ_contDiffAt line 56
  13. lemma OAI.PinchedHartogs.barrierThird_contDiffAt line 58
  14. lemma OAI.PinchedHartogs.logarithmicBarrier_contDiffAt line 60
  15. lemma OAI.PinchedHartogs.complexHessian_barrier line 63
  16. lemma OAI.PinchedHartogs.dz_complexHessian_real_comp line 73
  17. lemma OAI.PinchedHartogs.dbar_dz_complexHessian_real_comp line 113
  18. lemma OAI.PinchedHartogs.dz_complexHessian_barrier line 168
  19. lemma OAI.PinchedHartogs.dbar_dz_complexHessian_barrier line 202
  20. lemma OAI.PinchedHartogs.dbar_dz_real_eq_hessian line 252
  21. lemma OAI.PinchedHartogs.dz_dz_base_norm_sq line 257
  22. def OAI.PinchedHartogs.horizontalIdentity line 269
  23. def OAI.PinchedHartogs.inverseCube line 273
  24. def OAI.PinchedHartogs.inverseFourth line 274
  25. lemma OAI.PinchedHartogs.inverseSquare_hasDerivAt line 276
  26. lemma OAI.PinchedHartogs.inverseCube_hasDerivAt line 281
  27. lemma OAI.PinchedHartogs.psi_hessian_center line 293
  28. lemma OAI.PinchedHartogs.psi_third_center line 303
  29. lemma OAI.PinchedHartogs.psi_fourth_center line 320