OAI/Geometry/Kahler/BasePhaseFourier.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.phaseChar line 20
2. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_mul line 22
3. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_zero line 24
4. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_one line 25
5. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_add line 26
6. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_exp line 28
7. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_continuous line 32
8. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_norm line 34
9. lemma OAI.PinchedHartogs.BaseConstruction.circle_char_mean line 36
10. lemma OAI.PinchedHartogs.BaseConstruction.circle_char_prod_mean line 50
11. def OAI.PinchedHartogs.BaseConstruction.phaseSum line 55
12. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_continuous line 57
13. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_mean line 60
14. def OAI.PinchedHartogs.BaseConstruction.PhaseBandwidth line 68
15. def OAI.PinchedHartogs.BaseConstruction.OrbitMeanOne line 72
16. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_one line 75
17. lemma OAI.PinchedHartogs.BaseConstruction.orbitMean_one line 81