[Merged by Bors] - feat(Analysis/Calculus/DSlope): add eq_smul_dslope_of_zero and iterated version#37923
Conversation
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 14ec76b5f0Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
Apply suggestion from wwylele to simplify proof using sub_smul_dslope Co-authored-by: Weiyi Wang <wwylele@gmail.com>
There was a problem hiding this comment.
these seem a bit niche. Why do you want them? (sorry, this is in the PR description)
Also, given some weird things I noticed, and your username, I have to ask: are you a bot? Is this PR LLM-generated? If so, it should be marked with that tag and disclosed in the PR description.
j-loreaux
added
the
awaiting-author
|
@j-loreaux To answer your question: No, I am not a bot, but I am a human developer using LLMs (specifically Harmonic's Aristotle and Google's Gemini) to assist me in formalizing these theorems. I apologize for not disclosing this initially and for accidentally leaving a Japanese comment in the code. I have updated the PR description to mention the LLM assistance. Could you please add the I completely agree with all your code suggestions. The I will apply these changes to my local branch and push the updates shortly. Thank you again for your guidance! |
wwylele
left a comment
wwylele
left a comment
There was a problem hiding this comment.
Why did the code regress? If you are blindly asking LLM to update the code without understanding it, this is wasting reviewers' time
wwylele
left a comment
wwylele
left a comment
There was a problem hiding this comment.
Likewise, this has also regressed
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
j-loreaux
added
the
LLM-generated
…ated version (#37923) This PR adds two fundamental algebraic identities connecting a function with its `dslope` when the base point is a root: * `eq_smul_dslope_of_zero`: `f b = (b - a) • dslope f a b` when `f a = 0`. * `eq_pow_smul_iterate_dslope_of_zero`: The iterated version `f b = (b - a) ^ n • (Function.swap dslope a)^[n] f b` when the first `n-1` iterated dslopes vanish at `a`. These lemmas are essential for factoring out removable singularities locally. This PR was assisted by LLMs (Aristotle and Gemini). Co-authored-by: e-271828 <f_s@har.bbiq.jp>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
eq_smul_dslope_of_zero and iterated versioneq_smul_dslope_of_zero and iterated version
3 participants
This PR adds two fundamental algebraic identities connecting a function with its
dslopewhen the base point is a root:eq_smul_dslope_of_zero:f b = (b - a) • dslope f a bwhenf a = 0.eq_pow_smul_iterate_dslope_of_zero: The iterated versionf b = (b - a) ^ n • (Function.swap dslope a)^[n] f bwhen the firstn-1iterated dslopes vanish ata.These lemmas are essential for factoring out removable singularities locally.
This PR was assisted by LLMs (Aristotle and Gemini).