OAI/Geometry/Kahler/BaseDensityDefinitions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.BaseConstruction.phaseDerivative line 20
  2. def OAI.PinchedHartogs.BaseConstruction.centralPoint line 22
  3. def OAI.PinchedHartogs.BaseConstruction.densityHeight line 25
  4. def OAI.PinchedHartogs.BaseConstruction.densityCorrectionRaw line 28
  5. def OAI.PinchedHartogs.BaseConstruction.densityCorrection line 35
  6. def OAI.PinchedHartogs.BaseConstruction.density line 38
  7. lemma OAI.PinchedHartogs.BaseConstruction.phaseDerivative_smooth line 43
  8. lemma OAI.PinchedHartogs.BaseConstruction.centralPoint_smoothAt line 47
  9. lemma OAI.PinchedHartogs.BaseConstruction.densityHeight_smoothAt line 55
  10. lemma OAI.PinchedHartogs.BaseConstruction.densityCorrectionRaw_smoothAt line 60
  11. lemma OAI.PinchedHartogs.BaseConstruction.densityCorrection_zero_low line 78
  12. lemma OAI.PinchedHartogs.BaseConstruction.densityCorrection_smooth line 95
  13. lemma OAI.PinchedHartogs.BaseConstruction.density_smooth line 116