OAI/Geometry/Kahler/BaseProfiles.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PinchedHartogs.BaseConstruction.cosh_strict_quadratic line 20
  2. lemma OAI.PinchedHartogs.BaseConstruction.exists_profile_amplitude line 26
  3. lemma OAI.PinchedHartogs.BaseConstruction.profile_transition_width line 37
  4. def OAI.PinchedHartogs.BaseConstruction.leftCut line 55
  5. def OAI.PinchedHartogs.BaseConstruction.rightCut line 57
  6. lemma OAI.PinchedHartogs.BaseConstruction.leftCut_smooth line 60
  7. lemma OAI.PinchedHartogs.BaseConstruction.rightCut_smooth line 62
  8. lemma OAI.PinchedHartogs.BaseConstruction.leftCut_bounds line 66
  9. lemma OAI.PinchedHartogs.BaseConstruction.rightCut_bounds line 69
  10. lemma OAI.PinchedHartogs.BaseConstruction.leftCut_one line 79
  11. lemma OAI.PinchedHartogs.BaseConstruction.leftCut_zero line 82
  12. lemma OAI.PinchedHartogs.BaseConstruction.rightCut_zero_left line 85
  13. lemma OAI.PinchedHartogs.BaseConstruction.rightCut_zero_right line 87
  14. lemma OAI.PinchedHartogs.BaseConstruction.rightCut_one line 89
  15. lemma OAI.PinchedHartogs.BaseConstruction.integral_exp_neg_interval line 94
  16. lemma OAI.PinchedHartogs.BaseConstruction.cutoff_negative_mass line 97
  17. lemma OAI.PinchedHartogs.BaseConstruction.cutoff_positive_mass line 111
  18. def OAI.PinchedHartogs.BaseConstruction.profilePrimitive line 126
  19. lemma OAI.PinchedHartogs.BaseConstruction.profilePrimitive_deriv line 129
  20. lemma OAI.PinchedHartogs.BaseConstruction.profilePrimitive_smooth line 141
  21. lemma OAI.PinchedHartogs.BaseConstruction.profilePrimitive_zero line 153
  22. lemma OAI.PinchedHartogs.BaseConstruction.profilePrimitive_tail line 155
  23. structure OAI.PinchedHartogs.BaseConstruction.RadialProfiles line 172
  24. lemma OAI.PinchedHartogs.BaseConstruction.exists_radialProfiles line 196