noncomputable def quadraticHardInstanceFamily {n : ℕ} (L : ℝ) (k : Fin n) : EuclideanSpace ℝ (Fin n) → ℝ

Definition 2.10: for fixed L and k : Fin n, the textbook hard instance with one-based index k.1 + 1 ∈ {1, ..., n} is the quadratic objective on ℝⁿ obtained by applying smoothLowerBoundFunction L (Nat.succPNat k.1) to the first k.1 + 1 zero-based coordinates.