theorem inner_gradient_eq_zero_of_mem_direction_of_isMinOn_affineSubspace {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {s : AffineSubspace ℝ E} (hf : DifferentiableAt ℝ f x) (hx : x ∈ s) (hmin : IsMinOn f (↑s) x) {v : E} (hv : v ∈ s.direction) : inner ℝ (gradient f x) v = 0

If x minimizes f on an affine subspace s, then the gradient at x is orthogonal to every vector in the direction of s.

theorem gradients_pairwise_orthogonal_of_isMinOn_affineSearchSpaces {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x : ℕ → E) (searchSpace : ℕ → AffineSubspace ℝ E) (hdiff : ∀ (k : ℕ), DifferentiableAt ℝ f (x k)) (hdir : ∀ {a b : ℕ}, a < b → gradient f (x a) ∈ (searchSpace b).direction) (hmin : ∀ (k : ℕ), 0 < k → x k ∈ searchSpace k ∧ IsMinOn f (↑(searchSpace k)) (x k)) {k i : ℕ} (hki : k ≠ i) : inner ℝ (gradient f (x k)) (gradient f (x i)) = 0

If each positive stage x k minimizes f on an affine search space searchSpace k, and every earlier gradient lies in the direction of every later search space, then gradients at distinct stages are orthogonal.

theorem gradients_pairwise_orthogonal_of_isMinOn_affineSpan_gradients {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x : ℕ → E) (hdiff : ∀ (k : ℕ), DifferentiableAt ℝ f (x k)) (hmin : ∀ (k : ℕ), 0 < k → have searchSpace := AffineSubspace.mk' (x 0) (Submodule.span ℝ (Set.range fun (j : Fin k) => gradient f (x ↑j))); x k ∈ searchSpace ∧ IsMinOn f (↑searchSpace) (x k)) {k i : ℕ} (hki : k ≠ i) : inner ℝ (gradient f (x k)) (gradient f (x i)) = 0

Lemma 1.9.5: if each iterate xₖ with k > 0 lies in and minimizes f on the affine subspace x₀ + span {∇ f(x₀), …, ∇ f(xₖ₋₁)}, then the gradients at distinct iterates are orthogonal.