theorem scaled_primal_counterpart_pairing {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E →L[ℝ] ℝ} {xDagger : E} (hDagger : xDagger ∈ primalCounterparts a) (L : ↑PosReal) : a (-(‖a‖ / ↑L) • xDagger) = -(‖a‖ / ↑L * ‖a‖)

Helper for Lemma 10.65: the primal-counterpart equality rewrites the linear term in the non-Euclidean step.

theorem scaled_primal_counterpart_norm_sq_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E →L[ℝ] ℝ} {xDagger : E} (hDagger : xDagger ∈ primalCounterparts a) (L : ↑PosReal) : ‖-(‖a‖ / ↑L) • xDagger‖ ^ 2 ≤ (‖a‖ / ↑L) ^ 2

Helper for Lemma 10.65: the step direction has squared norm at most the square of its scalar coefficient because primal counterparts lie in the unit ball.

theorem non_euclidean_gradient_method_sufficient_decrease {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {Lf : NNReal} (hf : is_l_smooth_on f Set.univ Lf) (x : E) (L : ↑PosReal) (xDagger : E) (hDagger : xDagger ∈ primalCounterparts (fderiv ℝ f x)) : f (x - (‖fderiv ℝ f x‖ / ↑L) • xDagger) ≤ f x - (↑L - ↑Lf / 2) / ↑L ^ 2 * ‖fderiv ℝ f x‖ ^ 2

Lemma 10.65: if f is globally L_f-smooth and xDagger ∈ Λ_{f'(x)}, then the non-Euclidean trial point x - (‖f'(x)‖_* / L) • xDagger satisfies the sufficient-decrease inequality f(x - (‖f'(x)‖_* / L) • xDagger) ≤ f(x) - ((L - L_f / 2) / L^2) ‖f'(x)‖_*^2.