theorem UniformConvexOn.tangent_gap_le_gradient_sub_rpow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {Q : Set E} {d : E → ℝ} {p σp : ℝ} (huc : UniformConvexOn Q (uniformConvexPowerModulus σp p) d) (hp : 1 < p) (hσp : 0 < σp) {x y : E} (hx : x ∈ Q) (hy : y ∈ Q) (hdx : DifferentiableWithinAt ℝ d Q x) (hdy : DifferentiableWithinAt ℝ d Q y) : d y - d x - inner ℝ (gradientWithin d Q x) (y - x) ≤ (p - 1) / p * (1 / σp).rpow (1 / (p - 1)) * ‖gradientWithin d Q y - gradientWithin d Q x‖.rpow (p / (p - 1))

Lemma 4.2.2 in source-facing form: for a degree-p uniformly convex function, the Bregman gap between two feasible points is controlled by the dual power of the difference of their canonical within-gradients.