Skip to content

[Merged by Bors] - feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain#26985

Closed
agjftucker wants to merge 44 commits intoleanprover-community:masterfrom
agjftucker:agjftucker/implicit
Closed

[Merged by Bors] - feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain#26985
agjftucker wants to merge 44 commits intoleanprover-community:masterfrom
agjftucker:agjftucker/implicit

Conversation

@agjftucker
Copy link
Copy Markdown
Collaborator

@agjftucker agjftucker commented Jul 11, 2025 •
edited
Loading

@agjftucker agjftucker mentioned this pull request Jul 11, 2025
Closed
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2025
@agjftucker agjftucker force-pushed the agjftucker/implicit branch from c69cc5f to 8dc672d Compare July 11, 2025 13:51
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 11, 2025 •
edited
Loading

PR summary 83a9b27e0d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Calculus.ImplicitContDiff 1
Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (new file) 2044

Declarations diff

+ eventually_apply_eq_iff_implicitFunction
+ eventually_apply_eq_iff_implicitFunctionOfProdDomain
+ eventually_apply_implicitFunction
+ eventually_apply_implicitFunctionOfProdDomain
+ hasStrictFDerivAt_implicitFunctionOfProdDomain
+ implicitFunctionDataOfProdDomain
+ implicitFunctionOfProdDomain
+ implicitFunctionOfProdDomain_def
+ implicitFunction_apply_self
+ leftFun_eq_iff_implicitFunction
+ leftFun_implicitFunction
+ leftFun_implicitFunctionDataOfProdDomain
+ leftFun_implicitFunction_eq_leftFun
+ prodFun_implicitFunction
+ pt_implicitFunctionDataOfProdDomain
+ rightFun_implicitFunction
+ rightFun_implicitFunctionDataOfProdDomain
+ rightFun_implicitFunction_eq_rightFun
+ tendsto_implicitFunctionOfProdDomain
++ hasStrictFDerivAt_implicitFunction
+-+ implicitFunction
+-++ contDiffAt_implicitFunction
+-++ implicitFunction_def
- comp_implicitFunctionAux_eq_snd
- contDiff_implicitFunction
- implicitFunctionAux
- implicitFunctionAux_fst
- implicitFunctionData
- implicitFunctionData_leftFun_apply
- implicitFunctionData_leftFun_pt
- implicitFunctionData_pt
- implicitFunctionData_rightFun_apply
- implicitFunctionData_rightFun_pt
- implicitFunction_apply
- one_le

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 scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@agjftucker agjftucker added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 11, 2025
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Aug 1, 2025
@grunweg grunweg added the t-analysis Analysis (normed *, calculus) label Aug 4, 2025
@agjftucker agjftucker changed the title feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate feat(Analysis/Calculus/Implicit): define implicitFunOfBivariate Aug 5, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 12, 2025
@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 12, 2025
agjftucker
agjftucker commented Jan 27, 2026
View reviewed changes
winstonyin
winstonyin reviewed Jan 30, 2026
View reviewed changes
winstonyin
winstonyin reviewed Jan 30, 2026
View reviewed changes
winstonyin
winstonyin reviewed Jan 30, 2026
View reviewed changes
@winstonyin winstonyin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2026
winstonyin
winstonyin reviewed Jan 30, 2026
View reviewed changes
winstonyin
winstonyin reviewed Jan 31, 2026
View reviewed changes
@agjftucker agjftucker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 10, 2026
j-loreaux
j-loreaux reviewed Mar 17, 2026
View reviewed changes
Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean
filter_upwards [φ.leftFun_eq_iff_implicitFunction, φ.rightFun_implicitFunction_eq_rightFun]
exact fun v h _ => Iff.trans h ⟨congrArg _, by aesop⟩

theorem hasStrictFDerivAt_implicitFunctionOfProdDomain
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux Mar 17, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a bit weird that this is itself in the HasStrictFDerivAt namespace, but I don't currently have a better suggestion.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Mar 17, 2026

@agjftucker these last naming issues are the only remaining things in my mind. This looks quite good now.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 17, 2026
@agjftucker
Copy link
Copy Markdown
Collaborator Author

agjftucker commented Mar 18, 2026

@agjftucker these last naming issues are the only remaining things in my mind. This looks quite good now.

OK thanks. I would certainly like to see this process as one of slow improvement, though it more often feels like chasing my own tail! Anyway these points about naming are new and I will act on them.

During the inconclusive discussion about "Transparency and API design" I took the @[expose] tag off each of these files, even, most boldly, Implicit.lean. Should I leave it like that? I guess it is supposed to be the future style of Mathlb.

@agjftucker agjftucker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Mar 20, 2026

Yes, I think that removing @[expose] is in general a good thing. There's not a huge rush to do it, but it's nice to do when we can. Thanks!

bors merge

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Mar 20, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 20, 2026
@agjftucker
feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfPr…
ef7aa4b 
…odDomain (#26985)

This PR continues the work from #16743.

Original PR: #16743
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 20, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain [Merged by Bors] - feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain Mar 20, 2026
@mathlib-bors mathlib-bors bot closed this Mar 20, 2026
justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Mar 28, 2026
@agjftucker @justus-springer
feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfPr…
f4d111b 
…odDomain (leanprover-community#26985)

This PR continues the work from leanprover-community#16743.

Original PR: leanprover-community#16743
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux approved these changes

@sgouezel sgouezel Awaiting requested review from sgouezel

+1 more reviewer

@winstonyin winstonyin winstonyin left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@j-loreaux j-loreaux

@hrmacbeth hrmacbeth

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@agjftucker @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot @j-loreaux @winstonyin @grunweg @hrmacbeth