OAI/Geometry/Kahler/BaseRadialMoments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.BaseConstruction.hasDerivAt_sphere_integral line 20
  2. def OAI.PinchedHartogs.BaseConstruction.rotA line 37
  3. def OAI.PinchedHartogs.BaseConstruction.rotA' line 38
  4. def OAI.PinchedHartogs.BaseConstruction.rotA'' line 39
  5. lemma OAI.PinchedHartogs.BaseConstruction.rotA_deriv line 41
  6. lemma OAI.PinchedHartogs.BaseConstruction.rotA'_deriv line 48
  7. lemma OAI.PinchedHartogs.BaseConstruction.rotated_radialU line 54
  8. def OAI.PinchedHartogs.BaseConstruction.rotF line 60
  9. def OAI.PinchedHartogs.BaseConstruction.rotF' line 61
  10. def OAI.PinchedHartogs.BaseConstruction.rotF'' line 63
  11. lemma OAI.PinchedHartogs.BaseConstruction.rotF_deriv line 68
  12. lemma OAI.PinchedHartogs.BaseConstruction.rotF'_deriv line 74
  13. lemma OAI.PinchedHartogs.BaseConstruction.rotF_continuous line 83
  14. lemma OAI.PinchedHartogs.BaseConstruction.rotF'_continuous line 86
  15. lemma OAI.PinchedHartogs.BaseConstruction.rotF''_continuous line 89
  16. lemma OAI.PinchedHartogs.BaseConstruction.radial_moment_recurrence line 93
  17. lemma OAI.PinchedHartogs.BaseConstruction.radial_first_moment line 145
  18. lemma OAI.PinchedHartogs.BaseConstruction.radial_moment line 157