1. PhyslibAlpha
  2. Mathematics
  3. PartialDerivativeTest
Imports
/- Copyright (c) 2026 Bjørn Kjos-Hanssen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bjørn Kjos-Hanssen -/ module public import Mathlib.Analysis.Calculus.Gradient.Basic public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries public import Mathlib.LinearAlgebra.QuadraticForm.Basic public import Mathlib.Analysis.Calculus.FDeriv.Analytic public import Mathlib.Analysis.Analytic.IteratedFDeriv public import Mathlib.Analysis.Calculus.FDeriv.Symmetric public import Mathlib.Analysis.InnerProductSpace.PiL2

The Second Partial Derivatives Test

We prove a version of the second partial derivative test from calculus for analytic functions f : V → ℝ, where V is a finite-dimensional vector space.

Main results

    second_derivative_test: Suppose f is a real-valued function on a finite-dimensional inner product space that has vanishing gradient at x₀, and has a power series on a ball of positive radius around x₀. If the second Frechét derivative is positive definite at x₀ then f has local minimum at x₀.

Tags

partial derivative test, calculus

@[expose] public section

Update a vector of length 2 in coordinate 0.

@[simp] lemma Function.update₀ {α : Type*} {a b c : α} : Function.update ![a,b] 0 c = ![c,b] := α:Type u_1a:αb:αc:α⊢ update ![a, b] 0 c = ![c, b] α:Type u_1a:αb:αc:αi:Fin (Nat.succ 0).succ⊢ update ![a, b] 0 c i = ![c, b] i; α:Type u_1a:αb:αc:α⊢ update ![a, b] 0 c ((fun i => i) ⟨0, ⋯⟩) = ![c, b] ((fun i => i) ⟨0, ⋯⟩)α:Type u_1a:αb:αc:α⊢ update ![a, b] 0 c ((fun i => i) ⟨1, ⋯⟩) = ![c, b] ((fun i => i) ⟨1, ⋯⟩) α:Type u_1a:αb:αc:α⊢ update ![a, b] 0 c ((fun i => i) ⟨0, ⋯⟩) = ![c, b] ((fun i => i) ⟨0, ⋯⟩)α:Type u_1a:αb:αc:α⊢ update ![a, b] 0 c ((fun i => i) ⟨1, ⋯⟩) = ![c, b] ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙

Update a vector of length 2 in coordinate 1.

@[simp] lemma Function.update₁ {α : Type*} {a b c : α} : Function.update ![a,b] 1 c = ![a,c] := α:Type u_1a:αb:αc:α⊢ update ![a, b] 1 c = ![a, c] α:Type u_1a:αb:αc:αi:Fin (Nat.succ 0).succ⊢ update ![a, b] 1 c i = ![a, c] i; α:Type u_1a:αb:αc:α⊢ update ![a, b] 1 c ((fun i => i) ⟨0, ⋯⟩) = ![a, c] ((fun i => i) ⟨0, ⋯⟩)α:Type u_1a:αb:αc:α⊢ update ![a, b] 1 c ((fun i => i) ⟨1, ⋯⟩) = ![a, c] ((fun i => i) ⟨1, ⋯⟩) α:Type u_1a:αb:αc:α⊢ update ![a, b] 1 c ((fun i => i) ⟨0, ⋯⟩) = ![a, c] ((fun i => i) ⟨0, ⋯⟩)α:Type u_1a:αb:αc:α⊢ update ![a, b] 1 c ((fun i => i) ⟨1, ⋯⟩) = ![a, c] ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙

.

def QuadraticMap.toMultilinearMap {V : Type*} [AddCommGroup V] [Module ℝ V] (Q : QuadraticMap ℝ V ℝ) : MultilinearMap ℝ (fun _ : Fin 2 => V) ℝ := { toFun := fun v => Q.polarBilin (v 0) (v 1) map_update_add' := V:Type u_1inst✝¹:AddCommGroup Vinst✝:Module ℝ VQ:QuadraticMap ℝ V ℝ⊢ ∀ [inst : DecidableEq (Fin 2)] (m : Fin 2 → V) (i : Fin 2) (x y : V), (Q.polarBilin (update m i (x + y) 0)) (update m i (x + y) 1) = (Q.polarBilin (update m i x 0)) (update m i x 1) + (Q.polarBilin (update m i y 0)) (update m i y 1) All goals completed! 🐙 map_update_smul' := V:Type u_1inst✝¹:AddCommGroup Vinst✝:Module ℝ VQ:QuadraticMap ℝ V ℝ⊢ ∀ [inst : DecidableEq (Fin 2)] (m : Fin 2 → V) (i : Fin 2) (c : ℝ) (x : V), (Q.polarBilin (update m i (c • x) 0)) (update m i (c • x) 1) = c • (Q.polarBilin (update m i x 0)) (update m i x 1) All goals completed! 🐙}

The multilinear map associated to a quadratic map is continuous.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝB:V →ₗ[ℝ] V →L[ℝ] ℝhB:∀ (x y : V), (B x) y = Q.toMultilinearMap ![x, y]hB_cont:Continuous ⇑B⊢ Continuous ⇑Q.toMultilinearMap V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝB:V →ₗ[ℝ] V →L[ℝ] ℝhB:∀ (x y : V), (B x) y = Q.toMultilinearMap ![x, y]hB_cont:Continuous ⇑B⊢ ⇑Q.toMultilinearMap = fun x => ((⇑B ∘ fun v => v 0) x) (x 1); All goals completed! 🐙

.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝB:V →ₗ[ℝ] V →L[ℝ] ℝhB:∀ (x y : V), (B x) y = Q.toMultilinearMapHalfPolarBilin ![x, y]hB_cont:Continuous ⇑B⊢ Continuous ⇑Q.toMultilinearMapHalfPolarBilin V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝB:V →ₗ[ℝ] V →L[ℝ] ℝhB:∀ (x y : V), (B x) y = Q.toMultilinearMapHalfPolarBilin ![x, y]hB_cont:Continuous ⇑B⊢ ⇑Q.toMultilinearMapHalfPolarBilin = fun x => ((⇑B ∘ fun v => v 0) x) (x 1); All goals completed! 🐙

Construct a continuous multilinear map from a quadratic map on a finite dimensional space.

def QuadraticMap.toContinuousMultilinearMap {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticMap ℝ V ℝ) : ContinuousMultilinearMap ℝ (fun _ : Fin 2 ↦ V) ℝ := { Q.toMultilinearMap with cont := Q.toMultilinearMap_continuous }

The constructed continuous multilinear map agrees with the polar bilinear form.

theorem QuadraticMap.toContinuousMultilinearMap_apply {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticMap ℝ V ℝ) (x y : V) : Q.toContinuousMultilinearMap ![x, y] = Q.polarBilin x y := V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝx:Vy:V⊢ Q.toContinuousMultilinearMap ![x, y] = (Q.polarBilin x) y All goals completed! 🐙

.

theorem QuadraticMap.toContinuousMultilinearMap_applyHalf {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticMap ℝ V ℝ) (x y : V) : Q.toContinuousMultilinearMapHalfPolarBilin ![x, y] = (1/2) * Q.polarBilin x y := V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VQ:QuadraticMap ℝ V ℝx:Vy:V⊢ Q.toContinuousMultilinearMapHalfPolarBilin ![x, y] = 1 / 2 * (Q.polarBilin x) y All goals completed! 🐙

.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VF:QuadraticMap ℝ V ℝhf':F.PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → F.toContinuousMultilinearMapHalfPolarBilin ![m, m] ≤ F.toContinuousMultilinearMapHalfPolarBilin ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]this:F.toContinuousMultilinearMapHalfPolarBilin ![u, u] * ‖u‖⁻¹ = F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]⊢ ‖u‖ * ‖‖u‖⁻¹‖ = ‖u‖ * ‖u‖⁻¹ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VF:QuadraticMap ℝ V ℝhf':F.PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → F.toContinuousMultilinearMapHalfPolarBilin ![m, m] ≤ F.toContinuousMultilinearMapHalfPolarBilin ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]this:F.toContinuousMultilinearMapHalfPolarBilin ![u, u] * ‖u‖⁻¹ = F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]⊢ ‖‖u‖⁻¹‖ = ‖u‖⁻¹ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ VF:QuadraticMap ℝ V ℝhf':F.PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → F.toContinuousMultilinearMapHalfPolarBilin ![m, m] ≤ F.toContinuousMultilinearMapHalfPolarBilin ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]this:F.toContinuousMultilinearMapHalfPolarBilin ![u, u] * ‖u‖⁻¹ = F.toContinuousMultilinearMapHalfPolarBilin ![‖u‖⁻¹ • u, u]⊢ 0 ≤ ‖u‖⁻¹ All goals completed! 🐙)

The polar bilinear form of the second-derivative quadratic map is the symmetrized Hessian.

lemma polarBilin_iteratedFDerivQuadraticMap {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : V → ℝ) (x₀ : V) (x y : V) : (iteratedFDerivQuadraticMap f x₀).polarBilin x y = iteratedFDeriv ℝ 2 f x₀ ![x, y] + iteratedFDeriv ℝ 2 f x₀ ![y, x] := V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vx:Vy:V⊢ ((iteratedFDerivQuadraticMap f x₀).polarBilin x) y = (iteratedFDeriv ℝ 2 f x₀) ![x, y] + (iteratedFDeriv ℝ 2 f x₀) ![y, x] V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vx:Vy:V⊢ ({ toFun := fun y => (iteratedFDeriv ℝ 2 f x₀) ![y, y], toFun_smul := ⋯, exists_companion' := ⋯ }.polarBilin x) y = (iteratedFDeriv ℝ 2 f x₀) ![x, y] + (iteratedFDeriv ℝ 2 f x₀) ![y, x]; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vx:Vy:V⊢ (iteratedFDeriv ℝ 2 f x₀) ![x + y, x + y] - (iteratedFDeriv ℝ 2 f x₀) ![x, x] - (iteratedFDeriv ℝ 2 f x₀) ![y, y] = (iteratedFDeriv ℝ 2 f x₀) ![x, y] + (iteratedFDeriv ℝ 2 f x₀) ![y, x]; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vx:Vy:V⊢ ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![x + y, x + y] 0)) x + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![x + y, x + y] 0)) y = ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![x, y] 0)) y + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![y, x] 0)) x + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![y, y] 0)) y + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) (Fin.init ![x, x] 0)) x; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vx:Vy:V⊢ ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) x) x + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) y) x + (((fderiv ℝ (fun y => fderiv ℝ f y) x₀) x) y + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) y) y) = ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) x) y + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) y) x + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) y) y + ((fderiv ℝ (fun y => fderiv ℝ f y) x₀) x) x; All goals completed! 🐙

Symmetry of the second iterated Fréchet derivative (Schwarz's theorem).

All goals completed! 🐙; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ (iteratedFDeriv ℝ 2 f x₀) ![y, x] = (iteratedFDeriv ℝ 2 f x₀) ![x, y] V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ (iteratedFDeriv ℝ 2 f x₀) ![x, y] = (domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀)) ![y, x]; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ (iteratedFDeriv ℝ 2 f x₀) ![x, y] = (iteratedFDeriv ℝ 2 f x₀) fun i => ![y, x] i.rev exact congr_arg _ (V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ ![x, y] = fun i => ![y, x] i.rev V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀i:Fin (succ 1)⊢ ![x, y] i = ![y, x] i.rev; V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ ![x, y] ((fun i => i) ⟨0, ⋯⟩) = ![y, x] ((fun i => i) ⟨0, ⋯⟩).revV:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ ![x, y] ((fun i => i) ⟨1, ⋯⟩) = ![y, x] ((fun i => i) ⟨1, ⋯⟩).rev V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ ![x, y] ((fun i => i) ⟨0, ⋯⟩) = ![y, x] ((fun i => i) ⟨0, ⋯⟩).revV:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀x:Vy:Vh:domDomCongr Fin.revPerm (iteratedFDeriv ℝ 2 f x₀) = iteratedFDeriv ℝ 2 f x₀⊢ ![x, y] ((fun i => i) ⟨1, ⋯⟩) = ![y, x] ((fun i => i) ⟨1, ⋯⟩).rev All goals completed! 🐙)

Positive definiteness implies coercivity. The proof uses the general fact coercive_of_posdefHalf but requires a differentiability assumption on f.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vhf:ContDiffAt ℝ ⊤ f x₀hf':(iteratedFDerivQuadraticMap f x₀).PosDefkey:∀ (x y : V), (iteratedFDerivQuadraticMap f x₀).toContinuousMultilinearMapHalfPolarBilin ![x, y] = (iteratedFDeriv ℝ 2 f x₀) ![x, y]heq:continuousBilinearMapOfContinuousMultilinearMap (iteratedFDerivQuadraticMap f x₀).toContinuousMultilinearMapHalfPolarBilin = continuousBilinearMapOfContinuousMultilinearMap (iteratedFDeriv ℝ 2 f x₀)⊢ IsCoercive (continuousBilinearMapOfContinuousMultilinearMap (iteratedFDerivQuadraticMap f x₀).toContinuousMultilinearMapHalfPolarBilin) All goals completed! 🐙

Positive definiteness implies coercivity.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vhf':(iteratedFDerivQuadraticMap f x₀).PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → (iteratedFDeriv ℝ 2 f x₀) ![m, m] ≤ (iteratedFDeriv ℝ 2 f x₀) ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:(iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]this:(iteratedFDeriv ℝ 2 f x₀) ![u, u] * ‖u‖⁻¹ = (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]⊢ ‖u‖ * ‖‖u‖⁻¹‖ = ‖u‖ * ‖u‖⁻¹ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vhf':(iteratedFDerivQuadraticMap f x₀).PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → (iteratedFDeriv ℝ 2 f x₀) ![m, m] ≤ (iteratedFDeriv ℝ 2 f x₀) ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:(iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]this:(iteratedFDeriv ℝ 2 f x₀) ![u, u] * ‖u‖⁻¹ = (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]⊢ ‖‖u‖⁻¹‖ = ‖u‖⁻¹ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vhf':(iteratedFDerivQuadraticMap f x₀).PosDefhnt:Nontrivial Vthis✝:Nontrivial Vm:Vhm:‖m‖ = 1 ∧ ∀ (a : V), ‖a‖ = 1 → (iteratedFDeriv ℝ 2 f x₀) ![m, m] ≤ (iteratedFDeriv ℝ 2 f x₀) ![a, a]u:Vhu:¬u = 0h₁:‖u‖ * ‖u‖⁻¹ = 1h₂:(iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, ‖u‖⁻¹ • u] = ‖u‖⁻¹ * (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]this:(iteratedFDeriv ℝ 2 f x₀) ![u, u] * ‖u‖⁻¹ = (iteratedFDeriv ℝ 2 f x₀) ![‖u‖⁻¹ • u, u]⊢ 0 ≤ ‖u‖⁻¹ All goals completed! 🐙)

.

V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:InnerProductSpace ℝ Vf:V → ℝx₀:Vx:VC:ℝhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:(fderiv ℝ f x₀) x = (fderiv ℝ f x₀) x₀h₁:‖f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀‖ ≤ C / 2 * ‖x - x₀‖ ^ 2rev_ineq:∀ {a b c d : ℝ}, a + b ≤ c + d → d ≤ b → a ≤ c⊢ f x₀ ≤ f x refine rev_ineq ?_ <| mul_le_mul_of_nonneg_right (V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:InnerProductSpace ℝ Vf:V → ℝx₀:Vx:VC:ℝhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:(fderiv ℝ f x₀) x = (fderiv ℝ f x₀) x₀h₁:‖f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀‖ ≤ C / 2 * ‖x - x₀‖ ^ 2rev_ineq:∀ {a b c d : ℝ}, a + b ≤ c + d → d ≤ b → a ≤ c⊢ ?m.178 ≤ ?m.179 All goals completed! 🐙) (show 0 ≤ 1/2 V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:InnerProductSpace ℝ Vf:V → ℝx₀:Vx:VC:ℝhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:(fderiv ℝ f x₀) x = (fderiv ℝ f x₀) x₀h₁:‖f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀‖ ≤ C / 2 * ‖x - x₀‖ ^ 2⊢ f x₀ ≤ f x All goals completed! 🐙) V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:InnerProductSpace ℝ Vf:V → ℝx₀:Vx:VC:ℝhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:(fderiv ℝ f x₀) x = (fderiv ℝ f x₀) x₀rev_ineq:∀ {a b c d : ℝ}, a + b ≤ c + d → d ≤ b → a ≤ ch₁:|f x - ((2⁻¹ * (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀) + ((fderiv ℝ f x₀) x - (fderiv ℝ f x₀) x₀ + f x₀))| ≤ C / 2 * ‖x - x₀‖ ^ 2⊢ f x₀ + ((iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀) * (1 / 2) ≤ f x + C * ‖x - x₀‖ ^ 2 * (1 / 2) V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:InnerProductSpace ℝ Vf:V → ℝx₀:Vx:VC:ℝhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:(fderiv ℝ f x₀) x = (fderiv ℝ f x₀) x₀rev_ineq:∀ {a b c d : ℝ}, a + b ≤ c + d → d ≤ b → a ≤ ch₁:|f x - ((2⁻¹ * (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀) + ((fderiv ℝ f x₀) x - (fderiv ℝ f x₀) x₀ + f x₀))| ≤ C / 2 * ‖x - x₀‖ ^ 2this:-(f x - ((2⁻¹ * (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀) + ((fderiv ℝ f x₀) x₀ - (fderiv ℝ f x₀) x₀ + f x₀))) ≤ C / 2 * ‖x - x₀‖ ^ 2⊢ f x₀ + ((iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀) * (1 / 2) ≤ f x + C * ‖x - x₀‖ ^ 2 * (1 / 2) All goals completed! 🐙

Second partial derivative test, "little oh" form.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vh₀:gradient f x₀ = 0hcd:ContDiffAt ℝ ⊤ f x₀hf:(iteratedFDerivQuadraticMap f x₀).PosDefC✝:ℝhC✝:0 < C ∧ ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ((continuousBilinearMapOfContinuousMultilinearMap (iteratedFDeriv ℝ 2 f x₀)) u) uC:ℝhC:0 < C ∧ ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ ((continuousBilinearMapOfContinuousMultilinearMap (iteratedFDeriv ℝ 2 f x₀)) u) uh:∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : V) in nhds x₀, ‖f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀‖ ≤ c * ‖‖x - x₀‖ ^ 2‖x:Vhx:C * ‖x - x₀‖ ^ 2 ≤ (iteratedFDeriv ℝ 2 f x₀) fun x_1 => x - x₀hx₀:0 = (fderiv ℝ f x₀) x - (fderiv ℝ f x₀) x₀⊢ ‖f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀‖ ≤ C / 2 * ‖x - x₀‖ ^ 2 → f x₀ ≤ f x All goals completed! 🐙

Having a power series implies quadratic approximation.

V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝr:NNRealh✝:HasFPowerSeriesOnBall f p x₀ ↑rhbig:(fun y => f (x₀ + y) - p.partialSum 3 y) =O[nhds 0] fun y => ‖y‖ ^ 3h:((fun y => f (x₀ + y) - p.partialSum 3 y) ∘ fun x => x - x₀) =O[nhds x₀] ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀)⊢ Filter.Tendsto (fun x => ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀) x / ‖x - x₀‖ ^ 2) (nhds x₀) (nhds 0)V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝr:NNRealh✝:HasFPowerSeriesOnBall f p x₀ ↑rhbig:(fun y => f (x₀ + y) - p.partialSum 3 y) =O[nhds 0] fun y => ‖y‖ ^ 3h:((fun y => f (x₀ + y) - p.partialSum 3 y) ∘ fun x => x - x₀) =O[nhds x₀] ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀)⊢ ∀ᶠ (x : V) in nhds x₀, ‖x - x₀‖ ^ 2 = 0 → ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀) x = 0 V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝr:NNRealh✝:HasFPowerSeriesOnBall f p x₀ ↑rhbig:(fun y => f (x₀ + y) - p.partialSum 3 y) =O[nhds 0] fun y => ‖y‖ ^ 3h:((fun y => f (x₀ + y) - p.partialSum 3 y) ∘ fun x => x - x₀) =O[nhds x₀] ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀)⊢ Filter.Tendsto (fun x => ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀) x / ‖x - x₀‖ ^ 2) (nhds x₀) (nhds 0)V:Type u_1inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝr:NNRealh✝:HasFPowerSeriesOnBall f p x₀ ↑rhbig:(fun y => f (x₀ + y) - p.partialSum 3 y) =O[nhds 0] fun y => ‖y‖ ^ 3h:((fun y => f (x₀ + y) - p.partialSum 3 y) ∘ fun x => x - x₀) =O[nhds x₀] ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀)⊢ ∀ᶠ (x : V) in nhds x₀, ‖x - x₀‖ ^ 2 = 0 → ((fun y => ‖y‖ ^ 3) ∘ fun x => x - x₀) x = 0 All goals completed! 🐙 All goals completed! 🐙
@[nontriviality] lemma isLocalMin.of_subsingleton {V : Type*} [TopologicalSpace V] [Subsingleton V] {f : V → ℝ} {x₀ : V} : IsLocalMin f x₀ := V:Type u_1inst✝¹:TopologicalSpace Vinst✝:Subsingleton Vf:V → ℝx₀:V⊢ IsLocalMin f x₀ All goals completed! 🐙

The second partial derivative test.

V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝh₀:gradient f x₀ = 0r:NNRealh₁:HasFPowerSeriesOnBall f p x₀ ↑rhf:(iteratedFDerivQuadraticMap f x₀).PosDefa✝:Nontrivial Vh₂:∀ (x : V) (i : ℕ), ((p i) fun x_1 => x - x₀) = 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀h₃:∀ (x : V), (∑ i ∈ range 3, (p i) fun x_1 => x - x₀) = ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀⊢ IsLocalMin f x₀ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vp:FormalMultilinearSeries ℝ V ℝh₀:gradient f x₀ = 0r:NNRealh₁:HasFPowerSeriesOnBall f p x₀ ↑rhf:(iteratedFDerivQuadraticMap f x₀).PosDefa✝:Nontrivial Vh₂:∀ (x : V) (i : ℕ), ((p i) fun x_1 => x - x₀) = 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀h₃:∀ (x : V), (∑ i ∈ range 3, (p i) fun x_1 => x - x₀) = ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀h₄:∀ (x : V), (f x - ∑ i ∈ range 3, (p i) fun x_1 => x - x₀) = f x - ∑ i ∈ range 3, 1 / ↑i ! * (iteratedFDeriv ℝ i f x₀) fun x_1 => x - x₀⊢ IsLocalMin f x₀ All goals completed! 🐙

A more convenient form of the second partial derivative test: it suffices that f is analytic at x₀ (so that an explicit power series need not be produced by hand).

theorem second_derivative_test_analyticAt {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {f : V → ℝ} {x₀ : V} (h₀ : gradient f x₀ = 0) (han : AnalyticAt ℝ f x₀) (hf : (iteratedFDerivQuadraticMap f x₀).PosDef) : IsLocalMin f x₀ := V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vh₀:gradient f x₀ = 0han:AnalyticAt ℝ f x₀hf:(iteratedFDerivQuadraticMap f x₀).PosDef⊢ IsLocalMin f x₀ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vh₀:gradient f x₀ = 0hf:(iteratedFDerivQuadraticMap f x₀).PosDefp:FormalMultilinearSeries ℝ V ℝr:ENNRealhr:HasFPowerSeriesOnBall f p x₀ r⊢ IsLocalMin f x₀ V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vh₀:gradient f x₀ = 0hf:(iteratedFDerivQuadraticMap f x₀).PosDefp:FormalMultilinearSeries ℝ V ℝr:ENNRealhr:HasFPowerSeriesOnBall f p x₀ rr':NNRealhr'0:0 < ↑r'hr'lt:↑r' < r⊢ IsLocalMin f x₀ exact second_derivative_test h₀ (hr.mono (V:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:InnerProductSpace ℝ Vinst✝:FiniteDimensional ℝ Vf:V → ℝx₀:Vh₀:gradient f x₀ = 0hf:(iteratedFDerivQuadraticMap f x₀).PosDefp:FormalMultilinearSeries ℝ V ℝr:ENNRealhr:HasFPowerSeriesOnBall f p x₀ rr':NNRealhr'0:0 < ↑r'hr'lt:↑r' < r⊢ 0 < ↑r' All goals completed! 🐙) hr'lt.le) hf