OAI/Combinatorics/SumProduct/Alignment/MalcevTail03.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothBinomial.smooth_binomial_increment line 22
2. lemma OAI.MalcevTailSection.binomial_parameters_bounds line 66
3. theorem OAI.MalcevTailSection.smooth_word_bounds line 99
4. def OAI.MalcevTailSection.flowDifference line 136
5. lemma OAI.MalcevTailSection.polynomialMap_flowDifference line 140
6. lemma OAI.MalcevTailSection.flowDifference_contDiff line 147
7. theorem OAI.MalcevTailSection.flow_displacement_bounds line 155
8. theorem OAI.MalcevTailSection.smooth_word_displacement line 204
9. lemma OAI.MalcevTailFactor.error_abs line 228
10. theorem OAI.MalcevTailFactor.small_word_smooth line 237