First-order optimality of an infimal-convolution minimizer gives a supporting inequality.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.minimizer_supporting_inequality {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hgradPhi : O3.IsCoordinateGradient kernel.phi kernel.gradPhi) {x v : Point d} (hv : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v) (z : Point d) : ell (x + v) + O3.pairing (-kernel.gradPhi ((1 / chi) • v)) (z - (x + v)) ≤ ell z

The first-order relation at an infimal minimizer, proved directly from minimality, convexity of the nonsmooth objective, and the genuine derivative of the kernel. No subgradient oracle for ell is assumed.