feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate by agjftucker · Pull Request #30077 · leanprover-community/mathlib4

agjftucker · 2025-09-29T19:08:03Z

Two specializations of the implicit function theorem, one applying to an uncurried bivariate function and one applying to a curried bivariate function.

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

This PR is a synthesis of material from others which failed to make progress. But there seems always to have been a different reason for it, so I'm afraid I keep trying where maybe I shouldn't.

#26985 reviewed by j-loreaux and later on by winstonyin.
#16743 and #26300 reviewed by sgouezel.
Zulip chat with Yury Kudryashov.

There are certain changes agreed upon in those PRs, e.g. to existing names, that are doubtless good but that I have excised from this PR to avoid distraction.

…OfBivariate

…_implicitFunOfBivariate

…o f₁, fy to f₂, p₀ to x, p to y, x to u etc.

…es to derivative in product space

…licitFunOfProdDomain`

…view suggestion 1

github-actions · 2025-09-29T19:09:05Z

PR summary d194281a48

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Calculus.FDeriv.Partial` (new file)	1856
`Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate` (new file)	2125

Declarations diff

+ eventually_apply_eq_iff_implicitFunctionOfBivariate
+ eventually_apply_implicitFunctionOfBivariate
+ hasStrictFDerivAt_implicitFunctionOfBivariate
+ hasStrictFDerivAt_uncurry_coprod
+ implicitFunctionOfBivariate
+ implicitFunctionOfBivariate_def
+ isLittleO_sub_sub_fderiv
+ tendsto_implicitFunctionOfBivariate

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).

j-loreaux · 2026-03-17T18:46:53Z

@agjftucker it's very confusing when you have several open PRs covering the overlapping material. Please try to refrain from that unless you are going to close one of the PRs.

I have just reviewed #26985 which I think is ready other than some minor naming issues. Let's get that across the line and then you can get the additional material in this PR merged. Therefore, I will make this PR depend on that one.

mathlib-dependent-issues · 2026-03-20T17:20:42Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain #26985~~
By Dependent Issues (🤖). Happy coding!

j-loreaux · 2026-03-20T18:45:31Z

please merge master to reduce the diff, and then we'll go from there.

mathlib-merge-conflicts · 2026-03-20T20:03:01Z

This pull request has conflicts, please merge master and resolve them.

agjftucker · 2026-03-21T20:51:00Z

please merge master to reduce the diff, and then we'll go from there.

Thanks for working with these PRs! I'm happy to get a little something into Mathlib before AGI makes my puny human contribution irrelevant :)

j-loreaux

Thanks! Maybe Yury will tell us if we can find this key result elsewhere in the library.

j-loreaux · 2026-03-24T19:47:49Z

Mathlib/Analysis/Calculus/FDeriv/Partial.lean

+/-- If bivariate `f : E₁ → E₂ → F` has partial derivatives `f₁` and `f₂` in a neighbourhood of
+`u : E₁ × E₂` and if they are continuous there then the uncurried function `↿f` is strictly
+differentiable at `u` with its derivative mapping `z` to `f₁ u.1 u.2 z.1 + f₂ u.1 u.2 z.2`. -/
+public theorem hasStrictFDerivAt_uncurry_coprod
+    [IsRCLikeNormedField 𝕜] {u : E₁ × E₂} {f : E₁ → E₂ → F} {f₁ : E₁ → E₂ → E₁ →L[𝕜] F}
+    {f₂ : E₁ → E₂ → E₂ →L[𝕜] F} (df₁ : ∀ᶠ v in 𝓝 u, HasFDerivAt (f · v.2) (↿f₁ v) v.1)
+    (df₂ : ∀ᶠ v in 𝓝 u, HasFDerivAt (f v.1 ·) (↿f₂ v) v.2) (cf₁ : ContinuousAt ↿f₁ u)
+    (cf₂ : ContinuousAt ↿f₂ u) : HasStrictFDerivAt ↿f ((↿f₁ u).coprod (↿f₂ u)) u := by


I seem to recall @urkud proving this (or something related) semi-recently, but I can't seem to find it. Am I wrong Yury?

j-loreaux · 2026-03-24T19:50:55Z

Mathlib/Analysis/Calculus/ImplicitFunction/ContDiff.lean

I would revert all the changes in this file. At best they are just noise.

Well winstonyin asked me to move ImplicitContDiff.lean to the new folder. Then I altered some comments to be more uniform across the folder (all on lines I already had to touch in #26985). But I’m happy to do just the first, or neither!

j-loreaux · 2026-03-24T19:52:50Z

Mathlib/Analysis/Calculus/FDeriv/Partial.lean

+theorem isLittleO_sub_sub_fderiv
+    {α 𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+    {u : E} {v w : α → E} {l : Filter α} (hv : Tendsto v l (𝓝 u)) (hw : Tendsto w l (𝓝 u))
+    (s : Set E := Set.univ) (seg : ∀ᶠ χ in l, [w χ -[ℝ] v χ] ⊆ s := by simp)
+    {f : α → E → F} {f' : α → E → E →L[𝕜] F}
+    (df' : ∀ᶠ p in l ×ˢ 𝓝[s] u, HasFDerivWithinAt (f p.1) (f' p.1 p.2) s p.2)
+    {φ : E →L[𝕜] F} (cf' : Tendsto ↿f' (l ×ˢ 𝓝[s] u) (𝓝 φ)) :
+    (fun χ => f χ (v χ) - f χ (w χ) - φ (v χ - w χ)) =o[l] (fun χ => v χ - w χ) := by


This lemma should have a docstring. I realize it's private, but that's no reason to make things obscure.

agjftucker · 2026-04-01T17:06:47Z

Thanks! Maybe Yury will tell us if we can find this key result elsewhere in the library.

Sorry for the delay and thanks. I looked through one or two of Yury's current PRs but I haven't found this

agjftucker added 26 commits September 12, 2024 21:13

feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFun…

f4dd7e3

…OfBivariate

Mess around with comments

9431aec

Rename nhds_prod_image and leftFun_eq_iff_implicitFun

e0b5166

More comment-fiddling

84acc73

codisjoint_iff_exists_add_eq better argument order (?)

390040b

rename nhds_pair_image

59374bd

generalise, move and rename Tendsto.eventually_image_of_prod

5800e66

done

1f8fb9f

introduce tendsto_implicitFunOfBivariate and rename hasStrictFDerivAt…

8dc672d

…_implicitFunOfBivariate

Merge branch 'master' into agjftucker/implicit

aaa12db

Merge branch 'master' into agjftucker/implicit

d543e9a

apply review suggestion 3, also rename X to E₁, Y to E₂, Z to F, fx t…

c98af70

…o f₁, fy to f₂, p₀ to x, p to y, x to u etc.

include hasStrictFDerivAt_uncurry_coprod relating partial derivativ…

bdcb088

…es to derivative in product space

introduce new implicitFunOfBivariate and rename the old one to `imp…

ecb262e

…licitFunOfProdDomain`

is it going to build finally?

1d9bcc5

rejig typeclasses and comments, addressing review suggestion 2

52c1686

Merge branch 'master' into agjftucker/implicit

e86ef09

remove unnecessary partials theorem and go back to ...ProdDomain

8353554

revert name change already in leanprover-community#27634 and apply re…

7fb32c1

…view suggestion 1

oops finish the job of name revert

e30f9bd

is CI working today?

63f534c

Merge branch 'master' into agjftucker/implicit

fe91c27

defer implicitFunOfBivariate and its dependencies to a later PR

ba3dc62

adjust comments to reflect loss of implicitFunOfBivariate from this file

6056937

remove probably misplaced heading

21b8a3a

reintroduce implicitFunOfBivariate in its own file

db662fa

github-actions bot added the t-analysis Analysis (normed *, calculus) label Sep 29, 2025

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 Sep 29, 2025

agjftucker requested a review from sgouezel September 29, 2025 19:27

CI broken again huh? anyway remove distracting naming fixes

1cf9af0

mathlib-triage bot assigned ADedecker Feb 21, 2026

mathlib-triage bot unassigned ADedecker Mar 11, 2026

agjftucker added 2 commits March 11, 2026 10:47

tinker with comments and labels

7f76378

done

85959d4

agjftucker requested a review from urkud March 11, 2026 11:10

mathlib-triage bot assigned j-loreaux Mar 15, 2026

j-loreaux added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 17, 2026

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 20, 2026

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026

mathlib-merge-conflicts 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 Mar 20, 2026

Merge branch 'master' into implicitFunOfBivariate

bc5f904

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 Mar 21, 2026

fix errors and move ImplicitContDiff.lean to folder ImplicitFunction

c15defa

github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Mar 21, 2026

agjftucker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026

j-loreaux reviewed Mar 24, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 24, 2026

apply review suggestions by j-loreaux

e73014a

github-actions bot removed the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Apr 1, 2026

revert filenames in Mathlib.lean

25563cc

agjftucker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026

agjftucker added 2 commits April 1, 2026 18:17

Merge branch 'master' into implicitFunOfBivariate

b73b84e

Refine description of isLittleO_sub_sub_fderiv

cd20f5a

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate#30077

feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate#30077
agjftucker wants to merge 55 commits intoleanprover-community:masterfrom
agjftucker:implicitFunOfBivariate

agjftucker commented Sep 29, 2025 •

edited by j-loreaux

Loading

Uh oh!

github-actions bot commented Sep 29, 2025 •

edited

Loading

Declarations diff

Uh oh!

j-loreaux commented Mar 17, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 20, 2026

Uh oh!

j-loreaux commented Mar 20, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 20, 2026

Uh oh!

agjftucker commented Mar 21, 2026

Uh oh!

j-loreaux left a comment

Uh oh!

j-loreaux Mar 24, 2026

Uh oh!

j-loreaux Mar 24, 2026

Uh oh!

agjftucker Apr 1, 2026

Uh oh!

j-loreaux Mar 24, 2026

Uh oh!

agjftucker commented Apr 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

agjftucker commented Sep 29, 2025 • edited by j-loreaux Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary d194281a48

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux commented Mar 17, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 20, 2026

Uh oh!

j-loreaux commented Mar 20, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 20, 2026

Uh oh!

agjftucker commented Mar 21, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

agjftucker Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Mar 24, 2026

Choose a reason for hiding this comment

Uh oh!

agjftucker commented Apr 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

agjftucker commented Sep 29, 2025 •

edited by j-loreaux

Loading

github-actions bot commented Sep 29, 2025 •

edited

Loading