OAI/Geometry/KahlerSplitting/PathDerivatives.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniversalCoverSplitting.chart_mfderiv_inverses line 28
2. lemma OAI.UniversalCoverSplitting.projectionInChart_self line 48
3. lemma OAI.UniversalCoverSplitting.projectionInChart_idempotent line 65
4. lemma OAI.UniversalCoverSplitting.projectionInChart_complement line 79
5. theorem OAI.UniversalCoverSplitting.uniform_strict_derivative_on_compact line 103
6. def OAI.UniversalCoverSplitting.pathLinearApply line 177
7. theorem OAI.UniversalCoverSplitting.pathLinearApply_apply line 190
8. def OAI.UniversalCoverSplitting.pathDerivative line 193
9. theorem OAI.UniversalCoverSplitting.hasStrictFDerivAt_pathCompose line 198
10. theorem OAI.UniversalCoverSplitting.pathLinearApply_norm_le line 235
11. def OAI.UniversalCoverSplitting.pathLinearApplyL line 245
12. theorem OAI.UniversalCoverSplitting.pathLinearApplyL_apply line 252
13. theorem OAI.UniversalCoverSplitting.contDiffAt_pathCompose_one line 255