def IsTwiceContinuouslyDifferentiableOn {n m : ℕ} (E : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → Fin m → ℝ) : Prop

Definition 6.12 (Twice continuous differentiability): let E ⊆ ℝⁿ be open and f : ℝⁿ → ℝᵐ. The map f is twice continuously differentiable (class C²) on E when it is continuously differentiable on E and each first-order partial derivative map is continuously differentiable on E. We encode this with the openness hypothesis together with ContDiffOn ℝ 2 f E.

Equations

• IsTwiceContinuouslyDifferentiableOn E f = (IsOpen E ∧ ContDiffOn ℝ 2 f E)

theorem clairaut_mixed_partials_within {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} (hE : IsOpen E) (hf : ContDiffOn ℝ 2 f E) ⦃x₀ : EuclideanSpace ℝ (Fin n)⦄ : x₀ ∈ E → ∀ (i j : Fin n), DifferentiableWithinAt ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single i 1)) E x₀ ∧ DifferentiableWithinAt ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single j 1)) E x₀ ∧ (∀ (ℓ : Fin m), ((fderivWithin ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single i 1)) E x₀) (EuclideanSpace.single j 1)).ofLp ℓ = ((fderivWithin ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single j 1)) E x₀) (EuclideanSpace.single i 1)).ofLp ℓ) ∧ (fderivWithin ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single i 1)) E x₀) (EuclideanSpace.single j 1) = (fderivWithin ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => (fderivWithin ℝ f E x) (EuclideanSpace.single j 1)) E x₀) (EuclideanSpace.single i 1)

Theorem 6.5: (Clairaut's theorem) let E ⊆ ℝⁿ be open and let f : ℝⁿ → ℝᵐ be of class C² on E. Then for every x₀ ∈ E and all indices i, j, the mixed second partial derivatives exist and commute. Componentwise, for each ℓ, ∂²f_ℓ/(∂xⱼ ∂xᵢ) (x₀) = ∂²f_ℓ/(∂xᵢ ∂xⱼ) (x₀); equivalently, the corresponding vector-valued mixed derivatives are equal.