OAI/Geometry/PolarProducts/HolomorphicBalls.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SingularComparison.exists_inner_radius line 33
  2. theorem OAI.SingularComparison.outer_comparison line 58
  3. theorem OAI.SingularComparison.radius_bound line 67
  4. theorem OAI.ComplexPotential.exists_ball_from_logarithmic_pole line 98
  5. def OAI.TensorCalculus.pullbackOneForm line 230
  6. theorem OAI.TensorCalculus.pullbackOneForm_apply line 233
  7. theorem OAI.TensorCalculus.fderiv_pullbackOneForm line 236
  8. theorem OAI.TensorCalculus.exteriorD_pullbackOneForm line 250
  9. theorem OAI.ComplexPotential.dc_comp line 276
  10. theorem OAI.ComplexPotential.ddc_comp line 284
  11. def OAI.ComplexPotential.complexStructure line 311
  12. theorem OAI.ComplexPotential.complexStructure_apply line 314
  13. theorem OAI.ComplexPotential.complexStructure_sq line 316
  14. theorem OAI.ComplexPotential.complexStructure_norm line 319
  15. theorem OAI.ComplexPotential.fderiv_commutes_complexStructure line 322
  16. theorem OAI.ComplexPotential.complexStructure_skew line 328
  17. theorem OAI.ComplexPotential.IsPSHAt.holomorphic_comp line 335