OAI/Geometry/Kahler/HartogsTransferTools.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PinchedHartogs.liftBaseMapline 17 - lemma
OAI.PinchedHartogs.liftBaseMap_analyticAtline 19 - lemma
OAI.PinchedHartogs.fderiv_liftBaseMapline 24 - lemma
OAI.PinchedHartogs.baseHessian_value_compline 32 - lemma
OAI.PinchedHartogs.chartWeight_contDiffAtline 47 - lemma
OAI.PinchedHartogs.chartControl_pshline 53 - lemma
OAI.PinchedHartogs.euclidean_q_baseline 68 - lemma
OAI.PinchedHartogs.form_q_baseline 75 - lemma
OAI.PinchedHartogs.chartControl_form_boundsline 85 - lemma
OAI.PinchedHartogs.chartJets_lifted_boundsline 96