feat(Analysis/Convex): first-order convexity inequalities

[FordUniver]

Adds first-order characterizations of convexity for differentiable functions in three forms — directional, Fréchet, and gradient — together with concave duals, strict variants, iff converses, and the first-order optimality corollaries ConvexOn.isMinOn_of_fderiv_eq_zero / ConvexOn.isMinOn_of_gradient_eq_zero. Analysis.Convex.Deriv picks up the 1D additive forms of the slope inequalities.

---

The motivation is the Baillon–Haddad theorem in the Lipschitz-smooth stack (#39574 and follow-ups), whose proof plays the gradient form of the first-order convexity inequality against the descent bound of a K-smooth function. LineDeriv carries the proof content via 1D line restriction (ConvexOn.lineRestriction); FDeriv and Gradient are restatements via lineDeriv_eq_fderiv and Riesz (inner_gradient_left) respectively. This inverts mathlib's usual FDeriv-as-foundation default because convex first-order inequalities are naturally 1D — they only need directional differentiability, and the FDeriv/gradient forms are strictly stronger restatements.

• depends on: [Merged by Bors] - refactor(Analysis/Calculus/Gradient): ungate inner_gradient lemmas #39203
• depends on: [Merged by Bors] - feat(Analysis/Convex/Segment): add lineMap_mem_segment #39198

[github-actions]

PR summary a9a383ff18

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.LineDeriv (new file)	1895
Mathlib.Analysis.Convex.FDeriv (new file)	1896
Mathlib.Analysis.Convex.Gradient (new file)	2269

---

Declarations diff (regex)

+ ConcaveOn.lineRestriction
+ ConvexOn.lineRestriction
+ StrictConcaveOn.lineRestriction
+ StrictConvexOn.lineRestriction
+ add_deriv_mul_le
+ add_deriv_mul_lt
+ add_fderiv_le
+ add_fderiv_lt
+ add_hasDerivAt_mul_le
+ add_hasDerivAt_mul_lt
+ add_hasFDerivAt_le
+ add_hasFDerivAt_lt
+ add_hasLineDerivAt_le
+ add_hasLineDerivAt_lt
+ add_inner_gradient_le
+ add_inner_gradient_lt
+ add_lineDeriv_le
+ add_lineDeriv_lt
+ convexOn_iff_add_fderiv_le
+ convexOn_iff_add_inner_gradient_le
+ fderiv_sub_nonneg
+ inner_gradient_sub_nonneg
+ isMinOn_of_fderiv_eq_zero
+ isMinOn_of_gradient_eq_zero
+ le_add_deriv_mul
+ le_add_fderiv
+ le_add_hasDerivAt_mul
+ le_add_hasFDerivAt
+ le_add_hasLineDerivAt
+ le_add_inner_gradient
+ le_add_lineDeriv
+ lineDeriv_sub_nonneg
+ lineMap_eq_add_smul_sub
+ lt_add_deriv_mul
+ lt_add_fderiv
+ lt_add_hasDerivAt_mul
+ lt_add_hasFDerivAt
+ lt_add_hasLineDerivAt
+ lt_add_inner_gradient
+ lt_add_lineDeriv

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a9a383f).

• +39 new declarations
• −0 removed declarations

+ConcaveOn.le_add_deriv_mul
+ConcaveOn.le_add_fderiv
+ConcaveOn.le_add_hasDerivAt_mul
+ConcaveOn.le_add_hasFDerivAt
+ConcaveOn.le_add_hasLineDerivAt
+ConcaveOn.le_add_inner_gradient
+ConcaveOn.le_add_lineDeriv
+ConcaveOn.lineRestriction
+ConvexOn.add_deriv_mul_le
+ConvexOn.add_fderiv_le
+ConvexOn.add_hasDerivAt_mul_le
+ConvexOn.add_hasFDerivAt_le
+ConvexOn.add_hasLineDerivAt_le
+ConvexOn.add_inner_gradient_le
+ConvexOn.add_lineDeriv_le
+ConvexOn.fderiv_sub_nonneg
+ConvexOn.inner_gradient_sub_nonneg
+ConvexOn.isMinOn_of_fderiv_eq_zero
+ConvexOn.isMinOn_of_gradient_eq_zero
+ConvexOn.lineDeriv_sub_nonneg
+ConvexOn.lineRestriction
+StrictConcaveOn.lineRestriction
+StrictConcaveOn.lt_add_deriv_mul
+StrictConcaveOn.lt_add_fderiv
+StrictConcaveOn.lt_add_hasDerivAt_mul
+StrictConcaveOn.lt_add_hasFDerivAt
+StrictConcaveOn.lt_add_hasLineDerivAt
+StrictConcaveOn.lt_add_inner_gradient
+StrictConcaveOn.lt_add_lineDeriv
+StrictConvexOn.add_deriv_mul_lt
+StrictConvexOn.add_fderiv_lt
+StrictConvexOn.add_hasDerivAt_mul_lt
+StrictConvexOn.add_hasFDerivAt_lt
+StrictConvexOn.add_hasLineDerivAt_lt
+StrictConvexOn.add_inner_gradient_lt
+StrictConvexOn.add_lineDeriv_lt
+StrictConvexOn.lineRestriction
+convexOn_iff_add_fderiv_le
+convexOn_iff_add_inner_gradient_le

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a9a383ff18
Reference commit 1c3e8f34a8

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - refactor(Analysis/Calculus/Gradient): ungate inner_gradient lemmas #39203
• [Merged by Bors] - feat(Analysis/Convex/Segment): add lineMap_mem_segment #39198
  By Dependent Issues (🤖). Happy coding!