OAI/Combinatorics/SumProduct/Alignment/ParametricSmooth01.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.AllLevelStates.State.descend_of_not_irrational line 37
  2. theorem OAI.AllLevelStates.State.exists_irrational_state line 67
  3. def OAI.AllLevelStates.initialState line 85
  4. theorem OAI.AllLevelStates.normalized_factorization_exists line 122
  5. lemma OAI.AllLevelRemovals.rightWord_ordered line 169
  6. theorem OAI.AllLevelRemovals.rightWord_residues line 182
  7. def OAI.AllLevelStates.State.reindex line 211
  8. lemma OAI.AllLevelStates.State.irrational_reindex line 225
  9. theorem OAI.AllLevelStates.State.exists_irrational_fixed_residues line 232
  10. def OAI.ParametricSmooth.family line 268
  11. def OAI.ParametricSmooth.IsPolynomial line 271
  12. lemma OAI.ParametricSmooth.constant line 274
  13. lemma OAI.ParametricSmooth.coordinate line 276
  14. lemma OAI.ParametricSmooth.parameter line 278
  15. lemma OAI.ParametricSmooth.add line 280
  16. lemma OAI.ParametricSmooth.mul line 289
  17. lemma OAI.ParametricSmooth.neg line 298
  18. lemma OAI.ParametricSmooth.sub line 301
  19. lemma OAI.ParametricSmooth.pow line 303
  20. lemma OAI.ParametricSmooth.finite_sum line 308
  21. lemma OAI.ParametricSmooth.finite_prod line 315
  22. lemma OAI.ParametricSmooth.polynomial_eval line 322
  23. lemma OAI.ParametricSmooth.mvpolynomial_eval line 326
  24. lemma OAI.ParametricSmooth.rename_parameters line 334
  25. lemma OAI.ParametricSmooth.continuous_eval line 347
  26. lemma OAI.ParametricSmooth.derivative_family line 354
  27. theorem OAI.ParametricSmooth.compact_derivative_limit line 365
  28. theorem OAI.ParametricSmooth.compact_derivative_bound line 385