noncomputable def symmetric_matrix_min_eigenvalue {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) (hn : 0 < n) : ℝ

The smallest eigenvalue of a real symmetric n × n matrix, using the canonical descending Hermitian spectrum endpoint ⊤ when n > 0.

theorem Matrix.PosDef.isSymm {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.PosDef) : A.IsSymm

Companion bridge: a positive-definite real matrix is symmetric, so the source-facing symmetric_matrix_min_eigenvalue applies without an extra symmetry hypothesis.

theorem quadratic_affine_function_on_l2_strongConvexOn_iff_posSemidef_shift {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) (b : Fin n → ℝ) (c σ : ℝ) : StrongConvexOn Set.univ σ (quadratic_affine_function_on_lp 2 A b c) ↔ (A - σ • 1).PosSemidef

Proposition 5.11 (1): for the quadratic function x ↦ (1 / 2) xᵀ A x + bᵀ x + c on ℝ^n equipped with the ℓ₂ norm, strong convexity with parameter σ is equivalent to the shifted symmetric matrix A - σ I being positive semidefinite.

theorem quadratic_affine_function_on_l2_strongConvexOn_iff_le_min_eigenvalue {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) (hn : 0 < n) (b : Fin n → ℝ) (c σ : ℝ) : StrongConvexOn Set.univ σ (quadratic_affine_function_on_lp 2 A b c) ↔ σ ≤ symmetric_matrix_min_eigenvalue A hA hn

Proposition 5.11 (2): for a real symmetric quadratic form, the strong-convexity modulus σ is admissible exactly when it does not exceed the smallest eigenvalue of the Hessian matrix A.

theorem quadratic_affine_function_on_l2_exists_pos_strongConvexOn_iff_posDef {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsSymm) (b : Fin n → ℝ) (c : ℝ) : (∃ (σ : ℝ), 0 < σ ∧ StrongConvexOn Set.univ σ (quadratic_affine_function_on_lp 2 A b c)) ↔ A.PosDef

Proposition 5.11 (3): the quadratic function x ↦ (1 / 2) xᵀ A x + bᵀ x + c on ℝ^n is strongly convex for some positive modulus if and only if its symmetric Hessian matrix A is positive definite.

theorem symmetric_matrix_min_eigenvalue_isGreatest_strongConvexity_parameter {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hn : 0 < n) (hApos : A.PosDef) (b : Fin n → ℝ) (c : ℝ) : IsGreatest {σ : ℝ | 0 < σ ∧ StrongConvexOn Set.univ σ (quadratic_affine_function_on_lp 2 A b c)} (symmetric_matrix_min_eigenvalue A ⋯ hn)

Proposition 5.11 (4): if the quadratic Hessian matrix A is positive definite, then its smallest eigenvalue is the largest positive strong-convexity parameter of the associated quadratic function on ℝ^n with the ℓ₂ norm.