theorem firstOrderNondegeneracyThreshold_eq_secant_constant {σ2 L : ℝ} (hσ2 : 0 ≤ σ2) (hL : 0 < L) : 2 * √(σ2 / L) / (1 + σ2 / L) = 2 * √(σ2 * L) / (σ2 + L)

Helper for Lemma 4.2.6: when σ₂ ≥ 0 and L > 0, the chapter threshold 2 * sqrt q[σ₂, L] / (1 + q[σ₂, L]) rewrites to the secant constant 2 * sqrt (σ₂ * L) / (σ₂ + L).

theorem firstOrderNondegeneracyThreshold_le_coefficient_of_mem_S11 {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {σ2 L : ℝ} {f : E → ℝ} {xStar : E} [Nontrivial E] (hf : f ∈ setOf (IsStrongConvexSmoothObjective σ2 L)) (hxStar : IsMinOn f Set.univ xStar) {x : E} (hx : x ≠ xStar) : 2 * √(σ2 / L) / (1 + σ2 / L) ≤ firstOrderNondegeneracyCoefficient f xStar x

Helper for Lemma 4.2.6: away from the minimizer, the strengthened secant inequality for a strongly convex smooth objective gives the desired lower bound on the first-order coefficient.

theorem exists_firstOrderNondegeneracyLowerBound_of_mem_S11 {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {σ2 L : ℝ} {f : E → ℝ} {xStar : E} (hf : f ∈ setOf (IsStrongConvexSmoothObjective σ2 L)) (hxStar : IsMinOn f Set.univ xStar) : ∃ (τ : ℝ), 2 * √(σ2 / L) / (1 + σ2 / L) ≤ τ ∧ IsFirstOrderNondegeneracyLowerBound f xStar τ

Lemma 4.2.6 (1): if f lies in the strong-convex smooth class 𝓢^{1,1}_{σ₂,L}, then relative to any chosen global minimizer xStar there exists a uniform first-order nondegeneracy lower bound τ whose size is at least the explicit threshold 2 * sqrt q[σ₂, L] / (1 + q[σ₂, L]).

theorem sqrt_q_lt_of_firstOrderNondegeneracyThreshold_le {σ2 L τ : ℝ} (hσ2 : 0 < σ2) (hσL : σ2 < L) (hτ : 2 * √(σ2 / L) / (1 + σ2 / L) ≤ τ) : √(σ2 / L) < τ

Lemma 4.2.6 (2): if 0 < σ₂ and σ₂ < L, then every lower bound τ dominating the explicit threshold 2 * sqrt q[σ₂, L] / (1 + q[σ₂, L]) automatically satisfies the strict improvement sqrt q[σ₂, L] < τ.

theorem isFirstOrderNondegenerate_of_mem_S11 {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {σ2 L : ℝ} {f : E → ℝ} {xStar : E} (hf : f ∈ setOf (IsStrongConvexSmoothObjective σ2 L)) (hxStar : IsMinOn f Set.univ xStar) : IsFirstOrderNondegenerate f xStar

A global minimizer of a strongly convex smooth objective is first-order nondegenerate as soon as Lemma 4.2.6 supplies the explicit positive lower bound on the coefficient.