noncomputable def
secondOrderTaylorModelAt
{E : Type u}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(f : E → ℝ)
(x : E)
:
E → ℝ
Definition 1.4.17: the second-order Taylor model of f at x.
Instances For
@[simp]
theorem
secondOrderTaylorModelAt_apply
{E : Type u}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(f : E → ℝ)
(x y : E)
:
secondOrderTaylorModelAt f x y = f x + inner ℝ (gradient f x) (y - x) + 1 / 2 * inner ℝ ((hessian f x) (y - x)) (y - x)
Evaluating secondOrderTaylorModelAt f x recovers the displayed quadratic formula.
theorem
secondOrderTaylorModelAt_apply_hessianMatrix
{n : ℕ}
(f : EuclideanSpace ℝ (Fin n) → ℝ)
(x y : EuclideanSpace ℝ (Fin n))
:
secondOrderTaylorModelAt f x y = f x + inner ℝ (gradient f x) (y - x) + 1 / 2 * inner ℝ ((Matrix.toEuclideanLin (hessianMatrix f x)) (y - x)) (y - x)
On ℝⁿ, the quadratic Taylor model can be rewritten using the Hessian matrix ∇² f x
acting on the displacement y - x.