OAI/Geometry/Kahler/HartogsErrorBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.normalError_HHHH line 17
2. lemma OAI.PinchedHartogs.normalError_HHHV line 36
3. lemma OAI.PinchedHartogs.componentNorm_bound line 59
4. lemma OAI.PinchedHartogs.horizontalPart4_bound line 73
5. lemma OAI.PinchedHartogs.horizontalPart3_bound line 80
6. lemma OAI.PinchedHartogs.matrix_triple_sum_bound line 92
7. lemma OAI.PinchedHartogs.scaled_inverse_contraction_bound line 112
8. lemma OAI.PinchedHartogs.normalErrors_bounds line 130