[prevostad]

This PR proves two general facts about the derivative of a convex function. Together they give two of the four properties in the last clause of [LS, Theorem 26.6], "$F^$ is Legendre". The target is the Bandits roadmap's Layer 6.1, "Legendre functions", which asks for [LS, Theorem 26.6] ("the gradient is a bijection between interiors with inverse $\nabla F^$, $D_F(x,y)=D_{F^}(\nabla F(y),\nabla F(x))$, and $F^$ is Legendre").

Roadmap: Bandits

How the conjugate's Legendre property will use them. Once surjectivity of ∇F onto the interior of the domain of F⋆ is proved, the derivative of F⋆ at u is evaluation at h u, where h is the inverse of ∇F (#319's hasFDerivAt_toReal_fenchelConjugateOn).

• Strict convexity of F⋆ on the interior of its domain. This is ConvexOn.strictConvexOn_of_injOn applied to F⋆, whose derivative u ↦ h u is injective.
• Steepness of F⋆. This is ConvexOn.tendsto_norm_comp_atTop_of_steep applied to F and h: ‖∇F⋆ u‖ = ‖h u‖ → ∞ at the frontier of the interior of the domain of F⋆. The steepness hypothesis is stated in the filter form of feat: Legendre functions, their constrained minimizers and Bregman projections [LS, §26.4–26.6] #289's IsLegendre (‖f' y‖ → ∞ along 𝓝[s] x for x ∈ frontier s).

Neither statement uses IsLegendre (#289), fenchelConjugateOn (#319) or the coercivity lemmas (#321), so this PR does not depend on any open PR. After this PR, Layer 6.1 still needs three things: the surjectivity of ∇F (from #321's bounded tilted sublevel sets and #289's Corollary 26.8), the assembly of IsLegendre for F⋆ from #319 and this PR, and the merge of #289 itself.

LMLExplore/Analysis/Convex/FDeriv.lean (new, 209 lines):

• Convex.strictConvexOn_of_hasSubgradientWithinAt: suppose a function has a subgradient (LML's HasSubgradientWithinAt) on a convex set s at every point of s, and no linear form is a subgradient at two distinct points. Then the function is strictly convex on s. The proof: if f were affine on a segment, the subgradient at an inner point of the segment would also be a subgradient at its ends.
• StrictConvexOn.eq_of_hasSubgradientWithinAt: the converse. This is Tau Ceti's StrictConvexOn.eq_of_mem_subdifferential, restated for LML's subgradients on a set; main has no bridge between the two predicates.
• StrictConvexOn.injOn_of_hasFDerivWithinAt, ConvexOn.strictConvexOn_of_injOn and ConvexOn.strictConvexOn_iff_injOn: a convex function with derivatives f' on an open set is strictly convex there if and only if f' is injective. The forward direction needs only derivatives within s, and s need not be open.
• ConvexOn.tendsto_norm_atTop_of_steep: let f be convex on an open set s of a proper space, with steep derivatives, and let b be a linear form that is not a derivative at a point of s. Then ‖x‖ → ∞ along comap f' (𝓝 b) ⊓ 𝓟 s. The proof takes a cluster point by compactness. In the interior, the subgradient inequalities pass to the limit and make b the derivative. At the frontier, steepness contradicts f' → b.
• ConvexOn.tendsto_norm_comp_atTop_of_steep: the same for a right inverse h of f' on a set t: ‖h u‖ → ∞ as u → b within t.

I searched for overlap. Mathlib proves strict convexity from a strictly monotone derivative only on ℝ (StrictMonoOn.strictConvexOn_of_deriv), and Mathlib, Tau Ceti and LML have no strict-convexity criterion through an injective Fréchet derivative or subgradient. Nothing in them concerns steepness. No Mathlib infrastructure was vendored.

Sources: R. T. Rockafellar, Convex Analysis, Theorems 26.3 and 26.5, and T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Section 26.4 and Theorem 26.6. Both are cited in the file.

🤖 Prepared with Claude Code

[prevostad]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	All six statements faithfully formalize subgradient separation, strict convexity iff the derivative is injective, and steepness passing to a right inverse of the derivative; the hypotheses (open s, ProperSpace, filter-form steepness, b ∉ f' '' s) match the intended use in LS Theorem 26.6 and are neither vacuous nor over-strong.
✅	reuse	approved	claude/claude-opus-5-5	Mathlib has no subgradient or steepness API, and its strict-convexity-from-derivative results are only for ℝ (StrictMonoOn.strictConvexOn_of_deriv); the new lemmas generalize this and reuse Mathlib's StrictConvexOn.eq_of_isMinOn. No duplicate was located in Mathlib or LMLExplore; the LML and TauCeti sources were not in the checkout, so the claimed missing bridge to TauCeti's eq_of_mem_subdifferential could not be checked.
✅	scope	approved	claude/claude-opus-5-5	The PR proves two of the Legendre properties of F* from [LS, Theorem 26.6], strict convexity and steepness, which Bandits roadmap Layer 6.1 asks for. It is one coherent topic with a direct path to that target.
✅	attribution	approved	claude/claude-opus-5-5	The file names its central informal sources (Rockafellar, Convex Analysis, Theorems 26.3 and 26.5; Lattimore–Szepesvári, Bandit Algorithms, Section 26.4 and Theorem 26.6), and no Mathlib material is vendored. The roadmap is credited only in the PR description, as required.
✅	api-design	approved	claude/claude-opus-5-5	The PR exposes six general, well-named public theorems (no definitions, no compatibility artifacts, nothing hidden as private) that Layer 6.1 needs to show the conjugate is Legendre. No characteristic API or automation annotations are required.
✅	generality	approved	claude/claude-opus-5-5	The general subgradient criterion is proved first and the derivative versions are derived from it, and the steepness lemma is the general form with the right-inverse corollary derived from it. Every hypothesis is used and matches the Legendre-conjugate target.
✅	placement	approved	claude/claude-opus-5-5	The new generic convex-analysis file LMLExplore/Analysis/Convex/FDeriv.lean sits in the right topic directory, mirroring Mathlib's Analysis/Convex/Deriv.lean, with no roadmap-specific declarations and no sibling files sharing its name prefix. Both imports are used: LML subgradient API and isBoundedBilinearMap_apply at line 184.
✅	naming	approved	claude/claude-opus-5-5	All declarations use dot notation on the matching Mathlib types and are named after their conclusions in standard terminology; the only _iff lemma is a genuine biconditional and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new file's module docstring covers the material and its purpose with references, and every public theorem has an accurate docstring that describes the result without overclaiming.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, commented where non-trivial (cluster-point/frontier case split, affine-segment argument), use well-hinted nlinarith/linarith instead of brittle rewrite chains, and rely on no undocumented definitional equality.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 4044022. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.93.}