theorem line_deriv_within_nonneg_of_eventually_feasible {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {f : E → ℝ} {xStar d : E} (hmin : IsMinOn f Q xStar) (hd : ∀ᶠ (β : ℝ) in nhdsWithin 0 (Set.Ioi 0), xStar + β • d ∈ Q) (hline : LineDifferentiableWithinAt ℝ f Q xStar d) : 0 ≤ lineDerivWithin ℝ f Q xStar d

Helper for Lemma 3.19: any direction whose positive ray stays feasible near xStar has nonnegative intrinsic line derivative at a global minimizer.

theorem line_deriv_within_nonneg_on_feasible_displacements {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {f : E → ℝ} {xStar x : E} (hxStar : xStar ∈ Q) (hQ_convex : Convex ℝ Q) (hmin : IsMinOn f Q xStar) (hline : ∀ (d : E), (∀ᶠ (β : ℝ) in nhdsWithin 0 (Set.Ioi 0), xStar + β • d ∈ Q) → LineDifferentiableWithinAt ℝ f Q xStar d) (hx : x ∈ Q) : 0 ≤ lineDerivWithin ℝ f Q xStar (x - xStar)

Helper for Lemma 3.19: every feasible displacement from xStar has nonnegative intrinsic line derivative.

theorem line_deriv_within_nonneg_on_pointed_cone_hull_vsub_singleton {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {f : E → ℝ} {xStar p : E} (hxStar : xStar ∈ Q) (hQ_convex : Convex ℝ Q) (hmin : IsMinOn f Q xStar) (hline_hom : IsPositivelyHomogeneousOn 1 Set.univ (lineDerivWithin ℝ f Q xStar)) (hline : ∀ (d : E), (∀ᶠ (β : ℝ) in nhdsWithin 0 (Set.Ioi 0), xStar + β • d ∈ Q) → LineDifferentiableWithinAt ℝ f Q xStar d) (hp : p ∈ PointedCone.hull ℝ (Q -ᵥ {xStar})) : 0 ≤ lineDerivWithin ℝ f Q xStar p

Helper for Lemma 3.19: nonnegativity on feasible displacements extends to the pointed cone hull generated by Q - xStar.

theorem directionalDerivative_nonneg_on_posTangentCone_of_isMinOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {f : E → ℝ} {xStar : E} (hxStar : xStar ∈ Q) (hQ_convex : Convex ℝ Q) (hmin : IsMinOn f Q xStar) (hline_cont : Continuous (lineDerivWithin ℝ f Q xStar)) (hline_hom : IsPositivelyHomogeneousOn 1 Set.univ (lineDerivWithin ℝ f Q xStar)) (hline : ∀ (d : E), (∀ᶠ (β : ℝ) in nhdsWithin 0 (Set.Ioi 0), xStar + β • d ∈ Q) → LineDifferentiableWithinAt ℝ f Q xStar d) (p : E) (hp : p ∈ posTangentConeAt Q xStar) : 0 ≤ lineDerivWithin ℝ f Q xStar p

Lemma 3.19: if xStar minimizes f on the convex feasible set Q, then the intrinsic within-set directional-derivative map lineDerivWithin ℝ f Q xStar is nonnegative on the tangent cone 𝒯[Q] xStar.