[RemyDegenne]

This PR defines Legendre functions and proves the results of [LS, §26.4–26.6] about them that do not involve the Fenchel conjugate. It covers the Bandits roadmap's Layer 6.1, "Legendre functions" (the definition, [LS, Proposition 26.14], and [LS, Corollary 26.8] through [LS, Proposition 26.7]), and finishes Layer 6.2, "Bregman divergence and projections", with the Bregman projection theorem [LS, Theorem 26.15] and the generalized Pythagorean inequality [LS, Exercise 26.13]. The rest of Layer 6.2 was already on main: [LS, Theorem 26.3] is LML's HasFDerivWithinAt.hasSubgradientWithinAt (nonnegativity), bregDiv_self and ConvexOn.bregDiv, and the Hessian forms [LS, Theorems 26.12–26.13] are in Analysis/Convex/Bregman/Taylor.lean. These items are also the prerequisites that the OnlineLearning roadmap cites for its Layer 12.2 ("Constraints through Bregman projections [Ora, Theorem 12.11]: … the Bregman projection of Bandits 6.2"). Its Layer 6.1/6.2 relation lists "Legendre functions (6.1) and Bregman projections (6.2)" as provided here. The ReinforcementLearning roadmap's Bregman proximal steps also need them ("$F$ a Legendre mirror map (Bandits roadmap, Layer 6)").

Roadmap: Bandits

After this PR, Layer 6.1 still needs [LS, Theorem 26.6]: the gradient is a bijection between the interiors of the domains with inverse $\nabla F^$, $D_F(x,y)=D_{F^}(\nabla F(y),\nabla F(x))$, and $F^*$ is Legendre. It also needs the conversions of this representation to Tau Ceti's fenchelConjugate.

The representation follows the roadmap's first option: F : E → ℝ together with its convex domain D, on a real normed space E. IsLegendre F D asks for the following:

• F is convex on D;
• the interior of D is nonempty;
• F is differentiable and strictly convex on the interior;
• ‖fderiv ℝ F y‖ → ∞ along 𝓝[interior D] x for every x ∈ frontier (interior D). This is LS's sequence condition (c), stated with a filter.

The finite-dimensional hypothesis appears only where compactness is used. LS's Theorem 26.15 takes A ∩ dom f nonempty. Here A must meet the interior of D, because F is not assumed lower semicontinuous at the boundary, and on a boundary face of D the constrained minimum can then fail to exist.

LMLExplore/Analysis/Convex/Legendre.lean (new, 515 lines):

• IsLegendre, with convex, hasFDerivAt, hasSubgradientWithinAt, add_fderiv_apply_sub_le and mem_frontier_interior.
• IsLegendre.tendsto_fderiv_apply_sub [LS, Proposition 26.7]: ∇F(x + α (y - x)) (y - x) → ∞ as α → 1⁻, for x interior and y in the boundary of the interior. If the directional derivative stayed bounded, the tangent inequalities at x and along the segment would bound ‖∇F‖ there, contradicting steepness.
• IsLegendre.mem_interior_of_isMinOn_inter and mem_interior_of_isMinOn [LS, Corollary 26.8]: minimizers over A ∩ D are interior, for every convex A meeting the interior. fderiv_eq_zero_of_isMinOn follows.
• IsLegendre.isMinOn_inter_iff [LS, Proposition 26.14].
• IsLegendre.add_linear and add_const [LS, Exercise 26.10].
• IsLegendre.isBounded_sublevel, in finite dimension: a Legendre function with a minimizer has bounded sublevel sets. It grows linearly beyond a sphere around the minimizer.
• IsLegendre.existsUnique_isMinOn_inter [LS, Theorem 26.15 (a)]. Take a minimizing sequence and a subsequence that converges to some b. If b is interior, continuity makes it a minimizer. If b is on the boundary, Proposition 26.7 gives a point of A ∩ D with a smaller value.
• IsLegendre.isMinOn_bregDiv_iff [LS, Theorem 26.15 (b)].
• Bregman projections: isLegendre_bregDiv, existsUnique_isMinOn_bregDiv (projections of interior points onto A ∩ D exist and are unique), mem_interior_of_isMinOn_bregDiv, and the Legendre form of the Pythagorean inequality bregDiv_add_bregDiv_le.
• isLegendre_mul_log: x ↦ x log x on [0, ∞) is a non-degenerate witness with a nonempty boundary [LS, Example 26.11].

LMLExplore/Analysis/Convex/Bregman/Projection.lean (new, 93 lines):

• It now holds the two Bregman facts at constrained minimizers that were in OnlineLearning/FTRL/Basic.lean. Being general convex-analysis facts, they now sit before both FTRL and the Legendre file.
• bregDiv_add_bregDiv_le_of_isMinOn [LS, Exercise 26.13 (a)] derives the generalized Pythagorean inequality from them. F need not be convex, and J need not be a derivative at y.

LMLExplore/Analysis/Convex/Extrema.lean (new, 46 lines): ConvexOn.isMinOn_iff_forall_apply_sub_nonneg [LS, (26.2)], first-order optimality for convex functions with a derivative within the set. It is named after Mathlib's Mathlib/Analysis/Convex/Extrema.lean. No Mathlib, Tau Ceti or LML declaration states it; IsLocalMinOn.hasFDerivWithinAt_nonneg gives only one direction and does not use convexity.

Moved and renamed declarations (namespace change only, statements unchanged; every use now resolves through the parent namespace):

• LMLExplore.OnlineLearning.bregDiv_le_sub_of_isMinOn → LMLExplore.bregDiv_le_sub_of_isMinOn
• LMLExplore.OnlineLearning.bregDiv_le_sub_of_isMinOn_self → LMLExplore.bregDiv_le_sub_of_isMinOn_self

OnlineLearning/FTRL/Basic.lean now imports LMLExplore.Analysis.Convex.Bregman.Projection instead of Mathlib.Analysis.Calculus.LocalExtr.Basic.

Sources: [LS] T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Sections 26.4–26.6, and R. T. Rockafellar, Convex Analysis, Section 26. Both are cited in the files. No Mathlib infrastructure was vendored.

🤖 Prepared with Claude Code