Tangent spaces of level sets

TheoremVelocities of curves in a level set lie in the kernel of the derivative#✓fully proved

Let \(E\) be a real normed space, \(c \in \mathbb{R}\), and \(f : E \to \mathbb{R}\) a function differentiable at \(x \in E\). If a curve \(\gamma : \mathbb{R} \to E\) satisfies \(\gamma(0) = x\), has derivative \(v\) at \(0\), and satisfies \(f(\gamma(t)) = c\) for all \(t \in \mathbb{R}\), then \(Df(x)v = 0\).

Proof: Apply the chain rule to f ∘ γ, then compare its derivative with that of the constant function determined by the level-set equation.

theorem levelSet_tangent_vel_of_curve
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : E → ℝ} {c : ℝ} {x v : E}
    (hf : DifferentiableAt ℝ f x)
    {γ : ℝ → E} (hγ0 : γ 0 = x) (hγ : HasDerivAt γ v 0)
    (hmem : ∀ t, f (γ t) = c) :
    fderiv ℝ f x v = 0

Sources

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 5.12; https://en.wikipedia.org/wiki/Tangent_space.

TheoremKernel vectors are velocities of local curves in a level set#✓fully proved

Let \(E\) be a real Banach space and let \(f : E \to \mathbb{R}\) have a strict derivative \(f'\) at \(x \in E\), a continuous linear map \(E \to \mathbb{R}\) that is surjective. Then for every \(v \in E\) with \(f'(v) = 0\) there is a curve \(\varphi : \mathbb{R} \to E\) with \(\varphi(0) = x\) and \(\varphi'(0) = v\) such that \(f(\varphi(t)) = f(x)\) for all \(t\) in some neighbourhood of \(0\).

theorem _root_.HasStrictFDerivAt.exists_levelSet_curve
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x v : E}
    (hf : HasStrictFDerivAt f f' x) (hsurj : Function.Surjective f')
    (hmem : f' v = 0) :
    ∃ φ : ℝ → E, φ 0 = x ∧ HasDerivAt φ v 0 ∧ ∀ᶠ t in 𝓝 0, f (φ t) = f x

Used by 1

Used byKernel vectors are velocities of curves in a regular level set

TheoremKernel vectors are velocities of curves in a regular level set#✓fully proved

Let \(E\) be a real Banach space, \(f : E \to \mathbb{R}\) a \(C^1\) function, \(c \in \mathbb{R}\), and \(x \in E\) a point with \(f(x) = c\) at which the derivative \(Df(x) : E \to \mathbb{R}\) is surjective. Then for every \(v \in E\) with \(Df(x)v = 0\) there is a curve \(\gamma : \mathbb{R} \to E\) with \(\gamma(0) = x\), \(\gamma'(0) = v\) and \(f(\gamma(t)) = c\) for all \(t \in \mathbb{R}\).

Proof: Use the implicit function theorem to construct a local curve tangent to the kernel vector, then compose it with a bounded arctangent reparametrization to obtain a curve on all of ℝ (implicit function theorem, Banach space version: https://en.wikipedia.org/wiki/Implicit_function_theorem).

theorem levelSet_curve_of_tangent_vel
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {f : E → ℝ} {c : ℝ} {x v : E}
    (hf : ContDiff ℝ 1 f) (hx : f x = c)
    (hsurj : Function.Surjective (fderiv ℝ f x))
    (hmem : fderiv ℝ f x v = 0) :
    ∃ γ : ℝ → E, γ 0 = x ∧ HasDerivAt γ v 0 ∧ ∀ t, f (γ t) = c

Sources

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 5.12.

Uses 1

Proof usesKernel vectors are velocities of local curves in a level set

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.