OAI/Geometry/Kahler/BaseCircleLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.BaseConstruction.circle_real_char_mean line 19
2. lemma OAI.PinchedHartogs.BaseConstruction.circle_real_char_cos line 25
3. lemma OAI.PinchedHartogs.BaseConstruction.hasSum_circle_log line 36
4. lemma OAI.PinchedHartogs.BaseConstruction.circle_log_moments line 60