The quartic example objective
f(x₁, x₂) = (1 / 2) x₁² + (1 / 4) x₂⁴ - (1 / 2) x₂².
Instances For
theorem
saddlePointConvergenceObjective_unitStepGradientMethod_tendsto_origin :
Filter.Tendsto (gradientMethod (fun (x : ℕ) => 1) saddlePointConvergenceObjective (EuclideanSpace.single 0 1))
Filter.atTop (nhds 0)
Example 1.6.11 (1): for
f(x₁, x₂) = (1 / 2) x₁² + (1 / 4) x₂⁴ - (1 / 2) x₂², the unit-step gradient method started at
(1, 0) converges to (0, 0).
theorem
saddlePointConvergenceObjective_origin_is_stationary :
HasGradientAt saddlePointConvergenceObjective 0 0
Example 1.6.11 (2): the limit point (0, 0) is a stationary point of
saddlePointConvergenceObjective.
theorem
saddlePointConvergenceObjective_origin_is_not_localMin :
¬IsLocalMin saddlePointConvergenceObjective 0
Example 1.6.11 (3): the stationary point (0, 0) is not a local minimum of
saddlePointConvergenceObjective.
theorem
unitStepGradientMethod_converges_to_nonminimizing_stationary_point :
Filter.Tendsto (gradientMethod (fun (x : ℕ) => 1) saddlePointConvergenceObjective (EuclideanSpace.single 0 1))
Filter.atTop (nhds 0) ∧ HasGradientAt saddlePointConvergenceObjective 0 0 ∧ ¬IsLocalMin saddlePointConvergenceObjective 0
The unit-step quartic-example trajectory converges to a stationary point that is not a local minimum.