Regular level sets

TheoremLocal graph form of a level set near a regular point#✓fully proved

Let \(E\), \(G\) and \(F\) be finite-dimensional real normed spaces with \(\dim E = \dim G + \dim F\), let \(f \colon E \to F\) be a \(C^1\) map and let \(x_0 \in E\) be a point at which the derivative \(Df(x_0)\) is surjective. Then there exist a continuous linear isomorphism \(e \colon E \to G \times F\), a neighbourhood \(U\) in \(G\) of the first component of \(e(x_0)\), a map \(g \colon G \to F\) that is \(C^1\) on \(U\), and a neighbourhood \(V\) of \(x_0\) such that a point \(x \in V\) satisfies \(f(x) = f(x_0)\) if and only if \(e(x) = (u, g(u))\) for some \(u \in U\).

theorem _root_.ContDiff.exists_localGraph_of_surjective_fderiv
    {E G F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
    (hdim : Module.finrank ℝ E = Module.finrank ℝ G + Module.finrank ℝ F)
    (f : E → F) (hf : ContDiff ℝ 1 f) (x₀ : E)
    (hreg : Function.Surjective (fderiv ℝ f x₀)) :
    ∃ (e : E ≃L[ℝ] G × F)
      (U : Set G) (_ : U ∈ 𝓝 (e x₀).1) (g : G → F),
      ContDiffOn ℝ 1 g U ∧ ∃ V ∈ 𝓝 x₀, V ∩ f ⁻¹' {f x₀} =
        V ∩ e ⁻¹' {p : G × F | p.1 ∈ U ∧ p.2 = g p.1}

Used by 2

Used byRegular level sets are locally graphs · Regular level sets are locally parametrized by immersions

TheoremRegular level sets are locally graphs#✓fully proved

Let \(f \colon \mathbb{R}^{k+m} \to \mathbb{R}^m\) be a \(C^1\) map and let \(x_0 \in \mathbb{R}^{k+m}\) be a point at which the derivative \(Df(x_0)\) is surjective. Then there exist a linear isomorphism \(e \colon \mathbb{R}^{k+m} \to \mathbb{R}^k \times \mathbb{R}^m\), a neighbourhood \(U\) in \(\mathbb{R}^k\) of the first component of \(e(x_0)\), a map \(g \colon \mathbb{R}^k \to \mathbb{R}^m\) that is \(C^1\) on \(U\), and a neighbourhood \(V\) of \(x_0\) such that a point \(x \in V\) satisfies \(f(x) = f(x_0)\) if and only if \(e(x) = (u, g(u))\) for some \(u \in U\).

Proof: A projection onto the derivative kernel supplies adapted linear coordinates. The product-space implicit function theorem then identifies the level set with a local C¹ graph (https://en.wikipedia.org/wiki/Implicit_function_theorem).

theorem regularLevelSet_localGraph
    {k m : ℕ}
    (f : EuclideanSpace ℝ (Fin (k + m)) → EuclideanSpace ℝ (Fin m))
    (hf : ContDiff ℝ 1 f) (x₀ : EuclideanSpace ℝ (Fin (k + m)))
    (hreg : Function.Surjective (fderiv ℝ f x₀)) :
    ∃ (e : EuclideanSpace ℝ (Fin (k + m)) ≃L[ℝ]
          (EuclideanSpace ℝ (Fin k) × EuclideanSpace ℝ (Fin m)))
      (U : Set (EuclideanSpace ℝ (Fin k))) (_ : U ∈ 𝓝 ((e x₀).1))
      (g : EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin m)),
      ContDiffOn ℝ 1 g U ∧ ∃ V ∈ 𝓝 x₀, V ∩ f ⁻¹' {f x₀}
        = V ∩ e ⁻¹' {p : EuclideanSpace ℝ (Fin k) × EuclideanSpace ℝ (Fin m) |
          p.1 ∈ U ∧ p.2 = g p.1}

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4 (rank theorem).

Uses 1

Proof usesLocal graph form of a level set near a regular point

TheoremGraph maps are immersions#✓fully proved

Let \(E\) and \(F\) be real normed spaces, let \(n \in \mathbb{N} \cup \{\infty, \omega\}\) and let \(h \colon E \to F\) be a \(C^n\) map. Then the graph map \(x \mapsto (x, h(x))\) from \(E\) to \(E \times F\) is a \(C^n\) immersion, where \(E\) and \(E \times F\) are regarded as manifolds modelled on themselves.

theorem _root_.ContDiff.isImmersion_graph
    {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {n : ℕ∞ω} {h : E → F} (hh : ContDiff ℝ n h) :
    IsImmersion 𝓘(ℝ, E) 𝓘(ℝ, E × F) n (fun x => (x, h x))

TheoremRegular level sets are locally parametrized by immersions#✓fully proved

Let \(f \colon \mathbb{R}^{k+m} \to \mathbb{R}^m\) be a \(C^1\) map and let \(x_0 \in \mathbb{R}^{k+m}\) be a point at which the derivative \(Df(x_0)\) is surjective. Then there exist an open set \(U \subseteq \mathbb{R}^k\), a point \(u_0 \in U\), a map \(\varphi \colon \mathbb{R}^k \to \mathbb{R}^{k+m}\) that is \(C^1\) and a \(C^1\) immersion on all of \(\mathbb{R}^k\), and a neighbourhood \(V\) of \(x_0\) such that \(\varphi(u_0) = x_0\) and \(\varphi(U \cap \varphi^{-1}(V)) = V \cap f^{-1}(f(x_0))\).

Proof: Apply the implicit function theorem in adapted linear coordinates, then use a smooth bump to extend the local graphing function globally. A shear chart makes its graph map an immersion.

theorem regularLevelSet_localParametrization
    {k m : ℕ}
    (f : EuclideanSpace ℝ (Fin (k + m)) → EuclideanSpace ℝ (Fin m))
    (hf : ContDiff ℝ 1 f) (x₀ : EuclideanSpace ℝ (Fin (k + m)))
    (hreg : Function.Surjective (fderiv ℝ f x₀)) :
    ∃ (U : Set (EuclideanSpace ℝ (Fin k))) (_ : IsOpen U)
      (u₀ : EuclideanSpace ℝ (Fin k)) (_ : u₀ ∈ U)
      (φ : EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin (k + m))),
      ContMDiff 𝓘(ℝ, EuclideanSpace ℝ (Fin k)) 𝓘(ℝ, EuclideanSpace ℝ (Fin (k + m))) 1 φ ∧
      IsImmersion 𝓘(ℝ, EuclideanSpace ℝ (Fin k)) 𝓘(ℝ, EuclideanSpace ℝ (Fin (k + m))) 1 φ ∧
      ∃ V ∈ 𝓝 x₀, φ '' (U ∩ φ ⁻¹' V) = V ∩ f ⁻¹' {f x₀} ∧ φ u₀ = x₀

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed., Ch. 4 (rank theorem).

Uses 1

Proof usesLocal graph form of a level set near a regular point

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.