theorem StrongConvexOn.lower_tangent_derivWithin_of_mem_interior {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : Set E} {μ : ℝ} {f : E → ℝ} (hf : StrongConvexOn Q μ f) {x y : E} (hx : x ∈ interior Q) (hy : y ∈ Q) : f y ≥ f x + derivWithin (fun (t : ℝ) => f (x + t • (y - x))) (Set.Ici 0) 0 + μ / 2 * ‖x - y‖ ^ 2

Lemma 3.2.3: if f is μ-strongly convex on Q, then every interior point x of Q supports the quadratic lower bound f y ≥ f x + f'(x; y - x) + (μ / 2) * ‖x - y‖^2 at every y ∈ Q, where f'(x; y - x) is the one-sided directional derivative of the line restriction t ↦ f (x + t • (y - x)) at t = 0.