Implicit function theorem in familiar form

Stream: maths

[Miyahara Kō]

Hi.
As we all know, Mathlib does not contain the implicit function theorem in the familiar form.
According to Wikipedia, the implicit function theorem is written in the following form:

Let $X$, $Y$, $Z$ be Banach spaces. Let the mapping $f : X \times Y \to Z$ be continuously Fréchet differentiable. If $(x_0,y_0)\in X\times Y$, $f(x_0,y_0)=0$, and $y\mapsto Df(x_0,y_0)(0,y)$ is a Banach space isomorphism from $Y$ onto $Z$, then there exist neighbourhoods $U$ of $x_0$ and $V$ of $y_0$ and a Fréchet differentiable function $g : U \to V$ such that $f(x, g(x)) = 0$ and $f(x, y) = 0$ if and only if $y = g(x)$, for all $(x,y)\in U\times V$.

So, in my spare time, I formalized it in the above form.
I do not intend to make this PR as it is tedious, but I hope it helps!

import Mathlib

open scoped Topology

variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
variable {Y : Type*} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
variable {Z : Type*} [NormedAddCommGroup Z] [NormedSpace ℝ Z] [CompleteSpace Z]

example
    {f : X × Y → Z} {x₀ : X} {y₀ : Y} {dfx : X →L[ℝ] Z} {dfy : Y ≃L[ℝ] Z}
    (hdf : HasStrictFDerivAt f (dfx.coprod ↑dfy) (x₀, y₀)) (hf : f (x₀, y₀) = 0) :
    ∃ g : X → Y, (∃ dg : X →L[ℝ] Y, HasStrictFDerivAt g dg x₀) ∧
      ∀ᶠ p in 𝓝 (x₀, y₀), f p = 0 ↔ p.2 = g p.1 := by
  let d : ImplicitFunctionData ℝ (X × Y) Z X :=
    { leftFun := f
      rightFun := Prod.fst
      pt := (x₀, y₀)
      leftDeriv := dfx.coprod ↑dfy
      left_has_deriv := hdf
      rightDeriv := ContinuousLinearMap.fst ℝ X Y
      right_has_deriv := hasStrictFDerivAt_fst
      left_range := by
        change LinearMap.range (↑(dfx.coprod ↑dfy : X × Y →L[ℝ] Z) : X × Y →ₗ[ℝ] Z) = ⊤
        rw [ContinuousLinearMap.coe_coprod, LinearMap.range_coprod]
        conv_lhs => arg 2; arg 1; change (↑(↑dfy : Y ≃ₗ[ℝ] Z) : Y →ₗ[ℝ] Z)
        simp
      right_range := Submodule.range_fst
      isCompl_ker := by
        change IsCompl
          (LinearMap.ker (↑(dfx.coprod ↑dfy : X × Y →L[ℝ] Z) : X × Y →ₗ[ℝ] Z))
          (LinearMap.ker (LinearMap.fst ℝ X Y))
        rw [ContinuousLinearMap.coe_coprod]
        conv => arg 1; arg 1; arg 2; change (↑(↑dfy : Y ≃ₗ[ℝ] Z) : Y →ₗ[ℝ] Z)
        constructor
        · rw [disjoint_iff]; ext ⟨x, y⟩
          simp only [Submodule.mem_inf, LinearMap.mem_ker, LinearMap.coprod_apply,
            ContinuousLinearMap.coe_coe, LinearEquiv.coe_coe, LinearMap.fst_apply,
            and_comm (b := x = 0), Submodule.mem_bot, Prod.mk_eq_zero, and_congr_right_iff]
          rintro rfl; simp
        · rw [codisjoint_iff]; ext ⟨x, y⟩
          simp only [Submodule.mem_sup, LinearMap.mem_ker, LinearMap.coprod_apply,
            ContinuousLinearMap.coe_coe, LinearEquiv.coe_coe, LinearMap.fst_apply, Prod.exists,
            exists_and_left, exists_eq_left, Prod.mk_add_mk, add_zero, Prod.mk.injEq,
            Submodule.mem_top, iff_true]
          use x, dfy.symm (dfx (-x))
          refine ⟨?_, rfl, ?_⟩
          · change dfx x + dfy (dfy.symm (dfx (-x))) = 0
            simp
          use dfy.symm (dfx x) + y
          simp }
  use fun x => (d.implicitFunction 0 x).2
  constructor
  · use -(↑dfy.symm ∘L dfx)
    have hd :=
      d.implicitFunction_hasStrictFDerivAt
        ((ContinuousLinearMap.id ℝ X).prod (-(↑dfy.symm ∘L dfx))) ?_ ?_
    · replace hd := hasStrictFDerivAt_snd.comp x₀ hd
      simp only [hf, ContinuousLinearMap.snd_comp_prod] at hd
      exact hd
    · simp
    · ext x; simp
  · have hd₁ := d.left_map_implicitFunction; simp only [ImplicitFunctionData.prodFun, hf] at hd₁
    replace hd₁ := hd₁.curry_nhds.self_of_nhds.prod_inl_nhds y₀
    have hd₂ := d.right_map_implicitFunction; simp only [ImplicitFunctionData.prodFun, hf] at hd₂
    replace hd₂ := hd₂.curry_nhds.self_of_nhds.prod_inl_nhds y₀
    filter_upwards [hd₁, hd₂, d.implicitFunction_apply_image] with ⟨x, y⟩ hxy₁ hxy₂ hxy₃
    simp only at hxy₁ hxy₂ hxy₃ ⊢
    constructor
    · intro hxy₄
      replace hxy₄ := congr_arg (fun z => (d.implicitFunction z x).2) hxy₄
      beta_reduce at hxy₄; rwa [hxy₃] at hxy₄
    · rintro rfl
      convert hxy₁
      exact hxy₂.symm

[Kim Morrison]

Why not PR it? Nothing wrong with tedious!

[Ruben Van de Velde]

Tedious proof or tedious PR process?

[Miyahara Kō]

PR process. I wrote a whack-a-mole proof so should be golfed, but I can't afford to do that because I am in the middle of the project.

[A.]

Would you like me to help out by putting a PR together?

[Miyahara Kō]

@A. Yes, thank you very much!

[Kim Morrison]

Just a general remark --- mathematically contentful proofs shouldn't be "golfed", they should be made more readable and more structured! Golfing is only for proofs that no one will ever want to read (including someone in the far future needing to do maintenance for a breakage).

[Richard Osborn]

It really surprises me that this community created a positive connotation with the word "golf" when basically every other programming community uses it as a negative term.

[Johan Commelin]

Aren't there entire subreddits and stackexchanges dedicated to this positive activity :rofl: ?

[Richard Osborn]

There's also the International Obfuscated C Code Contest, but I don't think we should use it for inspiration :laughing:

[Yury G. Kudryashov]

When I was formalizing the implicit function theorem, I decided to prove a very general version and leave formalizing specialized versions for future, because there are tons of special cases we may need, and it's hard to guess which ones will be useful in practice.

[Yury G. Kudryashov]

The only question I have about "golfing" or not this proof is "are there parts of the proof that can be moved to reusable lemmas?"

[A.]

Thanks Yury. I do have a specific use case in mind and something like the above should work for it. (I want to talk about the evolution of the fixed point of a function defined on $\mathbb{R}^{n}$.)

I was thinking of

noncomputable def prodImplicitFunction {f : X × Y → Z} {x₀ : X} {y₀ : Y}
    {dfx : X →L[𝕜] Z} {dfy : Y ≃L[𝕜] Z} (df₀ : HasStrictFDerivAt f (dfx.coprod dfy) (x₀, y₀)) :
    X → Y := …

or possibly

noncomputable def prodImplicitFunction {f : X → Y → Z} {x₀ : X} {y₀ : Y}
    {dfx : X →L[𝕜] Z} (dfx₀ : HasStrictFDerivAt (f · y₀) dfx x₀)
    {dfy : Y ≃L[𝕜] Z} (dfy₀ : HasStrictFDerivAt (f x₀) (dfy : Y →L[𝕜] Z) y₀) :
    X → Y := …

(or both) along with

example {f : X × Y → Z} {x₀ : X} {y₀ : Y}
    {dfx : X →L[𝕜] Z} {dfy : Y ≃L[𝕜] Z} (df₀ : HasStrictFDerivAt f (dfx.coprod dfy) (x₀, y₀)) :
    ∀ᶠ (x, y) in 𝓝 (x₀, y₀), f (x, y) = f (x₀, y₀) ↔ y = df₀.prodImplicitFunction x := ...

example {f : X × Y → Z} {x₀ : X} {y₀ : Y}
    {dfx : X →L[𝕜] Z} {dfy : Y ≃L[𝕜] Z} (df₀ : HasStrictFDerivAt f (dfx.coprod dfy) (x₀, y₀)) :
    HasStrictFDerivAt df₀.prodImplicitFunction (-dfy.symm ∘L dfx) x₀ := ...

etc.

[A.]

I also want something on the second derivative.

[A.]

#16743

[Violeta Hernández]

Kim Morrison said:

Just a general remark --- mathematically contentful proofs shouldn't be "golfed", they should be made more readable and more structured!

It really does say something about Mathlib (about all formal math in general?) that 99% of our theorems still classify as golf-worthy :stuck_out_tongue:

[A.]

@Winston Yin (尹維晨) I guess this stuff will be fresh in your mind since your PR #30595 merged yesterday was only written last month. Does it subsume mine?

[A.]

Oh mine has a different number since the migration-to-fork thing. It's now #26985. It finally got the thumbs-up literally hours before yours went through!

[A.]

There's also this dependent PR #30077 for the curried function.

[Winston Yin (尹維晨)]

Thanks for pinging me on this. I'm sorry that I was not aware of this thread before starting my work in July. Let me ping @Michael Rothgang and @Sébastien Gouëzel who reviewed my PR to see how we may proceed.

[Winston Yin (尹維晨)]

Having one's hard work subsumed by someone else's PR is a very disappointing experience, and I apologise for this. However, I believe there are parts that can be extracted from your PRs (e.g. curried version). My PR was meant to show C^n for the implicit function, so that's different from yours. I'll also mention my dependent PR #31988, which shows the local uniqueness of the implicit function. Does that overlap with anything in your PRs?

[A.]

Don't worry, of my many disappointments this is among the smallest! I've only brought it up here because I'm lazy. It's been such a long time since I wrote mine that it will be an effort for me to work out the relationships myself.

[A.]

No I didn't attempt anything on $C^n$. IIRC I had developed the idea that the best thing to do there would be to extend the Faa di Bruno stuff that exists elsewhere.

[Winston Yin (尹維晨)]

My C^n stuff is whatever works minimally, and some generalisation is likely possible. I'm also happy to schedule a video call where we disentangle all this. We may be able to use some of the type signature of your bivariate implicit function in the curried form, reducing them to the IsContDiffImplicitAt in my PR.

[Jireh Loreaux]

@Winston Yin (尹維晨) and @A., yes, I still think the curried version in #26985 is worthwhile, unless I'm missing somethinb obvious, but I'm sorry that also only saw this thread for the first time today.

[Jireh Loreaux]

@Winston Yin (尹維晨) would you mind reviewing #26895 ? I would like to see it merged, and I had already delegated before this came up. Since you are so familiar with the material and its current state in Mathlib, I think you would be ideal to review it.

[Winston Yin (尹維晨)]

Yes, I'm happy to. I like that #26985 (btw @Jireh Loreaux you mislabelled the PR in your second message) is more general than my mathlib#IsContDiffImplicitAt.implicitFunctionData in that it doesn't assume ContDiff, and I also like its hypotheses {f₁ : E₁ →L[𝕜] F} {f₂ : E₂ ≃L[𝕜] F}. I would like to state the latter in terms of the former. @A. : Feel free to do this yourself before I attempt it myself.

[A.]

Great :grinning: In a week or two I should have the time to look through it myself