OAI/Geometry/Kahler/HartogsFrame.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.normalIndexEquiv line 17
  2. lemma OAI.PinchedHartogs.sum_normalIndex line 32
  3. def OAI.PinchedHartogs.normalFrameEquiv line 35
  4. lemma OAI.PinchedHartogs.normalFrame_coordinates line 40
  5. lemma OAI.PinchedHartogs.tensorValue_normalFrame line 48
  6. lemma OAI.PinchedHartogs.hermitianValue_normalFrame line 57
  7. lemma OAI.PinchedHartogs.normalPotential_frame_metric line 70
  8. lemma OAI.PinchedHartogs.normalPotential_sectional line 84
  9. def OAI.PinchedHartogs.metricErrorConstant line 97
  10. def OAI.PinchedHartogs.metricThreshold line 98
  11. lemma OAI.PinchedHartogs.metricThreshold_pos line 100
  12. lemma OAI.PinchedHartogs.normalPotentials_uniform_pinching line 103