OAI/Geometry/Kahler/BasePhaseSupport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.phaseBand line 22
2. lemma OAI.PinchedHartogs.BaseConstruction.mem_phaseBand line 23
3. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_extend line 25
4. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_band line 34
5. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_mono line 43
6. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_add line 49
7. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_zero line 58
8. lemma OAI.PinchedHartogs.BaseConstruction.phaseBandwidth_sum line 62
9. lemma OAI.PinchedHartogs.BaseConstruction.phaseChar_conj line 71
10. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_shift line 76
11. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_negshift line 87
12. lemma OAI.PinchedHartogs.BaseConstruction.phaseSum_union line 98
13. lemma OAI.PinchedHartogs.BaseConstruction.positive_shift_disjoint line 112