[prevostad]

This PR completes [LS, Theorem 26.6] for Legendre functions. It proves that the derivative of a Legendre function F with domain D is a bijection from the interior of D onto the interior of the effective domain of the conjugate F⋆ = fenchelConjugateOn F D, and that the inverse of this bijection is ∇F⋆ (part (a)). It also proves Bregman duality in the form D_{F⋆}(∇F y, ∇F x) = D_F(x, y) (part (b)) and that the real representative of F⋆ is Legendre on {u | F⋆ u ≠ ⊤} (part (c)). No lower semicontinuity of F at the boundary is assumed.

Roadmap: Bandits

Milestone: Bandits Layer 6, item 1 ("Legendre functions"), which asks for [LS, Theorem 26.6] (the gradient is a bijection between interiors with inverse ∇F⋆, D_F(x,y) = D_{F⋆}(∇F(y), ∇F(x)), and F⋆ is Legendre), [LS, Corollary 26.8] and [LS, Proposition 26.14]. Corollary 26.8, Proposition 26.14, the definition and the conversion to Tau Ceti's fenchelConjugate are already on main (#289, #319). The pieces this PR builds on are on main too: #321 gives bounded tilted sublevel sets and #322 gives strict convexity and steepness through the derivative. After this PR, item 6.1 has nothing left.

Surjectivity of ∇F works by minimizing the tilted Legendre function F - u over D. Its sublevel sets are bounded by #321's isBounded_setOf_le_of_mem_interior_setOf_fenchelConjugate_ne_top, but F - u need not have a minimizer over its domain. So the private existence lemma behind IsLegendre.existsUnique_isMinOn_inter now takes a bounded sublevel set {x ∈ A ∩ D | F x ≤ F x₀} instead of a global minimizer, and is exposed as IsLegendre.existsUnique_isMinOn_inter_of_isBounded. existsUnique_isMinOn_inter keeps its statement and is now a corollary of it.

New declarations:

• LMLExplore/Analysis/Convex/Legendre/Conjugate.lean (new):
  • IsLegendre.injOn_fderiv
  • IsLegendre.mapsTo_fderiv
  • IsLegendre.surjOn_fderiv
  • IsLegendre.bijOn_fderiv
  • IsLegendre.fderiv_toReal_fenchelConjugateOn_fderiv
  • IsLegendre.fderiv_toReal_fenchelConjugateOn_eq_apply_iff
  • IsLegendre.bregDiv_toReal_fenchelConjugateOn
  • IsLegendre.toReal_fenchelConjugateOn (F⋆ is Legendre)
• Conjugate.lean: convexOn_toReal_fenchelConjugateOn (the conjugate is convex on its effective domain, through Tau Ceti's convexOn_toReal and convex_epigraph_fenchelConjugate)
• Legendre/Basic.lean: IsLegendre.existsUnique_isMinOn_inter_of_isBounded

Module moves (git mv plus the module docstring, no declaration renames; nothing imported the old path):

old	new
LMLExplore.Analysis.Convex.Legendre	LMLExplore.Analysis.Convex.Legendre.Basic

No public declaration is removed or renamed. The informal sources are [LS, Theorem 26.6] and Rockafellar, Convex Analysis, Theorem 26.5, both cited in the module docstring. No Mathlib material is vendored.

🤖 Prepared with Claude Code

[prevostad]

AI review — changes requested

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	The new statements faithfully formalize [LS, Theorem 26.6] (a)–(c): the bijection between interiors with ∇F⋆ as its inverse (via the injective evaluation map into the bidual), Bregman duality with arguments and derivative point in the right order, and the conjugate being Legendre on its effective domain; the generalized minimization lemma's hypotheses are genuine. Edge cases (empty D giving ⊥ with real representative 0, finiteness off ⊤) check out.
✅	reuse	approved	claude/claude-opus-5-5	The Theorem 26.6 declarations are new material built on existing LMLExplore lemmas (StrictConvexOn.injOn_of_hasFDerivWithinAt, ConvexOn.strictConvexOn_of_injOn, ConvexOn.tendsto_norm_comp_atTop_of_steep, hasFDerivAt_toReal_fenchelConjugateOn) and Tau Ceti's convexOn_toReal/convex_epigraph_fenchelConjugate; no duplicate was found in the checked-out code or Mathlib (Tau Ceti's source is not in the checkout, so it was not searched). The old existsUnique_isMinOn_inter is now a corollary of the new bounded-sublevel version, so no parallel proof is left.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the stated target of Bandits Layer 6 item 1, [LS, Theorem 26.6] (roadmap/LMLRoadmaps/Bandits/README.md:491-492). The generalised minimisation lemma, the convexity of the conjugate and the Legendre → Legendre/Basic move each feed the new theorem directly, so the PR is one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new Legendre/Conjugate.lean module cites its informal sources, [LS, Theorem 26.6] and Rockafellar's Convex Analysis Theorem 26.5, and the moved Legendre/Basic.lean keeps its [LS]/Rockafellar references. Nothing is vendored or closely adapted from an uncredited formal source.
🟡	api-design	changes requested	claude/claude-opus-5-5	The new public surface matches [LS, Theorem 26.6] (a)–(c) and the module move leaves no compatibility layer, but two general facts about the bidual are kept private inside LMLExplore.IsLegendre instead of being public in a general file.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: finite-dimensionality is assumed only where the underlying conjugate differentiability/interior lemmas require it (Conjugate.lean FiniteDimensional section), and existsUnique_isMinOn_inter is now a corollary of the more general bounded-sublevel version rather than a duplicated proof.
✅	placement	approved	claude/claude-opus-5-5	The Legendre directory move is complete with no stale references, the new Conjugate.lean imports are all used, and the general conjugate-convexity lemma sits in the general Conjugate file next to its dependencies. The prior stale-docstring finding is fixed in this revision.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology (injOn/mapsTo/surjOn/bijOn, _iff on a genuine Iff, _of_isBounded for the added hypothesis) and follow local precedent such as IsLegendre.bregDiv for IsLegendre.toReal_fenchelConjugateOn. Namespaces are appropriate and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The prior stale module-path reference in Bregman/Projection.lean is fixed, and no reference to the old Legendre module path remains. The new Legendre/Conjugate module and every new public declaration have accurate docstrings that do not overclaim, and the cross-file module docstrings are updated consistently.
✅	proof-quality	approved	claude/claude-opus-5-5	The earlier findings are fixed: injectivity and norm preservation of the bidual embedding now come from NormedSpace.inclusionInDoubleDualLi, and their reliance on the definition of ContinuousLinearMap.apply is stated in the docstrings. The other proofs are short, have comments, and avoid brittle rewrite chains and undocumented definitional equality.

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

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

[prevostad]

🟡 api-design — request_changes claude/claude-opus-5-5

The new public surface matches [LS, Theorem 26.6] (a)–(c) and the module move leaves no compatibility layer, but two general facts about the bidual are kept private inside LMLExplore.IsLegendre instead of being public in a general file.

• LMLExplore/Analysis/Convex/Legendre/Conjugate.lean:61 — apply_injective and norm_apply are general facts about ContinuousLinearMap.apply ℝ ℝ : E → (E →L[ℝ] ℝ) →L[ℝ] ℝ (it is injective and preserves the norm). They are hidden as private in the LMLExplore.IsLegendre namespace, but the public ∇F⋆ statements in Analysis/Convex/Conjugate.lean use the same map, so users have to prove these facts again. Fix: Make them public under the ContinuousLinearMap namespace (e.g. ContinuousLinearMap.apply_injective, ContinuousLinearMap.norm_apply_apply) in a general or ForMathlib file that Conjugate.lean can import, and use them from there.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 22s · 85.9k in (77k cache read, 8.9k cache write) / 2.2k out tokens · reviewing this diff · rubric}