OAI/Geometry/Kahler/BasePhaseAveraging.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.BaseConstruction.phase_mean_derivative line 19
2. lemma OAI.PinchedHartogs.BaseConstruction.phase_average_product line 31
3. def OAI.PinchedHartogs.BaseConstruction.phaseAction line 44
4. lemma OAI.PinchedHartogs.BaseConstruction.phaseAction_coe line 46
5. lemma OAI.PinchedHartogs.BaseConstruction.phaseAction_continuous line 48
6. lemma OAI.PinchedHartogs.BaseConstruction.sigma_phase_average line 52
7. lemma OAI.PinchedHartogs.BaseConstruction.sigma_root_average line 63