[Merged by Bors] - feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 #33312
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PR summary adde41efa9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-merge-conflict-bot
added
the
merge-conflict
Collaborator
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
… into IterateMulPow
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
…s/mathlib4 into ChebyshevDerivative1a
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
Collaborator
Vierkantor
approved these changes
Jan 16, 2026
Contributor
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
All the code in here looks good to me 🎉 I have not worked with this file at all so I feel like I'm missing too much of the context to give a definitive say.
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Vierkantor. |
leanprover-community-mathlib4-bot
added
the
maintainer-merge
Contributor
|
bors r+ |
leanprover-community-mathlib4-bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 16, 2026
…d U at 1 (#33312) The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`. These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero. In principle, by combining with #33311, one can compute the explicit formula for the derivative at zero. A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
eliasjudin
pushed a commit
to eliasjudin/mathlib4
that referenced
this pull request
Jan 18, 2026
…d U at 1 (leanprover-community#33312) The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`. These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero. In principle, by combining with leanprover-community#33311, one can compute the explicit formula for the derivative at zero. A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
bilichboris
pushed a commit
to bilichboris/mathlib4
that referenced
this pull request
Jan 18, 2026
…d U at 1 (leanprover-community#33312) The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`. These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero. In principle, by combining with leanprover-community#33311, one can compute the explicit formula for the derivative at zero. A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
goliath-klein
pushed a commit
to PrParadoxy/mathlib4
that referenced
this pull request
Jan 24, 2026
…d U at 1 (leanprover-community#33312) The main results are `iterate_derivative_T_eval_one` and `iterate_derivative_U_eval_one`. These are derived using recurrences which for at every point, and in particular, `iterate_derivative_T_eval_zero` and `iterate_derivative_U_eval_zero` gives the recurrences at zero. In principle, by combining with leanprover-community#33311, one can compute the explicit formula for the derivative at zero. A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main results are
iterate_derivative_T_eval_oneanditerate_derivative_U_eval_one.These are derived using recurrences which for at every point, and in particular,
iterate_derivative_T_eval_zeroanditerate_derivative_U_eval_zerogives the recurrences at zero.In principle, by combining with #33311, one can compute the explicit formula for the derivative at zero.
A subsequent PR will derive consequences for these polynomials over the reals (these should work for every field).
The file is getting rather long — not sure what to do about it.