theorem prox_center_quadratic_lower_bound {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : Seminorm ℝ E} [p.IsNorm] {Q₂ : Set E} {d₂ : E → ℝ} {u₀ u : E} (hd₂ : NesterovIsProxFunction p Q₂ d₂) (hu₀ : NesterovIsProxCenter Q₂ d₂ u₀) (hu : u ∈ Q₂) : d₂ u ≥ 1 / 2 * p (u - u₀) ^ 2