Prove2Me

Smooth local level parametrization with derivative the tangent inclusion

Proved
ImplicitCalculus.smooth_level_parametrization

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryimplicit-function-theorem

Let V be a real Banach space and W a finite-dimensional real normed space. Suppose F from V to W is smooth at y and DF at y is surjective. Write K for its kernel. There exists a map gamma from K into V, smooth at zero, such that

γ(0)=y,Dγ0:K↪V,F(γ(z))=F(y)for all z near zero.\gamma(0)=y,\qquad D\gamma_0:K\hookrightarrow V,\qquad F(\gamma(z))=F(y)\quad\text{for all z near zero}.

The derivative is the canonical kernel inclusion. This is a local level parametrization; compactness, global regularity, contact forms, and a finite-dimensional source are unnecessary.

Preamble
import Mathlib.Analysis.Calculus.ImplicitContDiff

set_option autoImplicit false
open Filter
open scoped ContDiff Topology
Formal statement
theorem ImplicitCalculus.smooth_level_parametrization
    {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (F : V → W) (y : V) (hF : ContDiffAt ℝ ∞ F y)
    (hD : Function.Surjective (fderiv ℝ F y)) :
    ∃ γ : (fderiv ℝ F y).ker → V,
      ContDiffAt ℝ ∞ γ 0 ∧ γ 0 = y ∧
      HasFDerivAt γ (fderiv ℝ F y).ker.subtypeL 0 ∧
      ∀ᶠ z in 𝓝 (0 : (fderiv ℝ F y).ker), F (γ z) = F y := by sorry
Source
Smooth implicit-function theorem. Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Analysis/Calculus/ImplicitContDiff.lean, ImplicitFunctionData.contDiffAt_implicitFunction; Implicit.lean, to_implicitFunctionOfComplemented and map_implicitFunctionOfComplemented_eq.

View graph