feat(LipschitzSmooth/Convex): convex iff equivalences for K-smoothness

[FordUniver]

Adds the four pairwise iff equivalences for a differentiable convex function on a Hilbert space, between LipschitzSmoothWith K f, LipschitzWith K (fderiv ℝ f), LipschitzWith K (∇ f), and CocoerciveWith K f. The substantive work lives in the prerequisite PRs; this PR is the synthesis step that composes them.

---

This is the synthesis cap of the LipschitzSmooth stack: each iff direction is a one-line composition of (i) the Baillon-Haddad hard direction LipschitzSmoothWith K f → CocoerciveWith K f under convexity, (ii) the non-convex Hilbert-form descent lemma LipschitzWith K (∇ f) → LipschitzSmoothWith K f, (iii) the elementary direction CocoerciveWith K f → LipschitzWith K (∇ f) (Cauchy-Schwarz), and (iv) the Riesz isomorphism LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f). Splitting these out of the Baillon-Haddad PR keeps that PR focused on the actual theorem and isolates the dependency on the descent lemma to this synthesis layer.

• depends on: feat(Analysis/Calculus/LipschitzSmooth): add descent lemma #28
• depends on: feat(Analysis/Calculus/LipschitzSmooth): Baillon-Haddad theorem and convex equivalences #29

Diff for the changes just in this PR over its predecessors: link

[FordUniver]

Folded back into #29 — the four iffs are 30 lines of pure compositions of (i) Baillon-Haddad and (ii) the descent lemma in Hilbert form, and conceptually inseparable from the BH theorem itself. Splitting them was over-application of 'minimize formal dependencies'.