OAI/Geometry/Kahler/BaseWeightedDerivative.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.BaseConstruction.bounded_half_plane line 22
2. def OAI.PinchedHartogs.BaseConstruction.expSum line 35
3. lemma OAI.PinchedHartogs.BaseConstruction.expSum_differentiable line 38
4. def OAI.PinchedHartogs.BaseConstruction.dampedSum line 43
5. lemma OAI.PinchedHartogs.BaseConstruction.half_plane_norm_one_add line 46
6. lemma OAI.PinchedHartogs.BaseConstruction.dampedSum_bound line 51
7. lemma OAI.PinchedHartogs.BaseConstruction.dampedSum_diffCont line 70
8. lemma OAI.PinchedHartogs.BaseConstruction.dampedSum_eq line 84
9. lemma OAI.PinchedHartogs.BaseConstruction.dampedSum_imag_norm line 99
10. lemma OAI.PinchedHartogs.BaseConstruction.dampedSum_boundary line 109
11. lemma OAI.PinchedHartogs.BaseConstruction.expSum_upper_bound line 126
12. lemma OAI.PinchedHartogs.BaseConstruction.expSum_neg_frequencies line 162
13. lemma OAI.PinchedHartogs.BaseConstruction.expSum_disk_bound line 171
14. lemma OAI.PinchedHartogs.BaseConstruction.expSum_second_derivative_bound line 186