OAI/Combinatorics/SumProduct/Alignment/RoughLog01.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RoughCoefficientDescentBridge.PositiveGrid line 33
2. lemma OAI.RoughCoefficientDescentBridge.totalDegree_le line 35
3. lemma OAI.RoughCoefficientDescentBridge.circleNorm_nearInteger line 41
4. lemma OAI.RoughCoefficientDescentBridge.positive_peeling line 44
5. def OAI.RoughCoefficientDescentBridge.descentInput line 68
6. theorem OAI.RoughCoefficientDescentBridge.eventual_multivariate_coefficients line 112
7. def OAI.RoughLogPolynomialAdaptation.filtration line 176
8. lemma OAI.RoughLogPolynomialAdaptation.level_zero line 181
9. lemma OAI.RoughLogPolynomialAdaptation.level_one line 183
10. instance OAI.RoughLogPolynomialAdaptation.level_normal line 186
11. lemma OAI.RoughLogPolynomialAdaptation.level_terminal line 190
12. theorem OAI.RoughLogPolynomialAdaptation.coordinate_adapted line 202
13. def OAI.RoughLogPolynomialAdaptation.intCastVector line 225
14. lemma OAI.RoughLogPolynomialAdaptation.restrict_integer line 231
15. theorem OAI.RoughLogPolynomialAdaptation.logarithmic_adapted line 241