Curvature of hypersurfaces

DefinitionLocal defining function#✓fully proved

Let \(E\) be a real inner product space, \(S \subseteq E\), \(\rho : E \to \mathbb{R}\) and \(p \in E\). Then \(\rho\) is a local defining function of \(S\) at \(p\) when \(\rho(p) = 0\), \(\rho\) is of class \(C^2\) at \(p\), its differential \(D\rho(p)\) is nonzero, and for all \(x\) in some neighborhood of \(p\), \(x \in S\) if and only if \(\rho(x) = 0\). In particular \(p \in S\).

Every point of a \(C^2\) hypersurface has local defining functions, and every point of a regular level set of a \(C^2\) function is of this form.

def IsLocalDefiningFunction (S : Set E) (ρ : E → ℝ) (p : E) : Prop :=
  ρ p = 0 ∧ ContDiffAt ℝ 2 ρ p ∧ fderiv ℝ ρ p ≠ 0 ∧ ∀ᶠ x in 𝓝 p, x ∈ S ↔ ρ x = 0

Used by 1

Used byA point with a local defining function lies in the set

TheoremA point with a local defining function lies in the set#✓fully proved

Let \(E\) be a real inner product space, \(S \subseteq E\), \(\rho : E \to \mathbb{R}\) and \(p \in E\). If \(\rho\) is a local defining function of \(S\) at \(p\), then \(p \in S\).

theorem IsLocalDefiningFunction.mem {S : Set E} {ρ : E → ℝ} {p : E}
    (h : IsLocalDefiningFunction S ρ p) : p ∈ S

Uses 1

Statement usesLocal defining function

DefinitionSecond fundamental form of a level set#✓fully proved

Let \(E\) be a finite-dimensional real inner product space, \(\rho : E \to \mathbb{R}\) and \(p \in E\). Write \(\nabla\rho(p)\) for the gradient of \(\rho\) at \(p\) and \(D^2\rho(p)\) for the second derivative of \(\rho\) at \(p\) (a bilinear form on \(E\)). The second fundamental form at \(p\) of the level set of \(\rho\) through \(p\), with respect to the unit normal \(\nabla\rho(p) / \|\nabla\rho(p)\|\), is defined for all \(u, v \in E\) by \(\mathrm{II}(u, v) = D^2\rho(p)(u, v) / \|\nabla\rho(p)\|\), and it is \(0\) when \(\nabla\rho(p) = 0\). When \(\rho\) is \(C^2\) near \(p\) and \(\nabla\rho(p) \neq 0\), for tangent vectors \(u\), \(v\) (orthogonal to \(\nabla\rho(p)\)) it equals \(\langle D_u \nu, v \rangle\) for the unit normal field \(\nu = \nabla\rho / \|\nabla\rho\|\).

The formula is the second fundamental form (independent of the defining function, up to the sign fixed by the normal) only for tangent \(u\) and \(v\): two defining functions of the same hyperplane can give different values on the normal vector.

def levelSetSecondFundamentalForm (ρ : E → ℝ) (p u v : E) : ℝ :=
  fderiv ℝ (fderiv ℝ ρ) p u v / ‖∇ ρ p‖

Used by 1

Used bySecond fundamental form under rescaling of the defining function

DefinitionMean curvature of a level set#✓fully proved

Let \(E\) be a finite-dimensional real inner product space, \(\rho : E \to \mathbb{R}\) and \(p \in E\). Write \(\nabla\rho(p)\) for the gradient of \(\rho\) at \(p\), \(D^2\rho(p)\) for the second derivative of \(\rho\) at \(p\) (a bilinear form on \(E\)), and \(\Delta\rho(p) = \sum_i D^2\rho(p)(e_i, e_i)\) for a fixed orthonormal basis \((e_i)\) of \(E\). The mean curvature at \(p\) of the level set of \(\rho\) through \(p\), with respect to the unit normal \(\nu = \nabla\rho(p) / \|\nabla\rho(p)\|\), is \(H = (\Delta\rho(p) - D^2\rho(p)(\nu, \nu)) / \|\nabla\rho(p)\|\), and \(H = 0\) when \(\nabla\rho(p) = 0\).

This is the trace of the second fundamental form on the tangent hyperplane \(\nabla\rho(p)^\perp\), the sum of the principal curvatures, and it equals \(\operatorname{div}(\nabla\rho / \|\nabla\rho\|)(p)\) when \(\rho\) is \(C^2\) near \(p\) and \(\nabla\rho(p) \neq 0\). Since \(D^2\rho(p)\) is bilinear, \(\Delta\rho(p)\) does not depend on the choice of orthonormal basis.

def levelSetMeanCurvature (ρ : E → ℝ) (p : E) : ℝ :=
  ((∑ i, fderiv ℝ (fderiv ℝ ρ) p (stdOrthonormalBasis ℝ E i) (stdOrthonormalBasis ℝ E i)) -
      fderiv ℝ (fderiv ℝ ρ) p (∇ ρ p) (∇ ρ p) / ‖∇ ρ p‖ ^ 2) / ‖∇ ρ p‖

Used by 5

Used byHyperplanes have zero mean curvature · Reversing the normal negates the mean curvature · Mean curvature under rescaling of the defining function · Positive rescaling preserves the mean curvature · Mean curvature of the unit sphere

TheoremSecond fundamental form under rescaling of the defining function#✓fully proved

Let \(E\) be a finite-dimensional real inner product space. For every \(\rho : E \to \mathbb{R}\), all \(p, u, v \in E\) and every real \(c \neq 0\), the second fundamental form at \(p\) of the level set of \(c\rho\) through \(p\), evaluated at \((u, v)\), equals \(c / |c|\) (the sign of \(c\)) times the second fundamental form at \(p\) of the level set of \(\rho\) through \(p\), evaluated at \((u, v)\).

theorem levelSetSecondFundamentalForm_smul (ρ : E → ℝ) (p u v : E) {c : ℝ} (hc : c ≠ 0) :
    levelSetSecondFundamentalForm (c • ρ) p u v =
      c / |c| * levelSetSecondFundamentalForm ρ p u v

Uses 1

Statement usesSecond fundamental form of a level set

TheoremMean curvature under rescaling of the defining function#✓fully proved

Let \(E\) be a finite-dimensional real inner product space. For every \(\rho : E \to \mathbb{R}\), every \(p \in E\) and every real \(c \neq 0\), the mean curvature at \(p\) of the level set of \(c\rho\) through \(p\) equals \(c / |c|\) (the sign of \(c\)) times the mean curvature at \(p\) of the level set of \(\rho\) through \(p\).

theorem levelSetMeanCurvature_smul (ρ : E → ℝ) (p : E) {c : ℝ} (hc : c ≠ 0) :
    levelSetMeanCurvature (c • ρ) p = c / |c| * levelSetMeanCurvature ρ p

Uses 1 · Used by 2

Statement usesMean curvature of a level set

Used byReversing the normal negates the mean curvature · Positive rescaling preserves the mean curvature

TheoremPositive rescaling preserves the mean curvature#✓fully proved

Let \(E\) be a finite-dimensional real inner product space. For every \(\rho : E \to \mathbb{R}\), every \(p \in E\) and every real \(c > 0\), the mean curvature at \(p\) of the level set of \(c\rho\) through \(p\) equals the mean curvature at \(p\) of the level set of \(\rho\) through \(p\).

theorem levelSetMeanCurvature_smul_of_pos (ρ : E → ℝ) (p : E) {c : ℝ} (hc : 0 < c) :
    levelSetMeanCurvature (c • ρ) p = levelSetMeanCurvature ρ p

Uses 2

Statement usesMean curvature of a level set

Proof usesMean curvature under rescaling of the defining function

TheoremReversing the normal negates the mean curvature#✓fully proved

Let \(E\) be a finite-dimensional real inner product space. For every \(\rho : E \to \mathbb{R}\) and every \(p \in E\), the mean curvature at \(p\) of the level set of \(-\rho\) through \(p\) is the negative of the mean curvature at \(p\) of the level set of \(\rho\) through \(p\): replacing \(\rho\) by \(-\rho\) reverses the unit normal and changes the sign of the mean curvature.

theorem levelSetMeanCurvature_neg (ρ : E → ℝ) (p : E) :
    levelSetMeanCurvature (-ρ) p = -levelSetMeanCurvature ρ p

Uses 2

Statement usesMean curvature of a level set

Proof usesMean curvature under rescaling of the defining function

TheoremMean curvature of the unit sphere#✓fully proved

Let \(E\) be a finite-dimensional real inner product space of dimension \(n\). For every \(p \in E\) with \(\|p\| = 1\), the mean curvature at \(p\) of the level set of \(\rho(x) = \|x\|^2 - 1\) through \(p\) is \(n - 1\). That is, the unit sphere of \(E\) has mean curvature \(n - 1\) with respect to the outward normal, the mean curvature being the sum (not the average) of the principal curvatures.

theorem levelSetMeanCurvature_sphere (p : E) (hp : ‖p‖ = 1) :
    levelSetMeanCurvature (fun x : E ↦ ‖x‖ ^ 2 - 1) p = finrank ℝ E - 1

Uses 2

Statement usesMean curvature of a level set

Proof usesSecond derivative of the squared norm

TheoremHyperplanes have zero mean curvature#✓fully proved

Let \(E\) be a finite-dimensional real inner product space. For all \(a \in E\), \(c \in \mathbb{R}\) and \(p \in E\), the mean curvature at \(p\) of the level set of \(\rho(x) = \langle a, x \rangle - c\) through \(p\) is \(0\). In particular, for \(a \neq 0\) the hyperplane \(\{x \mid \langle a, x \rangle = c\}\) has mean curvature \(0\) at each of its points.

theorem levelSetMeanCurvature_affine (a : E) (c : ℝ) (p : E) :
    levelSetMeanCurvature (fun x : E ↦ inner ℝ a x - c) p = 0

Uses 1

Statement usesMean curvature of a level set

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.