OAI/Geometry/Kahler/BaseAdaptedHopf.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.adaptedHopf line 20
2. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_continuous line 23
3. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_integral line 26
4. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_bracket line 31
5. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_bracket_norm line 36
6. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_phase line 40
7. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_height line 45
8. lemma OAI.PinchedHartogs.BaseConstruction.adaptedHopf_correction_expansion line 50
9. lemma OAI.PinchedHartogs.BaseConstruction.phase_shifted_real_moment line 77