noncomputable def normalizedGradientPairing {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x d : E) : ℝ

The normalized first-order objective pairing dᵀ ∇f(x) / ‖d‖ used in the source minimization problem.

theorem normalizedGradientPairing_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x d : E) : normalizedGradientPairing f x d = inner ℝ d (gradient f x) / ‖d‖

The defining formula for normalizedGradientPairing.

class IsFeasibleSteepestDescentDirection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x : E) (X : Set E) (d : E) : Prop

Chapter11 Definition 11.1.7: a vector d is a feasible steepest descent direction at x when f is differentiable at x, d ≠ 0, d belongs to the closure of the Chapter 8 feasible direction set FD(x, X), and its normalized gradient pairing is minimal among all feasible directions in FD(x, X).

• ne : d ≠ 0
• differentiableAt : DifferentiableAt ℝ f x
• mem_closure : d ∈ closure (feasibleDirections x X)
• minimal (d' : E) (hd' : d' ∈ feasibleDirections x X) : normalizedGradientPairing f x d ≤ normalizedGradientPairing f x d'

instance instSubsingletonIsFeasibleSteepestDescentDirection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x d : E) (X : Set E) : Subsingleton (IsFeasibleSteepestDescentDirection f x X d)

IsFeasibleSteepestDescentDirection f x X d is a proposition.

theorem isFeasibleSteepestDescentDirection_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x d : E) (X : Set E) : IsFeasibleSteepestDescentDirection f x X d ↔ d ≠ 0 ∧ DifferentiableAt ℝ f x ∧ d ∈ closure (feasibleDirections x X) ∧ ∀ d' ∈ feasibleDirections x X, normalizedGradientPairing f x d ≤ normalizedGradientPairing f x d'

Unfolding formula for IsFeasibleSteepestDescentDirection.

theorem IsFeasibleSteepestDescentDirection.ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x d : E} {X : Set E} (h : IsFeasibleSteepestDescentDirection f x X d) : d ≠ 0

A feasible steepest descent direction is nonzero.

theorem IsFeasibleSteepestDescentDirection.mem_base {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x d : E} {X : Set E} (h : IsFeasibleSteepestDescentDirection f x X d) : x ∈ X

A feasible steepest descent direction is based at a feasible point.

theorem IsFeasibleSteepestDescentDirection.le_normalizedGradientPairing {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x d d' : E} {X : Set E} (h : IsFeasibleSteepestDescentDirection f x X d) (hd' : d' ∈ feasibleDirections x X) : normalizedGradientPairing f x d ≤ normalizedGradientPairing f x d'

The defining minimization inequality for a feasible steepest descent direction.