[RemyDegenne]

This PR proves the joint continuity of the cost (θ, w) ↦ inf_{θ' ∈ A} cost_θ(w, θ') of a set of alternatives in the model and the allocation, in the two settings of [DK19, Appendix F]: alternatives inside a compact set (Lemma 24), and any set of alternatives, compact or not, on a product model with locally relatively compact sublevel sets of the per-arm divergences (Lemmas 25–27, the non-compact setting of [FKV14]). It also proves the upper semicontinuity of this cost, and its measurability, under weaker hypotheses. The general theorems go into LMLExplore/Identification/Task/Continuity.lean, and their productBandit specialisation into Task/ProductModel.lean, which imports it. That file already derives the continuity of D(θ, ¬i), D(θ), T*(θ) and the upper hemicontinuity of w*(θ, ¬i) from this joint continuity, which so far had been proved only for best arm identification in a single exponential family (continuousOn_altCost_baiTask_restrict).

Roadmap: Identification

Milestones:

• Identification Layer 3.3 (Continuity), second bullet: "Prove the joint continuity of (θ, w) ↦ D(θ, w, A) on ∏_a S_a × [0, ∞)^α, for every set A ⊆ ∏_a S_a of alternatives, compact or not, for a product model …" and "Prove also the joint continuity … when the closure of ¬i in M is compact".
• Identification Layer 3.1, fourth bullet: "Prove that (θ, w) ↦ D(θ, w, ¬i) is upper semicontinuous, hence measurable, on every topological space of models on which θ ↦ KL(ν_a(θ), ν_a(λ)) is real-valued and continuous". The roadmap names this as the upper half of the Layer 3.3 continuity.

After this PR, the third part of that Layer 3.3 bullet remains: checking the per-arm hypotheses for exponential families in the mean parametrization (divergence tending to +∞ at the endpoints of the means) and for the two-parameter Gaussian model. The next bullet then applies these theorems to the oracle answers and allocations, which Task/Oracle.lean takes as hypotheses.

New public declarations, all in LMLExplore.Identification.IdentTask:

• upperSemicontinuousOn_biInf_cost: if every θ ↦ KL(ν_a(θ), ν_a(θ')), for θ' ∈ A, is finite and continuous on s, the cost of A is upper semicontinuous on s ×ˢ univ. upperSemicontinuous_altCost is the global form for D(θ, w, ¬i), and measurable_altCost follows from it through Mathlib's UpperSemicontinuous.measurable.
• continuousOn_biInf_cost_of_isCompact, continuousOn_altCost_of_isCompact: for A ⊆ K with K compact, and real divergences KL(ν_a(θ), ν_a(θ')) = k a θ θ' continuous on s ×ˢ K, the cost is continuous on s ×ˢ univ. The roadmap states this for divergences continuous on M × M with compact closure of ¬i in M. That is the case s = M, with K that closure.
• continuousOn_biInf_cost_pi, continuousOn_altCost_pi: for models θ : α → Θ₀ whose divergences on ∏ a, S a are real per-arm divergences k a (θ a) (θ' a) continuous on S a ×ˢ S a, with the relative-compactness hypothesis of the roadmap (every x ∈ S a has a neighbourhood U in S a such that {y ∈ S a | ∃ x' ∈ U, k a x' y ≤ r} lies in a compact subset of S a for every r), the cost of every A ⊆ ∏ a, S a is continuous on (∏ a, S a) ×ˢ univ.
• continuousOn_biInf_cost_productBandit, continuousOn_altCost_productBandit (in Task/ProductModel.lean): the specialisation to task.ν = productBandit κ, with the hypotheses on klDiv (κ a x) (κ a y) in ℝ≥0∞ as in the roadmap's continuousOn_iInf_cost_productBandit (finite, continuous on S a ×ˢ S a, sublevel sets for finite r locally in compact subsets of S a). They instantiate k a x y = (klDiv (κ a x) (κ a y)).toReal.
• continuousOn_gameValue_pi, continuousOn_charTime_pi: with finitely many answers and task.M ⊆ ∏ a, S a, D(θ) and T*(θ) are continuous on task.M. These show the product theorem discharging the hypothesis of the existing continuousWithinAt_gameValue and continuousWithinAt_charTime.

Design notes:

• The divergence hypothesis is stated per pair of models (hν : ∀ θ ∈ univ.pi S, ∀ θ' ∈ univ.pi S, ∀ a, klDiv (task.ν θ a) (task.ν θ' a) = ENNReal.ofReal (k a (θ a) (θ' a))), not as task.ν = productBandit κ. This covers productBandit κ (with k a x y = (klDiv (κ a x) (κ a y)).toReal), and also the vectors of means of per-arm exponential families in the style of IsDivergenceOn from Task/ExpFamily.lean. It also avoids importing Task/ProductModel.lean, which imports this file through Task/BestArm/Basic.lean.
• The continuity holds for all allocations w : α → ℝ, not only [0, ∞)^α, because cost counts a negative weight as 0 through ENNReal.ofReal.
• The proof does not go through Topology/Semicontinuity/Berge.lean, because Berge's theorem takes the infimum over a compact set, and A need not be compact. The lower semicontinuity is a direct argument. Near (θ, w), an alternative of cost at most r has its coordinates of positive weight in the compact sets given by the hypothesis. On those sets the per-arm costs converge uniformly, by Mathlib's IsCompact.mem_uniformity_of_prod. The coordinates of zero weight only add a nonnegative term. The two lower semicontinuity lemmas and the per-arm step are private, since the public continuity theorems subsume them.

References: [DK19] R. Degenne and W. M. Koolen, Pure exploration with multiple correct answers, NeurIPS 2019, supplementary material, Appendix F (Theorems 22–23, Lemmas 24–27). [FKV14] E. A. Feinberg, P. O. Kasyanov and M. Voorneveld, Berge's maximum theorem for noncompact image sets, J. Math. Anal. Appl. 413 (2014). Both are cited in the file. No Mathlib material is vendored. The PR removes or renames no public declaration.

🤖 Prepared with Claude Code

[RemyDegenne]

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	The upper semicontinuity, measurability, compact-alternatives [DK19, Lemma 24] and product-model [DK19, Lemmas 25–27] continuity statements match or slightly generalize the roadmap's Layer 3.1/3.3 claims, with non-vacuous hypotheses (satisfied by Gaussian and Bernoulli families) and no content moved into assumptions. The D(θ)/T*(θ) corollaries prove the existing continuousWithinAt_gameValue/continuousWithinAt_charTime hypothesis instead of assuming it.
✅	reuse	approved	claude/claude-opus-5-5	The new semicontinuity and continuity results for the cost of a set of alternatives use Mathlib's upperSemicontinuousOn_biInf, IsCompact.mem_uniformity_of_prod and UpperSemicontinuous.measurable, and no existing declaration already states them. The private expansion lemma differs from cost_eq_sum_ofReal_mul (Task/ExpFamily.lean:184), which requires 0 ≤ w and models α → ℝ, and from cost_eq_sum_of_ν_eq_productBandit, which sits in a file that imports this one.
✅	scope	approved	claude/claude-opus-5-5	Directly implements the Identification Layer 3.3 joint-continuity bullet (README.md:569–581, product-model non-compact and compact cases) and the Layer 3.1 upper-semicontinuity/measurability bullet (README.md:551–554), and wires the result into the existing D(θ)/T*(θ) continuity as README.md:592–595 anticipates. One coherent topic; the remaining per-arm checks for exponential families and the Gaussian model are stated as follow-up work.
✅	attribution	approved	claude/claude-opus-5-5	The central informal sources, [DK19] Appendix F (Theorems 22–23, Lemmas 24–27) and [FKV14], are cited in the module references and theorem docstrings of both touched files, matching the roadmap's citation for this milestone. No formal material is vendored, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The roadmap's productBandit continuity target is now stated with klDiv hypotheses in ℝ≥0∞, alongside the general per-arm k theorems and the altCost, gameValue and charTime forms. The private helpers serve only their proofs, no bodies are exposed, and no compatibility code is added.
✅	generality	approved	claude/claude-opus-5-5	The upper semicontinuity, compact-case and product-case continuity theorems are stated for arbitrary sets of alternatives and all allocations, with the altCost/productBandit/gameValue/charTime results as thin corollaries. All hypotheses are used and match or weaken the roadmap's level; the existing BAI-specific continuity is a separate closed-form argument, not a special-case duplicate.
✅	placement	approved	claude/claude-opus-5-5	The general joint-continuity theorems sit in Task/Continuity.lean, the home of the continuity results and their consequences, and the productBandit specialisations sit in Task/ProductModel.lean, which imports it through Task/BestArm/Basic.lean. Both new Mathlib imports are specific and used: HeineCantor for IsCompact.mem_uniformity_of_prod and BorelSpace.Order for UpperSemicontinuous.measurable.
✅	naming	approved	claude/claude-opus-5-5	New public names (upperSemicontinuousOn_biInf_cost, upperSemicontinuous_altCost, measurable_altCost, continuousOn_biInf_cost_of_isCompact, continuousOn_altCost_pi, continuousOn_biInf_cost_productBandit, continuousOn_gameValue_pi, continuousOn_charTime_pi, etc.) describe their conclusions in standard terminology, with biInf correctly naming the bounded infimum, consistent with the existing continuousOn_altCost_baiTask_restrict and continuousWithinAt_gameValue. No notation is introduced and no name overstates its statement.
✅	documentation	approved	claude/claude-opus-5-5	Module docstrings and all new public declarations describe their statements accurately, including the finite-r, all-allocations, finitely-many-answers and admissible-models hypotheses; no process or roadmap narrative in the files.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are well factored: the one-arm step, the 2r/v bound, the finite-sum estimate and the choice of r₂ < r are separate lemmas, and the remaining ~65-line lower-semicontinuity proof has a comment for each phase. No change/show, no undocumented defeq, and only short rewrite steps.

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

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