OAI/Combinatorics/SumProduct/Alignment/SmoothBinomial01.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MalcevTailSection.flowWord line 26
  2. lemma OAI.MalcevTailSection.polynomialMap_section line 29
  3. lemma OAI.MalcevTailSection.polynomialMap_flowWord line 43
  4. lemma OAI.MalcevTailSection.flowWord_contDiff line 54
  5. lemma OAI.MalcevTailSection.flowWord_bounds line 62
  6. lemma OAI.MalcevTailSection.flowWord_integer line 81
  7. def OAI.SmoothBinomial.universal line 112
  8. def OAI.SmoothBinomial.family line 116
  9. lemma OAI.SmoothBinomial.continuous_eval_family line 119
  10. lemma OAI.SmoothBinomial.iteratedDeriv_eval line 126
  11. lemma OAI.SmoothBinomial.iterate_derivative_family line 135
  12. theorem OAI.SmoothBinomial.compact_derivative_limit line 146
  13. lemma OAI.SmoothBinomial.universal_eval line 182
  14. lemma OAI.SmoothBinomial.universal_eval_zero line 192
  15. lemma OAI.SmoothBinomial.choose_eq_product line 196
  16. lemma OAI.SmoothBinomial.scale_identity line 202
  17. lemma OAI.SmoothBinomial.amplitude_identity line 216
  18. theorem OAI.SmoothBinomial.smooth_binomial_limit line 224
  19. theorem OAI.SmoothBinomial.smooth_binomial_bounds line 248