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: