[prevostad]

This PR characterises the interior of the effective domain of Tau Ceti's Legendre–Fenchel conjugate, for the pairing of a real normed space E with its dual. A functional u is interior to {v | f⋆ v ≠ ⊤} exactly when the tilt f - u grows at least linearly, u x + r ‖x‖ - M ≤ f x with r > 0. As a consequence, the tilted sublevel sets {x | f x ≤ u x + c} are bounded. It serves 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^*$, …"). The surjectivity half of that bijection, ∇F onto the interior of the domain of F⋆, consumes isBounded_setOf_le_of_mem_interior_setOf_fenchelConjugate_ne_top. Given u in that interior, it bounds a minimizing sequence of F - u on D. That gives a minimizer, which steepness ([LS, Corollary 26.8]) puts in the interior, where ∇F = u.

Roadmap: Bandits

After this PR, Layer 6.1 still needs the surjectivity argument itself and the fact that F⋆ is Legendre. Both are stated with the IsLegendre predicate of the open #289 and the conjugate on a set of the open #319, so they wait for those two PRs to merge. This PR depends on neither. It is stated with TauCeti.fenchelConjugate (topDualPairing ℝ E).flip, which #319's fenchelConjugateOn_eq_fenchelConjugate identifies with fenchelConjugateOn F D.

LMLExplore/Analysis/Convex/Coercive.lean (new, 141 lines):

• fenchelConjugate_le_of_norm_sub_le: in any real normed space, if u x + r ‖x‖ - M ≤ f x for every x, then f⋆ v ≤ M for ‖v - u‖ ≤ r.
• mem_interior_setOf_fenchelConjugate_ne_top_of_forall_le: hence u is interior to the domain of f⋆ when r > 0.
• exists_forall_le_of_mem_interior_setOf_fenchelConjugate_ne_top: the converse, in finite dimension. Tau Ceti's convexOn_toReal and convex_epigraph_fenchelConjugate make the real representative of f⋆ convex on its domain. Mathlib's ConvexOn.continuousOn_interior then bounds it above near u. The Fenchel–Young inequality at u + (ρ/2) φ, with φ a norming functional of x (exists_dual_vector''), gives the growth bound.
• mem_interior_setOf_fenchelConjugate_ne_top_iff: the two directions together, in finite dimension.
• isBounded_setOf_le_of_mem_interior_setOf_fenchelConjugate_ne_top: bounded tilted sublevel sets.

The statements take an arbitrary f : E → EReal, with no convexity, lower semicontinuity or properness. The case f ≡ ⊤ (where f⋆ ≡ ⊥) is covered. I searched Mathlib, Tau Ceti, LML and LMLExplore for an existing statement. Tau Ceti's tendsto_sub_atTop_of_superlinear (Analysis/Convex/Superlinear.lean) goes the other way: superlinear h makes every tilt coercive. It says nothing about the domain of the conjugate. Nothing else relates the interior of the domain of a conjugate to growth of tilts. No Mathlib infrastructure was vendored.

Sources: R. T. Rockafellar, Convex Analysis, Theorem 10.1 and Section 14; T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Section 26.5, 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 five statements are faithful under the conjugate convention sup_x (v x - f x), which the proofs pin down via fenchelConjugate_le and sub_le_fenchelConjugate; the growth/interior equivalence in finite dimension and the bounded tilted sublevel sets are correct, including the f ≡ ⊤, f = ⊥ somewhere, and trivial-E edge cases. No vacuity, placeholders, or over-strong assumptions; FiniteDimensional appears only where the converse genuinely uses it.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration relates the interior of the conjugate's domain to linear growth of tilts or yields bounded tilted sublevel sets; the proofs reuse Tau Ceti's conjugate API and Mathlib's ConvexOn.continuousOn_interior and exists_dual_vector'' rather than re-deriving them.
✅	scope	approved	claude/claude-opus-5-5	New material proves the bounded tilted sublevel sets that the surjectivity of ∇F onto the interior of dom F⋆ needs in [LS, Theorem 26.6], the Bandits Layer 6.1 'Legendre functions' target (Bandits/README.md:487-493). It is a direct prerequisite, delivered as one coherent file.
✅	attribution	approved	claude/claude-opus-5-5	The file cites its informal sources, Rockafellar (Theorem 10.1 and Section 14) and Lattimore–Szepesvári (Section 26.5, Theorem 26.6), and the docstring and description name the central Mathlib and Tau Ceti lemmas the proof uses. No earlier formalization of this result exists in the repository, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds five public theorems and no definitions: the growth-to-interior direction (valid in any normed space), its finite-dimensional converse, the iff combining them, and the bounded tilted sublevel sets result that the Layer 6.1 surjectivity argument needs. No compatibility layer, hidden general infrastructure, duplicate API, or missing annotation was found.
✅	generality	approved	claude/claude-opus-5-5	The growth-to-interior direction holds in every real normed space, and FiniteDimensional appears only where ConvexOn.continuousOn_interior needs it; the Banach-space converse would need lower-semicontinuous convex continuity, which Mathlib lacks. f is an arbitrary E → EReal with no unused hypotheses, and the iff and bounded-sublevel results are derived from the two directions rather than proved again.
✅	placement	approved	claude/claude-opus-5-5	The new generic file Analysis/Convex/Coercive.lean sits in the existing convex-analysis directory, has no flat Coercive* sibling, and has no earlier LMLExplore home for conjugate-domain material. Each import matches material the file uses, and none is a broad import Mathlib.
✅	naming	approved	claude/claude-opus-5-5	Declaration names describe their conclusions in standard Mathlib terminology (fenchelConjugate_le_of_…, mem_interior_setOf_…_ne_top, exists_forall_le_of_…, isBounded_setOf_le_of_…), and the only _iff lemma is a genuine Iff. Everything is in the LMLExplore namespace and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring now correctly says the converse is proved here for finite-dimensional E, which fixes the earlier finding that it wrongly called finite dimension necessary; every public theorem's docstring matches its statement. The module docstring states the mathematical purpose without roadmap or process narrative, and cites Rockafellar and Lattimore–Szepesvári.
✅	proof-quality	approved	claude/claude-opus-5-5	The proofs are short and use simp only, rw and linarith/gcongr steps without long brittle rewrite chains or change/show. The one non-trivial proof (the finite-dimensional converse) is commented at each structural step, and the iff and boundedness results reuse the directional lemmas.

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

_{Reviewing this diff at head 329725d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.55.}