OAI/Geometry/Kahler/BaseLogFactor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.logFactor line 19
2. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_discriminant line 22
3. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_one_le line 26
4. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_pos line 33
5. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_gt line 35
6. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_equation line 41
7. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_norm_identity line 50
8. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_zero line 64
9. lemma OAI.PinchedHartogs.BaseConstruction.logFactor_continuous line 72
10. lemma OAI.PinchedHartogs.BaseConstruction.circle_log_continuous line 76
11. lemma OAI.PinchedHartogs.BaseConstruction.regularized_circle_moments line 88