OAI/Geometry/KahlerSplitting/Boxes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalCoverSplitting.IsBox line 13
2. def OAI.UniversalCoverSplitting.hartogsFigure line 22
3. def OAI.UniversalCoverSplitting.hartogsEnvelope line 26
4. def OAI.UniversalCoverSplitting.HartogsBoxExtension line 29
5. theorem OAI.UniversalCoverSplitting.mixed_direction_identity line 45
6. theorem OAI.UniversalCoverSplitting.mixed_direction_norm_le line 60
7. theorem OAI.UniversalCoverSplitting.exists_quadratic_operator_bound line 92