theorem strongConvexOn_iff_quadratic_jensen_bound {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X] {μ : ℝ} {Q : Set X} {f : X → ℝ} (hQ : Convex ℝ Q) : StrongConvexOn Q μ f ↔ ∀ ⦃x y : X⦄, x ∈ Q → y ∈ Q → ∀ ⦃α : ℝ⦄, α ∈ Set.Icc 0 1 → f (α • x + (1 - α) • y) + α * (1 - α) * (μ / 2) * ‖x - y‖ ^ 2 ≤ α * f x + (1 - α) * f y

On a convex set Q in a real normed space, mathlib's owner predicate StrongConvexOn Q μ f is exactly the displayed quadratic Jensen inequality.

theorem strongConvexOn_iff_gradient_monotone {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {μ : ℝ} {Q : Set E} {f : E → ℝ} (hQ : Convex ℝ Q) (hf_diff : DifferentiableOn ℝ f Q) : StrongConvexOn Q μ f ↔ ∀ ⦃x y : E⦄, x ∈ Q → y ∈ Q → μ * ‖x - y‖ ^ 2 ≤ inner ℝ (gradientWithin f Q x - gradientWithin f Q y) (x - y)

On a convex set Q, a differentiable function is μ-strongly convex exactly when its within-set gradient is μ-strongly monotone in the ambient real inner product.

theorem strongConvexOn_tfae {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {μ : ℝ} {Q : Set E} {f : E → ℝ} (hQ : Convex ℝ Q) (hf_diff : DifferentiableOn ℝ f Q) : [StrongConvexOn Q μ f, ∀ ⦃x y : E⦄, x ∈ Q → y ∈ Q → μ * ‖x - y‖ ^ 2 ≤ inner ℝ (gradientWithin f Q x - gradientWithin f Q y) (x - y), ∀ ⦃x y : E⦄, x ∈ Q → y ∈ Q → ∀ ⦃α : ℝ⦄, α ∈ Set.Icc 0 1 → f (α • x + (1 - α) • y) + α * (1 - α) * (μ / 2) * ‖x - y‖ ^ 2 ≤ α * f x + (1 - α) * f y].TFAE

Theorem 2.10 on the canonical Hilbert-space owner layer: on a convex set Q, a differentiable function f is μ-strongly convex exactly when either of the two standard source-facing bridges holds, namely the strong gradient-monotonicity inequality or the quadratic Jensen inequality. The textbook Euclidean C¹ theorem is a direct specialization.