OAI/Geometry/Kahler/BasePatchPhase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.BaseConstruction.phaseAction_patch line 19
2. lemma OAI.PinchedHartogs.BaseConstruction.sigma_phase_average_restrict line 25
3. lemma OAI.PinchedHartogs.BaseConstruction.circle_regularized_shifted_moments line 58
4. lemma OAI.PinchedHartogs.BaseConstruction.densityCorrection_constant_phase line 67
5. lemma OAI.PinchedHartogs.BaseConstruction.ideal_patch_phase_mean line 89