OAI/Geometry/Kahler/BaseDensityUpdate.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.disjoint_sum_abs_boundline 22 - lemma
OAI.PinchedHartogs.BaseConstruction.densityCorrectionRaw_value_boundline 40 - lemma
OAI.PinchedHartogs.BaseConstruction.horizontal_direction_ratioline 72 - lemma
OAI.PinchedHartogs.BaseConstruction.phase_direction_ratioline 91