def chapter02Exercise26Objective (x : EuclideanSpace ℝ (Fin 2)) : ℝ

The objective f(x) = x₁^4 + x₁^2 + x₂^2 from Exercise 2.6, encoded on ℝ².

noncomputable def chapter02Exercise26CurrentPoint : EuclideanSpace ℝ (Fin 2)

The current point (1, 1) used in Exercise 2.6.

noncomputable def chapter02Exercise26SearchDirection : EuclideanSpace ℝ (Fin 2)

The search direction (-3, -1) used in Exercise 2.6.

noncomputable def chapter02Exercise26Phi : ℝ → ℝ

The one-dimensional line-search profile α ↦ f(xk + α • dk) for Exercise 2.6.

def chapter02Exercise26PhiDeriv : ℝ → ℝ

The explicit derivative φ'(α) = 324 α^3 - 324 α^2 + 128 α - 20 of the Exercise 2.6 line-search profile.

noncomputable def chapter02Exercise26NextPoint : EuclideanSpace ℝ (Fin 2)

The accepted Wolfe-rule update point (-1 / 2, 1 / 2) from Exercise 2.6.

theorem search_ray_eq (α : ℝ) : chapter02Exercise26CurrentPoint + α • chapter02Exercise26SearchDirection = (EuclideanSpace.equiv (Fin 2) ℝ).symm ![1 - 3 * α, 1 - α]

Helper for Chapter02 Exercise 2.6: the search ray from (1, 1) in direction (-3, -1) has the explicit coordinate form (1 - 3 α, 1 - α).

theorem phi_eq_profile (α : ℝ) : chapter02Exercise26Phi α = (1 - 3 * α) ^ 4 + (1 - 3 * α) ^ 2 + (1 - α) ^ 2

Helper for Chapter02 Exercise 2.6: the line-search profile is the scalar quartic obtained by substituting the explicit search ray into f(x₁, x₂) = x₁^4 + x₁^2 + x₂^2.

theorem half_step_update_eq : chapter02Exercise26CurrentPoint + (1 / 2) • chapter02Exercise26SearchDirection = chapter02Exercise26NextPoint

Helper for Chapter02 Exercise 2.6: the accepted half-step update lands at (-1 / 2, 1 / 2).

theorem chapter02Exercise26WolfeRuleProducesHalfStepUpdate : WolfePowellCondition chapter02Exercise26Phi chapter02Exercise26PhiDeriv (1 / 10) (1 / 2) (1 / 2) ∧ chapter02Exercise26CurrentPoint + (1 / 2) • chapter02Exercise26SearchDirection = chapter02Exercise26NextPoint

Chapter02 Exercise 2.6 (1): the half-step α = 1 / 2 satisfies the Wolfe rule with ρ = 1 / 10 and σ = 1 / 2, and the resulting update point is (-1 / 2, 1 / 2).

theorem chapter02Exercise26AlphaOneNotWolfe : ¬WolfePowellCondition chapter02Exercise26Phi chapter02Exercise26PhiDeriv (1 / 10) (1 / 2) 1

Chapter02 Exercise 2.6 (2): the trial steplength α = 1 does not satisfy the Wolfe rule for the Exercise 2.6 line-search profile with ρ = 1 / 10 and σ = 1 / 2.

theorem chapter02Exercise26AlphaHalfWolfe : WolfePowellCondition chapter02Exercise26Phi chapter02Exercise26PhiDeriv (1 / 10) (1 / 2) (1 / 2)

Chapter02 Exercise 2.6 (3): the trial steplength α = 1 / 2 satisfies the Wolfe rule for the Exercise 2.6 line-search profile with ρ = 1 / 10 and σ = 1 / 2.

theorem chapter02Exercise26AlphaTenthNotWolfe : ¬WolfePowellCondition chapter02Exercise26Phi chapter02Exercise26PhiDeriv (1 / 10) (1 / 2) (1 / 10)

Chapter02 Exercise 2.6 (4): the trial steplength α = 1 / 10 does not satisfy the Wolfe rule for the Exercise 2.6 line-search profile with ρ = 1 / 10 and σ = 1 / 2.