[RemyDegenne]

This PR restates the Gaussian closed forms of thresholding, minimum threshold and Any Low Arm for Gaussian arms with arm-dependent known variances v a, the arm laws ν μ a = 𝒩(μ a, v a) (for instance Bandits.gaussianMeanVarBandit fun a ↦ (μ a, v a)), and derives the common-variance statements from them as the case of a constant v.

Roadmap: Generalization

Target: Generalization 1.8, "Gaussian thresholding, minimum threshold and Any Low Arm with arm-dependent variances" (after 1.6, merged in #278). This PR meets the target. Next on that path is Identification 3.6, which this target unblocks. Target 1.9 (half-spaces and best arm identification with arm-dependent variances) is a separate target.

The arm-dependent forms use the convention that Task/HalfSpace.lean (Identification 3.6) and IdentTask.cost_gaussianReal already use: a hypothesis hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a) with hv : ∀ a, v a ≠ 0, and the suffix _gaussianReal. The Gaussian bandits with means and variances satisfy hν by gaussianMeanVarBandit_apply. gaussianBandit · σ2 satisfies it by gaussianBandit_apply, which is how the common-variance statements are derived. So the bridge gaussianBandit_eq_gaussianMeanVarBandit is not needed.

New statements:

• altCost_thresholdingTask_gaussianReal: D(μ, w, ¬s) = min_a w a (μ a - γ)² / (2 v a).
• charTime_thresholdingTask_gaussianReal, charTime_minThresholdTask_gaussianReal_false: T*(μ) = ∑ a, 2 v a / (μ a - γ)².
• charTime_minThresholdTask_gaussianReal_true: T*(μ) = 2 v a₀ / (μ a₀ - γ)² for an arm a₀ below γ that maximizes (μ a - γ)² / v a among the arms below γ. With arm-dependent variances, this arm is no longer an arm of smallest mean.
• oracleAlloc_anyLowArmTask_gaussianReal: the oracle allocations are the vertices of the arms below γ that maximize (μ a - γ)² / v a.
• klDiv_eq_ofReal_expFamilyDiv_gaussianReal (Task/ExpFamily.lean): such arms have the divergences of the exponential families of the 𝒩(0, v a). All five proofs feed this to the IsDivergenceOn lemmas of target 1.6.

Restated statements. They keep their names and their signatures, and are now one-line corollaries: altCost_thresholdingTask_gaussianBandit, charTime_thresholdingTask_gaussianBandit, charTime_minThresholdTask_gaussianBandit_false, charTime_minThresholdTask_gaussianBandit_true and oracleAlloc_anyLowArmTask_gaussianBandit (the last one keeps a short set computation that identifies the maximizing arms with the arms of smallest mean). As the roadmap asks, not_convex_oracleAlloc_anyLowArmTask_gaussianBandit keeps a common variance. IdentTask.cost_gaussianBandit was already derived on main from IdentTask.cost_gaussianReal, which takes arm-dependent variances, so this PR leaves it unchanged. In both files the Gaussian statements now sit in one final section Gaussian, because they need ν : (α → ℝ) → Kernel α ℝ instead of the sections' explicit ν valued in 𝓨.

Generalized declaration (same name, no removals): LMLExplore.setOf_forall_mem_expFamilyMeans_gaussianReal now takes per-index variances {v : ι → ℝ≥0} (hv : ∀ i, v i ≠ 0). Callers with a common variance pass (fun _ ↦ hσ2) (Task/BestArm/Basic.lean, Task/BestArm/StaticProportions.lean, Task/Threshold/StaticProportions.lean). No public declaration is removed or renamed.

🤖 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 arm-dependent-variance statements give the correct Gaussian closed forms: thresholding cost and characteristic time, both minimum-threshold cases (with the arm maximizing (μ a − γ)²/v a among the arms below γ in place of the smallest mean), and the Any Low Arm oracle allocations. The hypotheses hν/hv fix the intended model, gaussianBandit_apply and gaussianMeanVarBandit_apply satisfy hν by rfl, and the common-variance corollaries keep their exact statements.
✅	reuse	approved	claude/claude-opus-5-5	The arm-dependent KL bridge klDiv_eq_ofReal_expFamilyDiv_gaussianReal, the expFamilyDiv_gaussianReal_max_* helpers and the _gaussianReal closed forms have no counterpart in Mathlib or LMLExplore and are assembled from klDiv_gaussianReal_gaussianReal_same_var, expFamilyDiv_gaussianReal, expFamilyDiv_self and the generic IsDivergenceOn lemmas. The common-variance statements are now one-line corollaries via gaussianBandit_apply, matching the existing cost_gaussianBandit/cost_gaussianReal pattern.
✅	scope	approved	claude/claude-opus-5-5	Implements Generalization target 1.8 (roadmap/LMLRoadmaps/Generalization/README.md:422-433) as one unit: the five Gaussian thresholding, minimum threshold and Any Low Arm closed forms are restated with arm-dependent variances, the common-variance versions become corollaries, and the non-convexity example keeps a common variance, as the target asks. The supporting lemmas (klDiv_eq_ofReal_expFamilyDiv_gaussianReal, the max-divergence helpers, per-index setOf_forall_mem_expFamilyMeans_gaussianReal) are direct prerequisites, and IdentTask.cost_gaussianBandit is already derived from cost_gaussianReal (Task/ExpFamily.lean:376,398).
✅	attribution	approved	claude/claude-opus-5-5	The arm-dependent-variance Gaussian closed forms are routine specializations of the project's own IsDivergenceOn lemmas. They keep their citations to DK19 and KKG18, and both papers are listed in the References sections of Threshold/Basic.lean and AnyLowArm.lean.
✅	api-design	approved	claude/claude-opus-5-5	Arm-dependent-variance _gaussianReal statements and Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal follow the existing hν/hv convention, the common-variance forms are genuine corollaries rather than compatibility wrappers, and setOf_forall_mem_expFamilyMeans_gaussianReal is generalized in place with all callers updated. The public expFamilyDiv_gaussianReal_max_* helpers are consumed by AnyLowArm.lean and are task-specific, so their exposure and placement are justified.
✅	generality	approved	claude/claude-opus-5-5	Each Gaussian closed form is proved once with arm-dependent variances v a, and the common-variance statements are one-line specializations; setOf_forall_mem_expFamilyMeans_gaussianReal is generalized to per-index variances. The earlier finding about an over-specific helper is resolved: expFamilyDiv_gaussianReal_max_of_le has been removed, and the remaining helpers use the variance they take.
✅	placement	approved	claude/claude-opus-5-5	The new KL bridge sits in Bandits/Instances.lean next to the common-variance lemma it generalizes, the task-specific expFamilyDiv_gaussianReal_max_* helpers sit in Threshold/Basic.lean where both they and AnyLowArm.lean use them, and the generalized setOf_forall_mem_expFamilyMeans_gaussianReal stays in its home. No import changes and nothing is misplaced.
✅	naming	approved	claude/claude-opus-5-5	The new _gaussianReal declarations match the arm-dependent-variance naming already used in Task/HalfSpace.lean, and klDiv_eq_ofReal_expFamilyDiv_gaussianReal, expFamilyDiv_gaussianReal_max_of_lt and expFamilyDiv_gaussianReal_max_pos describe their conclusions in standard terms. No notation is introduced and nothing sits in the wrong namespace.
✅	documentation	approved	claude/claude-opus-5-5	Docstrings for the new arm-dependent-variance theorems, the two max-divergence helpers, the KL bridge lemma (whose gaussianMeanVarBandit claim is confirmed by gaussianMeanVarBandit_apply) and the restated common-variance corollaries match their statements, and the module summaries were updated consistently. No stale, overclaiming or process-oriented documentation found.
✅	proof-quality	approved	claude/claude-opus-5-5	The arm-dependent Gaussian proofs are short and rely on the shared expFamilyDiv_gaussianReal_max_of_lt/_pos lemmas, and the common-variance statements are clean one-line corollaries via gaussianBandit_apply. There is no undocumented defeq manipulation or brittle unfolding-heavy automation.

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

_{Reviewing this diff at head 9d9ef47. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.67.}