Partial derivatives and symmetry of mixed partials

DefinitionPartial derivative along a coordinate axis#✓fully proved

For \(f : \mathbb{R}^n \to \mathbb{R}\) and a coordinate index \(i\), let \(e_i\) be the \(i\)-th standard basis vector. The partial derivative \(\partial_i f : \mathbb{R}^n \to \mathbb{R}\) sends \(x\) to the derivative at \(t = 0\) of \(t \mapsto f(x + t e_i)\), taken to be \(0\) when this function is not differentiable at \(0\).

noncomputable def partialDeriv {n : ℕ} (f : (Fin n → ℝ) → ℝ) (i : Fin n) :
    (Fin n → ℝ) → ℝ :=
  fun x => deriv (fun t : ℝ => f (x + t • Pi.single i (1 : ℝ))) 0

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9; stable ref https://en.wikipedia.org/wiki/Partial_derivative.

Used by 5

Used bySymmetry of mixed partial derivatives (Clairaut's theorem) · Partial derivative as a Fréchet derivative · Partial derivative function of a differentiable function · Mixed partial derivatives via the second Fréchet derivative · Partial derivative as the derivative of a coordinate slice

TheoremPartial derivative as the derivative of a coordinate slice#✓fully proved

For \(f : \mathbb{R}^n \to \mathbb{R}\), a coordinate index \(i\) and a point \(x \in \mathbb{R}^n\), let \(e_i\) be the \(i\)-th standard basis vector. The partial derivative of \(f\) along the \(i\)-th coordinate axis at \(x\) equals the derivative at \(t = 0\) of the one-variable function \(t \mapsto f(x + t e_i)\), taken to be \(0\) when that function is not differentiable at \(0\).

theorem partialDeriv_spec {n : ℕ} (f : (Fin n → ℝ) → ℝ) (i : Fin n)
    (x : Fin n → ℝ) :
    partialDeriv f i x =
      deriv (fun t : ℝ => f (x + t • Pi.single i (1 : ℝ))) 0

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9.

Uses 1

Statement usesPartial derivative along a coordinate axis

TheoremPartial derivative as a Fréchet derivative#✓fully proved

Let \(f : \mathbb{R}^n \to \mathbb{R}\) be differentiable at a point \(x\), and let \(e_i\) be the \(i\)-th standard basis vector of \(\mathbb{R}^n\). Then the partial derivative of \(f\) along the \(i\)-th coordinate axis at \(x\) equals \(Df(x)\,e_i\), the Fréchet derivative of \(f\) at \(x\) applied to \(e_i\).

The proof differentiates \(f\) along the line \(t \mapsto x + t e_i\) by the chain rule.

theorem partialDeriv_eq_fderiv_apply {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (i : Fin n) (x : Fin n → ℝ) (hf : DifferentiableAt ℝ f x) :
    partialDeriv f i x = fderiv ℝ f x (Pi.single i (1 : ℝ))

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9.

Uses 1 · Used by 2

Statement usesPartial derivative along a coordinate axis

Used byPartial derivative function of a differentiable function · Mixed partial derivatives via the second Fréchet derivative

TheoremPartial derivative function of a differentiable function#✓fully proved

Let \(f : \mathbb{R}^n \to \mathbb{R}\) be differentiable and let \(e_i\) be the \(i\)-th standard basis vector of \(\mathbb{R}^n\). Then the partial derivative \(\partial_i f\) of \(f\) along the \(i\)-th coordinate axis is the function \(x \mapsto Df(x)\,e_i\), where \(Df(x)\) is the Fréchet derivative of \(f\) at \(x\).

theorem partialDeriv_eq_fderiv_apply_of_differentiable {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (i : Fin n) (hf : Differentiable ℝ f) :
    partialDeriv f i = fun x => fderiv ℝ f x (Pi.single i (1 : ℝ))

Uses 2 · Used by 1

Statement usesPartial derivative along a coordinate axis

Proof usesPartial derivative as a Fréchet derivative

Used byMixed partial derivatives via the second Fréchet derivative

TheoremMixed partial derivatives via the second Fréchet derivative#✓fully proved

Let \(f : \mathbb{R}^n \to \mathbb{R}\) be twice continuously differentiable, write \(e_k\) for the \(k\)-th standard basis vector of \(\mathbb{R}^n\) and \(\partial_k g\) for the partial derivative of a function \(g\) along the \(k\)-th coordinate axis, and let \(Df\) be the Fréchet derivative of \(f\), a map from \(\mathbb{R}^n\) to the linear maps \(\mathbb{R}^n \to \mathbb{R}\). Then for all coordinate indices \(i, j\) and every \(x \in \mathbb{R}^n\), \(\partial_j (\partial_i f)(x) = \big(D(Df)(x)\,e_j\big)\,e_i\), where \(D(Df)(x)\) is the Fréchet derivative of \(Df\) at \(x\).

theorem partialDeriv_partialDeriv_eq_fderiv_fderiv {n : ℕ}
    (f : (Fin n → ℝ) → ℝ) (i j : Fin n) (x : Fin n → ℝ) (hf : ContDiff ℝ 2 f) :
    partialDeriv (partialDeriv f i) j x =
      fderiv ℝ (fderiv ℝ f) x (Pi.single j (1 : ℝ)) (Pi.single i (1 : ℝ))

Uses 3 · Used by 1

Statement usesPartial derivative along a coordinate axis

Proof usesPartial derivative as a Fréchet derivative · Partial derivative function of a differentiable function

Used bySymmetry of mixed partial derivatives (Clairaut's theorem)

TheoremSymmetry of mixed partial derivatives (Clairaut's theorem)#✓fully proved

For a function \(g : \mathbb{R}^n \to \mathbb{R}\), write \(\partial_i g\) for its partial derivative along the \(i\)-th coordinate axis. If \(f : \mathbb{R}^n \to \mathbb{R}\) is twice continuously differentiable, then for all coordinate indices \(i, j\) and every point \(x \in \mathbb{R}^n\), \(\partial_j (\partial_i f)(x) = \partial_i (\partial_j f)(x)\).

The proof writes both mixed partials as values of the second Fréchet derivative of \(f\) at \(x\) and applies Schwarz's theorem on the symmetry of second derivatives.

theorem iterated_partialDeriv_commute {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (i j : Fin n) (x : Fin n → ℝ) (hf : ContDiff ℝ 2 f) :
    partialDeriv (partialDeriv f i) j x =
      partialDeriv (partialDeriv f j) i x

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Theorem 9.41 (pp. 235–236).

Uses 2

Statement usesPartial derivative along a coordinate axis

Proof usesMixed partial derivatives via the second Fréchet derivative

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.