OAI/Geometry/Kahler/BaseRadialPatch.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.bracketUnit line 19
2. lemma OAI.PinchedHartogs.BaseConstruction.bracketUnit_continuous line 21
3. lemma OAI.PinchedHartogs.BaseConstruction.bracketUnit_coe line 24
4. lemma OAI.PinchedHartogs.BaseConstruction.bracketUnit_preserves line 27
5. lemma OAI.PinchedHartogs.BaseConstruction.peakPatch_iff_radial line 31
6. lemma OAI.PinchedHartogs.BaseConstruction.densityHeight_radial line 42
7. lemma OAI.PinchedHartogs.BaseConstruction.radial_patch_integral line 47
8. lemma OAI.PinchedHartogs.BaseConstruction.log_radial_substitution_real line 86
9. lemma OAI.PinchedHartogs.BaseConstruction.radial_patch_integral_exp line 96