feat(Analysis/Calculus/LipschitzSmooth): add descent lemma

[FordUniver]

Establishes the descent lemma for LipschitzSmoothWith: a differentiable function f : E → F between real normed spaces (F complete) whose Fréchet derivative is K-Lipschitz is K-smooth. The 1D deriv and Hilbert-space gradient forms follow as corollaries. The proof routes through a segment-pointwise predicate LipschitzSmoothOnSegmentWith and the fundamental theorem of calculus along a line segment. Also adds the identification of Lipschitz constants between the Fréchet derivative and the gradient (via Riesz representation), and its 1D deriv analogue.

---

This is the substantive descent-lemma layer on top of the foundational LipschitzSmoothWith predicate API (leanprover-community#39574), whose codomain-generality it inherits. The Baillon–Haddad equivalence between cocoercivity and Lipschitz-smoothness under convexity is the final layer, deferred to a follow-up that additionally depends on the Convex first-order package (leanprover-community#41494).

The Fréchet descent lemma proof uses segment-level curve integration (curveIntegral_fderiv_segment) from Mathlib.MeasureTheory.Integral.CurveIntegral. The gradient form uses toDual_comp_gradient to identify fderiv ℝ f and ∇ f as related by a LinearIsometryEquiv; the 1D analogue uses the isometry (ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm (evaluation at 1) in the same way.

• depends on: feat(Analysis/Calculus/LipschitzSmooth): add LipschitzSmoothWith and CocoerciveWith leanprover-community/mathlib4#39574
• depends on: feat(MeasureTheory/Integral/CurveIntegral): integrability and FTC along a line segment leanprover-community/mathlib4#39524
• depends on: [Merged by Bors] - feat(Analysis/Calculus/AddTorsor/AffineMap): smoothness of AffineMap.lineMap leanprover-community/mathlib4#39206
• depends on: [Merged by Bors] - refactor(Analysis/Calculus/Gradient): ungate inner_gradient lemmas leanprover-community/mathlib4#39203
• depends on: [Merged by Bors] - feat(Analysis/Calculus/Gradient): add toDual_gradient and companions leanprover-community/mathlib4#39202

Diff: link