OAI/AlgebraicGeometry/Seshadri/Interpolation/InitialBasis.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Interpolation.DerivativeSummable.zero line 13
2. lemma OAI.MaximalSeshadri.Interpolation.DerivativeSummable.add line 19
3. lemma OAI.MaximalSeshadri.Interpolation.DerivativeSummable.smul line 33
4. def OAI.MaximalSeshadri.Interpolation.derivativeSeriesSubmodule line 43
5. theorem OAI.MaximalSeshadri.Interpolation.exists_commonDerivativeRadius line 49
6. def OAI.MaximalSeshadri.Interpolation.seriesPartialMap line 75
7. def OAI.MaximalSeshadri.Interpolation.seriesJetMap line 88
8. lemma OAI.MaximalSeshadri.Interpolation.seriesJetMap_eq line 97
9. def OAI.MaximalSeshadri.Interpolation.LexInitial line 108
10. lemma OAI.MaximalSeshadri.Interpolation.exponentWeight_nonneg line 113
11. lemma OAI.MaximalSeshadri.Interpolation.exponentWeight_mono line 116
12. lemma OAI.MaximalSeshadri.Interpolation.continuous_exponentWeight line 121
13. lemma OAI.MaximalSeshadri.Interpolation.finite_boundedWeight line 125
14. lemma OAI.MaximalSeshadri.Interpolation.LexInitial.beta_lt_of_eq_weight line 138
15. theorem OAI.MaximalSeshadri.Interpolation.exists_strictWeight_of_lex line 150
16. def OAI.MaximalSeshadri.Interpolation.lexKey line 202
17. lemma OAI.MaximalSeshadri.Interpolation.lexKey_le_iff line 205
18. lemma OAI.MaximalSeshadri.Interpolation.lexKey_injective line 210
19. lemma OAI.MaximalSeshadri.Interpolation.LexInitial.key_le line 220
20. lemma OAI.MaximalSeshadri.Interpolation.LexInitial.unique line 224
21. theorem OAI.MaximalSeshadri.Interpolation.exists_lexInitial line 228
22. theorem OAI.MaximalSeshadri.Interpolation.linearIndependent_of_lexInitial line 249