From d41d3e982f407bc30b8307d614e8872b4f09ef44 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 12 Nov 2026 09:33:14 +0100
Subject: [PATCH 1/3] feat: Gaussian thresholding, minimum threshold and Any
 Low Arm with arm-dependent variances

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/Identification/Task/AnyLowArm.lean | 114 ++++++---
 .../Identification/Task/BestArm/Basic.lean    |   4 +-
 .../Task/BestArm/StaticProportions.lean       |   3 +-
 LMLExplore/Identification/Task/ExpFamily.lean |  14 +
 .../Identification/Task/Threshold/Basic.lean  | 239 +++++++++++-------
 .../Task/Threshold/StaticProportions.lean     |   4 +-
 .../ExponentialFamily/Gaussian.lean           |  10 +-
 7 files changed, 251 insertions(+), 137 deletions(-)

diff --git a/LMLExplore/Identification/Task/AnyLowArm.lean b/LMLExplore/Identification/Task/AnyLowArm.lean
index c59f079..f8f8da0 100644
--- a/LMLExplore/Identification/Task/AnyLowArm.lean
+++ b/LMLExplore/Identification/Task/AnyLowArm.lean
@@ -34,8 +34,9 @@ the mean parametrization on its set of means, and let `γ` be in every `S_a`.
   [DK19, Proposition 5]: the convexity of each `w*(μ, ¬i)` does not extend to `w*(μ)`. This is why
   the guarantee of Track-and-Stop for tasks with multiple correct answers involves the convex hull
   of `w*(μ)`, and why the sticky variant of Degenne and Koolen commits to one oracle answer. For
-  Gaussian arms with a common variance, the oracle allocations are the vertices of the arms of
-  smallest mean, and two arms with the same smallest mean below `γ` give this non-convex set.
+  Gaussian arms with known variances `v a`, the oracle allocations are the vertices of the arms
+  below `γ` maximizing `(μ a - γ)² / v a`. With a common variance, these are the arms of smallest
+  mean, and two arms with the same smallest mean below `γ` give this non-convex set.
 
 The costs are computed on the vectors of means in `S`, `{λ | ∀ c, λ c ∈ S c}`, as for
 thresholding and minimum threshold. The statements follow those of the formalization of
@@ -65,6 +66,9 @@ thresholding and minimum threshold. The statements follow those of the formaliza
   allocations are their vertices `Pi.single a 1`.
 * `LMLExplore.Identification.not_convex_oracleAlloc_anyLowArmTask_restrict`: if two distinct arms
   maximize `d_a(μ a, max (μ a) γ)`, the oracle allocations are not convex [DK19, Proposition 5].
+* `LMLExplore.Identification.oracleAlloc_anyLowArmTask_gaussianReal`: for Gaussian arms with
+  variances `v a` and some mean below `γ`, the oracle allocations are the vertices of the arms
+  below `γ` maximizing `(μ a - γ)² / v a`.
 * `LMLExplore.Identification.oracleAlloc_anyLowArmTask_gaussianBandit`,
   `LMLExplore.Identification.not_convex_oracleAlloc_anyLowArmTask_gaussianBandit`: for Gaussian
   arms with a common variance and a smallest mean below `γ`, the oracle allocations are the vertices
@@ -436,57 +440,95 @@ theorem not_convex_oracleAlloc_anyLowArmTask_restrict (hd : ∀ a, IsDivergenceO
 
 /-! ### Gaussian arms -/
 
-variable [MeasurableSingletonClass α] {σ2 : ℝ≥0}
+section Gaussian
 
-/-- **The oracle allocations of Gaussian Any Low Arm** [DK19, Example 1]. For Gaussian arms with a
-common variance `σ2 ≠ 0` and a vector of means `μ` whose smallest mean `μ a₀` is below `γ`, the
-oracle allocations are the vertices `Pi.single a 1` of the arms `a` of smallest mean. -/
-theorem oracleAlloc_anyLowArmTask_gaussianBandit [DecidableEq α] (hσ2 : σ2 ≠ 0) {a₀ : α}
-    (ha₀ : ∀ a, μ a₀ ≤ μ a) (hγ : μ a₀ < γ) :
-    (anyLowArmTask (Bandits.gaussianBandit · σ2) id γ).oracleAlloc μ =
-      (fun a ↦ Pi.single a 1) '' {a | μ a = μ a₀} := by
-  rw [← (anyLowArmTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
+variable {ν : (α → ℝ) → Kernel α ℝ} [∀ μ, IsMarkovKernel (ν μ)] {v : α → ℝ≥0}
+
+/-- **The oracle allocations of Gaussian Any Low Arm** [DK19, Example 1]. For Gaussian arms with
+variances `v a ≠ 0` and a vector of means `μ` with some mean below `γ`, the oracle allocations are
+the vertices `Pi.single a 1` of the arms `a` below `γ` that maximize `(μ a - γ)² / v a` among the
+arms below `γ`. -/
+theorem oracleAlloc_anyLowArmTask_gaussianReal [DecidableEq α] (hv : ∀ a, v a ≠ 0)
+    (hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a)) (h : ∃ b, μ b < γ) :
+    (anyLowArmTask ν id γ).oracleAlloc μ = (fun a ↦ Pi.single a 1) ''
+      {a | μ a < γ ∧ ∀ b, μ b < γ → (μ b - γ) ^ 2 / v b ≤ (μ a - γ) ^ 2 / v a} := by
+  rw [← (anyLowArmTask ν id γ).restrict_univ,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hv,
     oracleAlloc_anyLowArmTask_restrict_of_exists_lt
-      (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
-      (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ') ⟨a₀, hγ⟩]
-  simp only [expFamilyDiv_gaussianReal 0 hσ2]
+      (S := fun a ↦ (gaussianReal 0 (v a)).expFamilyMeans id) _
+      (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') h]
+  simp only [expFamilyDiv_gaussianReal 0 (hv _)]
   congr 1
-  -- The arms maximizing `(μ a - max (μ a) γ)² / (2 σ2)` are those of smallest mean.
-  have hσ2' : 0 < 2 * (σ2 : ℝ) := by
-    have := NNReal.coe_pos.2 (pos_iff_ne_zero.2 hσ2)
+  -- The divergence `(μ a - max (μ a) γ)² / (2 v a)` of an arm is `(μ a - γ)² / (2 v a) > 0` if
+  -- the arm is below `γ`, and `0` otherwise.
+  have h_lt (a : α) (ha : μ a < γ) :
+      (μ a - max (μ a) γ) ^ 2 / (2 * v a) = (μ a - γ) ^ 2 / v a / 2 := by
+    rw [max_eq_right ha.le, div_mul_eq_div_div_swap]
+  have h_ge (a : α) (ha : γ ≤ μ a) : (μ a - max (μ a) γ) ^ 2 / (2 * v a) = 0 := by
+    rw [max_eq_left ha, sub_self, zero_pow two_ne_zero, zero_div]
+  have h_pos (a : α) (ha : μ a < γ) : 0 < (μ a - γ) ^ 2 / v a := by
+    have : 0 < (v a : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 (hv a))
+    have : 0 < (μ a - γ) ^ 2 := by nlinarith [mul_pos (sub_pos.2 ha) (sub_pos.2 ha)]
     positivity
+  obtain ⟨b₀, hb₀⟩ := h
+  ext a
+  simp only [Set.mem_ofPred_eq]
+  constructor
+  · intro ha
+    -- A maximizing arm is below `γ`, since the arms above `γ` have divergence `0`.
+    have hlt : μ a < γ := by
+      by_contra hge
+      have h_le := ha b₀
+      rw [h_lt b₀ hb₀, h_ge a (not_lt.1 hge)] at h_le
+      linarith [h_pos b₀ hb₀]
+    refine ⟨hlt, fun b hb ↦ ?_⟩
+    have h_le := ha b
+    rw [h_lt b hb, h_lt a hlt] at h_le
+    linarith
+  · rintro ⟨hlt, ha⟩ b
+    rw [h_lt a hlt]
+    rcases lt_or_ge (μ b) γ with hb | hb
+    · rw [h_lt b hb]
+      linarith [ha b hb]
+    · rw [h_ge b hb]
+      linarith [h_pos a hlt]
+
+/-- **The oracle allocations of Gaussian Any Low Arm with a common variance** [DK19, Example 1].
+For Gaussian arms with a common variance `σ2 ≠ 0` and a vector of means `μ` whose smallest mean
+`μ a₀` is below `γ`, the oracle allocations are the vertices `Pi.single a 1` of the arms `a` of
+smallest mean. -/
+theorem oracleAlloc_anyLowArmTask_gaussianBandit [MeasurableSingletonClass α] [DecidableEq α]
+    {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {a₀ : α} (ha₀ : ∀ a, μ a₀ ≤ μ a) (hγ : μ a₀ < γ) :
+    (anyLowArmTask (Bandits.gaussianBandit · σ2) id γ).oracleAlloc μ =
+      (fun a ↦ Pi.single a 1) '' {a | μ a = μ a₀} := by
+  rw [oracleAlloc_anyLowArmTask_gaussianReal (v := fun _ ↦ σ2) (fun _ ↦ hσ2)
+    (Bandits.gaussianBandit_apply · σ2) ⟨a₀, hγ⟩]
+  congr 1
+  -- The arms below `γ` farthest from `γ` are those of smallest mean.
+  have hσ2' : 0 < (σ2 : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 hσ2)
   ext a
   simp only [Set.mem_ofPred_eq, div_le_div_iff_of_pos_right hσ2']
   constructor
+  · rintro ⟨hlt, ha⟩
+    nlinarith [ha a₀ hγ, ha₀ a]
   · intro ha
-    have h_le := ha a₀
-    rw [max_eq_right hγ.le] at h_le
-    rcases le_or_gt γ (μ a) with h | h
-    · rw [max_eq_left h, sub_self] at h_le
-      nlinarith [mul_pos (sub_pos.2 hγ) (sub_pos.2 hγ)]
-    · rw [max_eq_right h.le] at h_le
-      nlinarith [ha₀ a]
-  · intro ha b
-    rw [ha, max_eq_right hγ.le]
-    rcases le_total (μ b) γ with h | h
-    · rw [max_eq_right h]
-      nlinarith [ha₀ b]
-    · rw [max_eq_left h, sub_self]
-      simpa using sq_nonneg (μ a₀ - γ)
+    exact ⟨ha ▸ hγ, fun b _ ↦ by nlinarith [ha₀ b]⟩
 
 /-- **A model of Gaussian Any Low Arm with non-convex oracle allocations** [DK19, Proposition 5].
 For Gaussian arms with a common variance `σ2 ≠ 0`, if two distinct arms `a` and `b` share the
 smallest mean `μ a = μ b < γ`, then the oracle allocations `w*(μ)`, which contain the vertices
 `Pi.single a 1` and `Pi.single b 1` but not their midpoint, are not convex. -/
-theorem not_convex_oracleAlloc_anyLowArmTask_gaussianBandit (hσ2 : σ2 ≠ 0) {a b : α}
+theorem not_convex_oracleAlloc_anyLowArmTask_gaussianBandit [MeasurableSingletonClass α]
+    {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {a b : α}
     (hab : a ≠ b) (hμab : μ a = μ b) (ha : ∀ c, μ a ≤ μ c) (hγ : μ a < γ) :
     ¬ Convex ℝ ((anyLowArmTask (Bandits.gaussianBandit · σ2) id γ).oracleAlloc μ) := by
   classical
   rw [oracleAlloc_anyLowArmTask_gaussianBandit hσ2 ha hγ]
   exact not_convex_image_single (s := {c | μ c = μ a}) rfl hμab.symm hab
 
+end Gaussian
+
 end LMLExplore.Identification
diff --git a/LMLExplore/Identification/Task/BestArm/Basic.lean b/LMLExplore/Identification/Task/BestArm/Basic.lean
index cab5dc6..108f925 100644
--- a/LMLExplore/Identification/Task/BestArm/Basic.lean
+++ b/LMLExplore/Identification/Task/BestArm/Basic.lean
@@ -1215,7 +1215,7 @@ theorem altCost_baiTask_gaussianBandit (hσ2 : σ2 ≠ 0) (ha : ∀ b, μ b ≤
       ⨅ (b) (_ : b ≠ a),
         ENNReal.ofReal (w a * w b / (w a + w b) * (μ a - μ b) ^ 2 / (2 * σ2)) := by
   rw [← (baiTask (Bandits.gaussianBandit · σ2) id).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 (fun _ ↦ hσ2),
     altCost_baiTask_restrict_eq_iInf_expFamilyPairCost _ (not_ae_eq_const_gaussianReal 0 hσ2)
       (fun c ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 (μ c))
       (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ') ha hw]
@@ -1243,7 +1243,7 @@ theorem answerValue_baiTask_gaussianBandit_of_forall_eq_or_eq (hσ2 : σ2 ≠ 0)
       ENNReal.ofReal ((μ a - μ b) ^ 2 / (8 * σ2)) := by
   have hσ2' : (σ2 : ℝ) ≠ 0 := NNReal.coe_ne_zero.2 hσ2
   rw [← (baiTask (Bandits.gaussianBandit · σ2) id).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 (fun _ ↦ hσ2),
     answerValue_baiTask_restrict_eq_expFamilyDiv_of_forall_eq_or_eq _
       (not_ae_eq_const_gaussianReal 0 hσ2) (fun c ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 (μ c))
       (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ') hba hα hμ
diff --git a/LMLExplore/Identification/Task/BestArm/StaticProportions.lean b/LMLExplore/Identification/Task/BestArm/StaticProportions.lean
index 4eb30ba..ae16eb4 100644
--- a/LMLExplore/Identification/Task/BestArm/StaticProportions.lean
+++ b/LMLExplore/Identification/Task/BestArm/StaticProportions.lean
@@ -316,7 +316,8 @@ theorem staticDifficulty_baiTask_gaussianBandit_two {σ2 : ℝ≥0} (hσ2 : σ2
     simp only [expFamilyDiv_gaussianReal 0 hσ2, natParam_gaussianReal 0 hσ2]
     field_simp [sub_ne_zero.2 hμ01]
     ring
-  rw [setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2, IdentTask.restrict_univ, h_val] at h
+  rw [setOf_forall_mem_expFamilyMeans_gaussianReal 0 (fun _ ↦ hσ2), IdentTask.restrict_univ,
+    h_val] at h
   rw [← inv_inv ((baiTask (Bandits.gaussianBandit · σ2) id).staticDifficulty μ), h,
     ← ENNReal.ofReal_inv_of_pos (by positivity), inv_div]
 
diff --git a/LMLExplore/Identification/Task/ExpFamily.lean b/LMLExplore/Identification/Task/ExpFamily.lean
index aa7bd69..a71a8a5 100644
--- a/LMLExplore/Identification/Task/ExpFamily.lean
+++ b/LMLExplore/Identification/Task/ExpFamily.lean
@@ -36,6 +36,8 @@ parametrization have them (`isDivergenceOn_expFamilyDiv`).
 
 * `LMLExplore.Identification.isDivergenceOn_expFamilyDiv`: the divergence `d(μ, μ')` of an
   exponential family in the mean parametrization is a divergence on its means.
+* `LMLExplore.Identification.klDiv_eq_ofReal_expFamilyDiv_gaussianReal`: Gaussian arms with
+  variances `v c ≠ 0` have the divergences of the exponential families of the `𝒩(0, v c)`.
 * `LMLExplore.Identification.IdentTask.cost_eq_sum_ofReal_mul`: on the vectors of means in `S`,
   `cost_μ(w, μ') = ∑ c, w c d_c(μ c, μ' c)`.
 * `LMLExplore.Identification.IdentTask.cost_eq_sum_ofReal_mul_left`: the cost with the free vector
@@ -172,6 +174,18 @@ theorem isDivergenceOn_expFamilyDiv {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧
   monotoneOn_left _ hy := (strictMonoOn_expFamilyDiv_left hT hy).monotoneOn
   antitoneOn_left _ hy := (strictAntiOn_expFamilyDiv_left hT hy).antitoneOn
 
+/-- For Gaussian arms with variances `v c ≠ 0`, the arm `c` has the divergence of the exponential
+family of `𝒩(0, v c)`: `KL(ν_c(μ), ν_c(μ')) = d_c(μ c, μ' c)` with
+`d_c = (gaussianReal 0 (v c)).expFamilyDiv id`, the divergence on the means of
+`isDivergenceOn_expFamilyDiv`. The Gaussian bandits with arm-dependent known variances
+`fun μ ↦ Bandits.gaussianMeanVarBandit fun a ↦ (μ a, v a)` are such arms. -/
+lemma klDiv_eq_ofReal_expFamilyDiv_gaussianReal {α : Type*} {mα : MeasurableSpace α}
+    {ν : (α → ℝ) → Kernel α ℝ} {v : α → ℝ≥0} (hv : ∀ c, v c ≠ 0)
+    (hν : ∀ μ c, ν μ c = gaussianReal (μ c) (v c)) (μ μ' : α → ℝ) (c : α) :
+    klDiv (ν μ c) (ν μ' c) =
+      ENNReal.ofReal ((gaussianReal 0 (v c)).expFamilyDiv id (μ c) (μ' c)) := by
+  rw [hν, hν, klDiv_gaussianReal_gaussianReal_same_var (hv c), expFamilyDiv_gaussianReal 0 (hv c)]
+
 namespace IdentTask
 
 variable {α 𝓨 ℐ : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨} [Fintype α]
diff --git a/LMLExplore/Identification/Task/Threshold/Basic.lean b/LMLExplore/Identification/Task/Threshold/Basic.lean
index b10b645..193bed9 100644
--- a/LMLExplore/Identification/Task/Threshold/Basic.lean
+++ b/LMLExplore/Identification/Task/Threshold/Basic.lean
@@ -25,8 +25,8 @@ parametrization on their sets of means, are an instance (`isDivergenceOn_expFami
   with mean above `γ` are the vectors in which some arm `a` crossed `γ`. The infimum of their costs
   is approached by moving a single arm to the other side of `γ`, ever closer to `γ`, so that
   `D(μ, w, ¬S*) = min_a w a d_a(μ a, γ)`. The allocation maximizing it is proportional to
-  `d_a(μ a, γ)⁻¹`, and `T*(μ) = ∑ a, d_a(μ a, γ)⁻¹`. For Gaussian arms with variance `σ2`,
-  `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`.
+  `d_a(μ a, γ)⁻¹`, and `T*(μ) = ∑ a, d_a(μ a, γ)⁻¹`. For Gaussian arms with known variances
+  `v a`, `T*(μ) = ∑ a, 2 v a / (μ a - γ)²`.
 * *Minimum threshold* (`minThresholdTask ν id γ`): if all the means are above `γ` (answer `false`),
   the alternatives are the vectors with some mean below `γ`, and the game is that of thresholding:
   `D(μ, w, ¬false) = min_a w a d_a(μ a, γ)` and `T*(μ) = ∑ a, d_a(μ a, γ)⁻¹`
@@ -35,8 +35,13 @@ parametrization on their sets of means, are an instance (`isDivergenceOn_expFami
   `γ`, and the infimum of the costs is reached in the limit where these arms are moved to `γ`:
   `D(μ, w, ¬true) = ∑ a, w a d_a(μ a, max (μ a) γ)`, whose supremum over the simplex is
   `D(μ, ¬true) = max_a d_a(μ a, max (μ a) γ)`, and `T*(μ) = (max_a d_a(μ a, max (μ a) γ))⁻¹`. For
-  Gaussian arms with a common variance `σ2`, this is `2 σ2 / (μ a₀ - γ)²` for an arm `a₀` of
-  smallest mean [DK19, Lemma 38; KKG18, Lemma 1].
+  Gaussian arms with known variances `v a`, this is `2 v a₀ / (μ a₀ - γ)²` for an arm `a₀` below
+  `γ` maximizing `(μ a - γ)² / v a` among the arms below `γ`; with a common variance, `a₀` is an
+  arm of smallest mean [DK19, Lemma 38; KKG18, Lemma 1].
+
+The Gaussian arms with known variances `v a ≠ 0` are the arm laws `ν μ a = 𝒩(μ a, v a)`, for
+instance the bandits `Bandits.gaussianMeanVarBandit fun a ↦ (μ a, v a)`; the Gaussian bandits
+`Bandits.gaussianBandit μ σ2` with a common variance are the case of a constant `v`.
 
 The admissible models are the vectors of means in `S`, `task.restrict {λ | ∀ c, λ c ∈ S c}`. Each
 arm has its own divergence: the arms do not interact in these tasks. The transportation costs
@@ -58,9 +63,13 @@ which also uses only the hypotheses `IsDivergenceOn`, and the game of a weighted
   `D(μ, w, ¬S*) = min_a w a d_a(μ a, γ)`, `D(μ, ¬S*) = (∑ a, d_a(μ a, γ)⁻¹)⁻¹`,
   `T*(μ) = ∑ a, d_a(μ a, γ)⁻¹`, and the only optimal allocation is proportional to
   `d_a(μ a, γ)⁻¹`.
+* `LMLExplore.Identification.altCost_thresholdingTask_gaussianReal`,
+  `LMLExplore.Identification.charTime_thresholdingTask_gaussianReal`: for Gaussian arms with
+  variances `v a`, `D(μ, w, ¬S*) = min_a w a (μ a - γ)² / (2 v a)` and
+  `T*(μ) = ∑ a, 2 v a / (μ a - γ)²`.
 * `LMLExplore.Identification.altCost_thresholdingTask_gaussianBandit`,
-  `LMLExplore.Identification.charTime_thresholdingTask_gaussianBandit`: for Gaussian arms,
-  `D(μ, w, ¬S*) = min_a w a (μ a - γ)² / (2 σ2)` and `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`.
+  `LMLExplore.Identification.charTime_thresholdingTask_gaussianBandit`: their cases of a common
+  variance `σ2`.
 * `LMLExplore.Identification.altCost_minThresholdTask_restrict_false`,
   `LMLExplore.Identification.answerValue_minThresholdTask_restrict_false`,
   `LMLExplore.Identification.charTime_minThresholdTask_restrict_false`,
@@ -71,10 +80,14 @@ which also uses only the hypotheses `IsDivergenceOn`, and the game of a weighted
   `LMLExplore.Identification.charTime_minThresholdTask_restrict_true`: for minimum threshold,
   `D(μ, w, ¬true) = ∑ a, w a d_a(μ a, max (μ a) γ)`, `D(μ, ¬true) = max_a d_a(μ a, max (μ a) γ)`
   and, when some mean is below `γ`, `T*(μ) = (max_a d_a(μ a, max (μ a) γ))⁻¹` [DK19, Lemma 38].
+* `LMLExplore.Identification.charTime_minThresholdTask_gaussianReal_false`,
+  `LMLExplore.Identification.charTime_minThresholdTask_gaussianReal_true`: for Gaussian arms with
+  variances `v a`, `T*(μ) = ∑ a, 2 v a / (μ a - γ)²` if all the means are above `γ`, and
+  `T*(μ) = 2 v a₀ / (μ a₀ - γ)²` if the arm `a₀` below `γ` maximizes `(μ a - γ)² / v a` among the
+  arms below `γ`.
 * `LMLExplore.Identification.charTime_minThresholdTask_gaussianBandit_false`,
-  `LMLExplore.Identification.charTime_minThresholdTask_gaussianBandit_true`: for Gaussian arms,
-  `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²` if all the means are above `γ`, and
-  `T*(μ) = 2 σ2 / (μ a₀ - γ)²` if the smallest mean `μ a₀` is below `γ`.
+  `LMLExplore.Identification.charTime_minThresholdTask_gaussianBandit_true`: their cases of a
+  common variance `σ2`, where `a₀` is an arm of smallest mean.
 
 ## References
 
@@ -210,44 +223,6 @@ theorem charTime_thresholdingTask_restrict [Nonempty α]
     answerValue_thresholdingTask_restrict ν hd hγ hμ hν hμγ hs, ENNReal.ofReal_inv_of_pos hpos,
     inv_inv]
 
-/-! #### Gaussian arms -/
-
-variable [MeasurableSingletonClass α] {σ2 : ℝ≥0}
-
-/-- **The cost of the alternatives in Gaussian thresholding.** For Gaussian arms with a common
-variance `σ2 ≠ 0`, a vector of means `μ` with no mean equal to `γ`, whose correct answer is the set
-`s` of the arms with mean above `γ`, and a nonnegative allocation `w`,
-`D(μ, w, ¬s) = min_a w a (μ a - γ)² / (2 σ2)`. -/
-theorem altCost_thresholdingTask_gaussianBandit (hσ2 : σ2 ≠ 0) (hμγ : ∀ a, μ a ≠ γ)
-    {s : Finset α} (hs : ∀ a, a ∈ s ↔ γ < μ a) (hw : 0 ≤ w) :
-    (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).altCost μ w s =
-      ⨅ a, ENNReal.ofReal (w a * (μ a - γ) ^ 2 / (2 * σ2)) := by
-  rw [← (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
-    altCost_thresholdingTask_restrict (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
-      (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ')
-      hμγ hs hw]
-  simp only [expFamilyDiv_gaussianReal 0 hσ2, mul_div_assoc]
-
-/-- **The characteristic time of Gaussian thresholding.** For Gaussian arms with a common variance
-`σ2 ≠ 0` and a vector of means `μ` with no mean equal to `γ`, `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`. -/
-theorem charTime_thresholdingTask_gaussianBandit [Nonempty α] (hσ2 : σ2 ≠ 0)
-    (hμγ : ∀ a, μ a ≠ γ) :
-    (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
-      ENNReal.ofReal (∑ a, 2 * σ2 / (μ a - γ) ^ 2) := by
-  rw [← (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
-    charTime_thresholdingTask_restrict (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
-      (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ')
-      hμγ]
-  simp only [expFamilyDiv_gaussianReal 0 hσ2, inv_div]
-
 end Thresholding
 
 /-! ### Minimum threshold -/
@@ -445,60 +420,140 @@ theorem charTime_minThresholdTask_restrict_true (hd : ∀ a, IsDivergenceOn (d a
   rw [IdentTask.charTime_eq_inv_answerValue _ h_corr,
     answerValue_minThresholdTask_restrict_true ν hd hγ hμ hν]
 
-/-! #### Gaussian arms -/
+end MinThreshold
 
-variable [MeasurableSingletonClass α] {σ2 : ℝ≥0}
+/-! ### Gaussian arms -/
+
+section Gaussian
+
+variable {ν : (α → ℝ) → Kernel α ℝ} [∀ μ, IsMarkovKernel (ν μ)] {v : α → ℝ≥0}
+
+/-- **The cost of the alternatives in Gaussian thresholding.** For Gaussian arms with variances
+`v a ≠ 0`, a vector of means `μ` with no mean equal to `γ`, whose correct answer is the set `s` of
+the arms with mean above `γ`, and a nonnegative allocation `w`,
+`D(μ, w, ¬s) = min_a w a (μ a - γ)² / (2 v a)`. -/
+theorem altCost_thresholdingTask_gaussianReal (hv : ∀ a, v a ≠ 0)
+    (hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a)) (hμγ : ∀ a, μ a ≠ γ) {s : Finset α}
+    (hs : ∀ a, a ∈ s ↔ γ < μ a) (hw : 0 ≤ w) :
+    (thresholdingTask ν id γ).altCost μ w s =
+      ⨅ a, ENNReal.ofReal (w a * (μ a - γ) ^ 2 / (2 * v a)) := by
+  rw [← (thresholdingTask ν id γ).restrict_univ,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hv,
+    altCost_thresholdingTask_restrict (S := fun a ↦ (gaussianReal 0 (v a)).expFamilyMeans id) _
+      (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ hs hw]
+  exact iInf_congr fun a ↦ by rw [expFamilyDiv_gaussianReal 0 (hv a), mul_div_assoc]
+
+/-- **The characteristic time of Gaussian thresholding.** For Gaussian arms with variances
+`v a ≠ 0` and a vector of means `μ` with no mean equal to `γ`, `T*(μ) = ∑ a, 2 v a / (μ a - γ)²`. -/
+theorem charTime_thresholdingTask_gaussianReal [Nonempty α] (hv : ∀ a, v a ≠ 0)
+    (hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a)) (hμγ : ∀ a, μ a ≠ γ) :
+    (thresholdingTask ν id γ).charTime μ = ENNReal.ofReal (∑ a, 2 * v a / (μ a - γ) ^ 2) := by
+  rw [← (thresholdingTask ν id γ).restrict_univ,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hv,
+    charTime_thresholdingTask_restrict (S := fun a ↦ (gaussianReal 0 (v a)).expFamilyMeans id) _
+      (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
+  exact congrArg ENNReal.ofReal (Finset.sum_congr rfl fun a _ ↦ by
+    rw [expFamilyDiv_gaussianReal 0 (hv a), inv_div])
 
 /-- **The characteristic time of Gaussian minimum threshold when all the means are above the
-threshold** [DK19, Lemma 37]. For Gaussian arms with a common variance `σ2 ≠ 0` and a vector of
-means `μ` with all its means above `γ`, `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`. -/
-theorem charTime_minThresholdTask_gaussianBandit_false [Nonempty α] (hσ2 : σ2 ≠ 0)
-    (hμγ : ∀ a, γ < μ a) :
-    (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
-      ENNReal.ofReal (∑ a, 2 * σ2 / (μ a - γ) ^ 2) := by
-  rw [← (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
-    charTime_minThresholdTask_restrict_false (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
-      (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ')
-      hμγ]
-  simp only [expFamilyDiv_gaussianReal 0 hσ2, inv_div]
+threshold** [DK19, Lemma 37]. For Gaussian arms with variances `v a ≠ 0` and a vector of means `μ`
+with all its means above `γ`, `T*(μ) = ∑ a, 2 v a / (μ a - γ)²`. -/
+theorem charTime_minThresholdTask_gaussianReal_false [Nonempty α] (hv : ∀ a, v a ≠ 0)
+    (hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a)) (hμγ : ∀ a, γ < μ a) :
+    (minThresholdTask ν id γ).charTime μ = ENNReal.ofReal (∑ a, 2 * v a / (μ a - γ) ^ 2) := by
+  rw [← (minThresholdTask ν id γ).restrict_univ,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hv,
+    charTime_minThresholdTask_restrict_false
+      (S := fun a ↦ (gaussianReal 0 (v a)).expFamilyMeans id) _
+      (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
+  exact congrArg ENNReal.ofReal (Finset.sum_congr rfl fun a _ ↦ by
+    rw [expFamilyDiv_gaussianReal 0 (hv a), inv_div])
 
 /-- **The characteristic time of Gaussian minimum threshold when some mean is below the
-threshold** [DK19, Lemma 38]. For Gaussian arms with a common variance `σ2 ≠ 0` and a vector of
-means `μ` whose smallest mean `μ a₀` is below `γ`, `T*(μ) = 2 σ2 / (μ a₀ - γ)²`. -/
-theorem charTime_minThresholdTask_gaussianBandit_true (hσ2 : σ2 ≠ 0) {a₀ : α}
-    (ha₀ : ∀ a, μ a₀ ≤ μ a) (hγ : μ a₀ < γ) :
-    (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
-      ENNReal.ofReal (2 * σ2 / (μ a₀ - γ) ^ 2) := by
-  have hσ2' : 0 < (σ2 : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 hσ2)
-  rw [← (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
-    charTime_minThresholdTask_restrict_true (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
-      (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (fun μ' _ ↦ Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv hσ2 μ μ')
-      ⟨a₀, hγ⟩]
-  simp only [expFamilyDiv_gaussianReal 0 hσ2]
-  -- The largest divergence to the alternatives is that of the arm with the smallest mean.
-  have h_sup : ⨆ a, ENNReal.ofReal ((μ a - max (μ a) γ) ^ 2 / (2 * σ2)) =
-      ENNReal.ofReal ((μ a₀ - γ) ^ 2 / (2 * σ2)) := by
+threshold** [DK19, Lemma 38]. For Gaussian arms with variances `v a ≠ 0` and a vector of means `μ`
+with an arm `a₀` below `γ` that maximizes `(μ a - γ)² / v a` among the arms below `γ`,
+`T*(μ) = 2 v a₀ / (μ a₀ - γ)²`. -/
+theorem charTime_minThresholdTask_gaussianReal_true (hv : ∀ a, v a ≠ 0)
+    (hν : ∀ μ a, ν μ a = gaussianReal (μ a) (v a)) {a₀ : α} (hγ : μ a₀ < γ)
+    (ha₀ : ∀ a, μ a < γ → (μ a - γ) ^ 2 / v a ≤ (μ a₀ - γ) ^ 2 / v a₀) :
+    (minThresholdTask ν id γ).charTime μ = ENNReal.ofReal (2 * v a₀ / (μ a₀ - γ) ^ 2) := by
+  rw [← (minThresholdTask ν id γ).restrict_univ,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hv,
+    charTime_minThresholdTask_restrict_true
+      (S := fun a ↦ (gaussianReal 0 (v a)).expFamilyMeans id) _
+      (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
+      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') ⟨a₀, hγ⟩]
+  -- The largest divergence to the alternatives is that of the arm `a₀`.
+  have h_sup : ⨆ a, ENNReal.ofReal ((gaussianReal 0 (v a)).expFamilyDiv id (μ a)
+      (max (μ a) γ)) = ENNReal.ofReal ((μ a₀ - γ) ^ 2 / (2 * v a₀)) := by
     refine le_antisymm (iSup_le fun a ↦ ENNReal.ofReal_le_ofReal ?_)
-      (le_iSup_of_le a₀ (by rw [max_eq_right hγ.le]))
-    refine div_le_div_of_nonneg_right ?_ (by positivity)
-    rcases le_total (μ a) γ with h | h
-    · rw [max_eq_right h]
-      nlinarith [ha₀ a]
-    · rw [max_eq_left h, sub_self]
-      simpa using sq_nonneg (μ a₀ - γ)
-  have hpos : 0 < (μ a₀ - γ) ^ 2 / (2 * σ2) := by
+      (le_iSup_of_le a₀ (by rw [max_eq_right hγ.le, expFamilyDiv_gaussianReal 0 (hv a₀)]))
+    rw [expFamilyDiv_gaussianReal 0 (hv a)]
+    rcases lt_or_ge (μ a) γ with h | h
+    · rw [max_eq_right h.le, div_mul_eq_div_div_swap, div_mul_eq_div_div_swap]
+      exact div_le_div_of_nonneg_right (ha₀ a h) zero_le_two
+    · rw [max_eq_left h, sub_self, zero_pow two_ne_zero, zero_div]
+      positivity
+  have hpos : 0 < (μ a₀ - γ) ^ 2 / (2 * v a₀) := by
     have : 0 < (μ a₀ - γ) ^ 2 := by nlinarith [mul_pos (sub_pos.2 hγ) (sub_pos.2 hγ)]
+    have : 0 < (v a₀ : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 (hv a₀))
     positivity
   rw [h_sup, ← ENNReal.ofReal_inv_of_pos hpos, inv_div]
 
-end MinThreshold
+/-- **The cost of the alternatives in Gaussian thresholding with a common variance.** For Gaussian
+arms with a common variance `σ2 ≠ 0`, a vector of means `μ` with no mean equal to `γ`, whose
+correct answer is the set `s` of the arms with mean above `γ`, and a nonnegative allocation `w`,
+`D(μ, w, ¬s) = min_a w a (μ a - γ)² / (2 σ2)`. -/
+theorem altCost_thresholdingTask_gaussianBandit [MeasurableSingletonClass α] {σ2 : ℝ≥0}
+    (hσ2 : σ2 ≠ 0) (hμγ : ∀ a, μ a ≠ γ) {s : Finset α} (hs : ∀ a, a ∈ s ↔ γ < μ a) (hw : 0 ≤ w) :
+    (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).altCost μ w s =
+      ⨅ a, ENNReal.ofReal (w a * (μ a - γ) ^ 2 / (2 * σ2)) :=
+  altCost_thresholdingTask_gaussianReal (v := fun _ ↦ σ2) (fun _ ↦ hσ2)
+    (Bandits.gaussianBandit_apply · σ2) hμγ hs hw
+
+/-- **The characteristic time of Gaussian thresholding with a common variance.** For Gaussian arms
+with a common variance `σ2 ≠ 0` and a vector of means `μ` with no mean equal to `γ`,
+`T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`. -/
+theorem charTime_thresholdingTask_gaussianBandit [MeasurableSingletonClass α] [Nonempty α]
+    {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) (hμγ : ∀ a, μ a ≠ γ) :
+    (thresholdingTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
+      ENNReal.ofReal (∑ a, 2 * σ2 / (μ a - γ) ^ 2) :=
+  charTime_thresholdingTask_gaussianReal (v := fun _ ↦ σ2) (fun _ ↦ hσ2)
+    (Bandits.gaussianBandit_apply · σ2) hμγ
+
+/-- **The characteristic time of Gaussian minimum threshold with a common variance when all the
+means are above the threshold** [DK19, Lemma 37]. For Gaussian arms with a common variance
+`σ2 ≠ 0` and a vector of means `μ` with all its means above `γ`, `T*(μ) = ∑ a, 2 σ2 / (μ a - γ)²`.
+-/
+theorem charTime_minThresholdTask_gaussianBandit_false [MeasurableSingletonClass α] [Nonempty α]
+    {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) (hμγ : ∀ a, γ < μ a) :
+    (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
+      ENNReal.ofReal (∑ a, 2 * σ2 / (μ a - γ) ^ 2) :=
+  charTime_minThresholdTask_gaussianReal_false (v := fun _ ↦ σ2) (fun _ ↦ hσ2)
+    (Bandits.gaussianBandit_apply · σ2) hμγ
+
+/-- **The characteristic time of Gaussian minimum threshold with a common variance when some mean
+is below the threshold** [DK19, Lemma 38]. For Gaussian arms with a common variance `σ2 ≠ 0` and a
+vector of means `μ` whose smallest mean `μ a₀` is below `γ`, `T*(μ) = 2 σ2 / (μ a₀ - γ)²`. -/
+theorem charTime_minThresholdTask_gaussianBandit_true [MeasurableSingletonClass α] {σ2 : ℝ≥0}
+    (hσ2 : σ2 ≠ 0) {a₀ : α} (ha₀ : ∀ a, μ a₀ ≤ μ a) (hγ : μ a₀ < γ) :
+    (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).charTime μ =
+      ENNReal.ofReal (2 * σ2 / (μ a₀ - γ) ^ 2) :=
+  charTime_minThresholdTask_gaussianReal_true (v := fun _ ↦ σ2) (fun _ ↦ hσ2)
+    (Bandits.gaussianBandit_apply · σ2) hγ fun a ha ↦
+      div_le_div_of_nonneg_right (by nlinarith [ha₀ a]) σ2.2
+
+end Gaussian
 
 end LMLExplore.Identification
diff --git a/LMLExplore/Identification/Task/Threshold/StaticProportions.lean b/LMLExplore/Identification/Task/Threshold/StaticProportions.lean
index 04f8c5d..6d162a5 100644
--- a/LMLExplore/Identification/Task/Threshold/StaticProportions.lean
+++ b/LMLExplore/Identification/Task/Threshold/StaticProportions.lean
@@ -235,7 +235,7 @@ theorem staticDifficulty_minThresholdTask_gaussianBandit_false [Nonempty α] (h
     (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).staticDifficulty μ =
       ENNReal.ofReal (∑ a, 2 * σ2 / (μ a - γ) ^ 2) := by
   rw [← (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 (fun _ ↦ hσ2),
     staticDifficulty_minThresholdTask_restrict_false
       (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
       (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
@@ -255,7 +255,7 @@ theorem staticDifficulty_minThresholdTask_gaussianBandit_true (hσ2 : σ2 ≠ 0)
       ENNReal.ofReal (2 * σ2 / (μ a₀ - γ) ^ 2) := by
   rw [← charTime_minThresholdTask_gaussianBandit_true hσ2 ha₀ hγ,
     ← (minThresholdTask (Bandits.gaussianBandit · σ2) id γ).restrict_univ,
-    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 hσ2,
+    ← setOf_forall_mem_expFamilyMeans_gaussianReal 0 (fun _ ↦ hσ2),
     staticDifficulty_minThresholdTask_restrict_true
       (S := fun _ ↦ (gaussianReal 0 σ2).expFamilyMeans id) _
       (fun _ ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 hσ2))
diff --git a/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean b/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean
index 5d7ed45..7d285fb 100644
--- a/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean
+++ b/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean
@@ -70,7 +70,7 @@ Fixed variance, statistic `id`:
   constant under `𝒩(m, v)`, the nondegeneracy assumption of the mean parametrization.
 * `LMLExplore.expFamilyMeans_gaussianReal`, `LMLExplore.mem_expFamilyMeans_gaussianReal`,
   `LMLExplore.setOf_forall_mem_expFamilyMeans_gaussianReal`: for `v ≠ 0`, the means of the family
-  are all of `ℝ`, and every vector is a vector of means of the family.
+  are all of `ℝ`, and every vector is a vector of means of the families of variances `v i ≠ 0`.
 * `LMLExplore.natParam_gaussianReal`: for `v ≠ 0`, the natural parameter of the mean `μ` is
   `(μ - m) / v`.
 * `LMLExplore.expFamily_natParam_gaussianReal`: for `v ≠ 0`, the member of mean `μ` is `𝒩(μ, v)`.
@@ -172,9 +172,11 @@ lemma mem_expFamilyMeans_gaussianReal (m : ℝ) (hv : v ≠ 0) (μ : ℝ) :
     μ ∈ (gaussianReal m v).expFamilyMeans id := by
   simp [hv]
 
-/-- For `v ≠ 0`, every vector is a vector of means of the exponential family of `𝒩(m, v)`. -/
-lemma setOf_forall_mem_expFamilyMeans_gaussianReal {ι : Type*} (m : ℝ) (hv : v ≠ 0) :
-    {μ : ι → ℝ | ∀ i, μ i ∈ (gaussianReal m v).expFamilyMeans id} = univ := by
+/-- For variances `v i ≠ 0`, every vector is a vector of means of the exponential families of
+the `𝒩(m, v i)`: `μ i` is a mean of the family of `𝒩(m, v i)` for every `i`. -/
+lemma setOf_forall_mem_expFamilyMeans_gaussianReal {ι : Type*} (m : ℝ) {v : ι → ℝ≥0}
+    (hv : ∀ i, v i ≠ 0) :
+    {μ : ι → ℝ | ∀ i, μ i ∈ (gaussianReal m (v i)).expFamilyMeans id} = univ := by
   simp [hv]
 
 /-- For `v ≠ 0`, the natural parameter of the member of mean `μ` of the exponential family of

From a65e35ea096d5ea653277ef1f967f4eb0a51e53c Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 12 Nov 2026 09:56:48 +0100
Subject: [PATCH 2/3] =?UTF-8?q?refactor:=20move=20the=20arm-dependent=20Ga?=
 =?UTF-8?q?ussian=20KL=20bridge=20to=20Bandits/Instances=20and=20share=20t?=
 =?UTF-8?q?he=20divergence=20to=20max=20x=20=CE=B3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Move klDiv_eq_ofReal_expFamilyDiv_gaussianReal from
Identification/Task/ExpFamily.lean (namespace LMLExplore.Identification) to
Bandits/Instances.lean (namespace LMLExplore.Bandits), next to its
common-variance counterpart. Add expFamilyDiv_gaussianReal_max_of_lt,
expFamilyDiv_gaussianReal_max_of_le and expFamilyDiv_gaussianReal_max_pos in
Threshold/Basic.lean, used by the minimum-threshold and Any Low Arm proofs.

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/Bandits/Instances.lean             | 19 ++++++--
 LMLExplore/Identification/Task/AnyLowArm.lean | 29 ++++-------
 LMLExplore/Identification/Task/ExpFamily.lean | 14 ------
 .../Identification/Task/Threshold/Basic.lean  | 48 +++++++++++++------
 4 files changed, 58 insertions(+), 52 deletions(-)

diff --git a/LMLExplore/Bandits/Instances.lean b/LMLExplore/Bandits/Instances.lean
index 54dde50..563a682 100644
--- a/LMLExplore/Bandits/Instances.lean
+++ b/LMLExplore/Bandits/Instances.lean
@@ -32,9 +32,10 @@ arms of `gaussianBandit μ σ2` are `σ2`-sub-Gaussian, and Bernoulli arms are i
 the Bernoulli reward tables `x ∼ streamMeasure (bernoulliBandit p)`. We also compute the relative
 entropy between the arms of two Gaussian bandits with the same variance [LS, Theorem 14.1], the
 quantity that enters the lower bounds, and identify it with the divergence of the exponential family
-of `𝒩(0, σ2)` (`LMLExplore.Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv`), and the relative
-entropy between the arms of two Bernoulli bandits with means in `(0, 1)` with the divergence of the
-exponential family of a Bernoulli law
+of `𝒩(0, σ2)` (`LMLExplore.Bandits.klDiv_gaussianBandit_eq_ofReal_expFamilyDiv`, and
+`LMLExplore.Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal` for Gaussian arms `𝒩(μ c, v c)` with
+arm-dependent variances), and the relative entropy between the arms of two Bernoulli bandits with
+means in `(0, 1)` with the divergence of the exponential family of a Bernoulli law
 (`LMLExplore.Bandits.klDiv_bernoulliBandit_eq_ofReal_expFamilyDiv`, and
 `LMLExplore.Bandits.klDiv_bernoulliBandit_projIcc_eq_ofReal_expFamilyDiv` for bandits indexed by
 real means). For the Gaussian bandit with unknown variances we compute the mean and the variance of
@@ -101,6 +102,18 @@ lemma klDiv_gaussianBandit_eq_ofReal_expFamilyDiv (hσ2 : σ2 ≠ 0) (μ μ' : 
       ENNReal.ofReal ((gaussianReal 0 σ2).expFamilyDiv id (μ a) (μ' a)) := by
   rw [klDiv_gaussianBandit _ _ hσ2, expFamilyDiv_gaussianReal 0 hσ2]
 
+/-- For Gaussian arms with variances `v c ≠ 0`, the arm `c` has the divergence of the exponential
+family of `𝒩(0, v c)`: `KL(ν_c(μ), ν_c(μ')) = d_c(μ c, μ' c)` with
+`d_c = (gaussianReal 0 (v c)).expFamilyDiv id`. The Gaussian bandits with arm-dependent known
+variances `fun μ ↦ gaussianMeanVarBandit fun a ↦ (μ a, v a)` are such arms; this generalizes
+`klDiv_gaussianBandit_eq_ofReal_expFamilyDiv`. -/
+lemma klDiv_eq_ofReal_expFamilyDiv_gaussianReal {α : Type*} {mα : MeasurableSpace α}
+    {ν : (α → ℝ) → Kernel α ℝ} {v : α → ℝ≥0} (hv : ∀ c, v c ≠ 0)
+    (hν : ∀ μ c, ν μ c = gaussianReal (μ c) (v c)) (μ μ' : α → ℝ) (c : α) :
+    klDiv (ν μ c) (ν μ' c) =
+      ENNReal.ofReal ((gaussianReal 0 (v c)).expFamilyDiv id (μ c) (μ' c)) := by
+  rw [hν, hν, klDiv_gaussianReal_gaussianReal_same_var (hv c), expFamilyDiv_gaussianReal 0 (hv c)]
+
 end Gaussian
 
 section GaussianMeanVar
diff --git a/LMLExplore/Identification/Task/AnyLowArm.lean b/LMLExplore/Identification/Task/AnyLowArm.lean
index f8f8da0..3ef6fdb 100644
--- a/LMLExplore/Identification/Task/AnyLowArm.lean
+++ b/LMLExplore/Identification/Task/AnyLowArm.lean
@@ -459,20 +459,8 @@ theorem oracleAlloc_anyLowArmTask_gaussianReal [DecidableEq α] (hv : ∀ a, v a
       (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
-      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') h]
-  simp only [expFamilyDiv_gaussianReal 0 (hv _)]
+      (fun μ' _ ↦ Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') h]
   congr 1
-  -- The divergence `(μ a - max (μ a) γ)² / (2 v a)` of an arm is `(μ a - γ)² / (2 v a) > 0` if
-  -- the arm is below `γ`, and `0` otherwise.
-  have h_lt (a : α) (ha : μ a < γ) :
-      (μ a - max (μ a) γ) ^ 2 / (2 * v a) = (μ a - γ) ^ 2 / v a / 2 := by
-    rw [max_eq_right ha.le, div_mul_eq_div_div_swap]
-  have h_ge (a : α) (ha : γ ≤ μ a) : (μ a - max (μ a) γ) ^ 2 / (2 * v a) = 0 := by
-    rw [max_eq_left ha, sub_self, zero_pow two_ne_zero, zero_div]
-  have h_pos (a : α) (ha : μ a < γ) : 0 < (μ a - γ) ^ 2 / v a := by
-    have : 0 < (v a : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 (hv a))
-    have : 0 < (μ a - γ) ^ 2 := by nlinarith [mul_pos (sub_pos.2 ha) (sub_pos.2 ha)]
-    positivity
   obtain ⟨b₀, hb₀⟩ := h
   ext a
   simp only [Set.mem_ofPred_eq]
@@ -482,19 +470,20 @@ theorem oracleAlloc_anyLowArmTask_gaussianReal [DecidableEq α] (hv : ∀ a, v a
     have hlt : μ a < γ := by
       by_contra hge
       have h_le := ha b₀
-      rw [h_lt b₀ hb₀, h_ge a (not_lt.1 hge)] at h_le
-      linarith [h_pos b₀ hb₀]
+      rw [expFamilyDiv_gaussianReal_max_of_le _ (not_lt.1 hge)] at h_le
+      linarith [expFamilyDiv_gaussianReal_max_pos (hv b₀) hb₀]
     refine ⟨hlt, fun b hb ↦ ?_⟩
     have h_le := ha b
-    rw [h_lt b hb, h_lt a hlt] at h_le
+    rw [expFamilyDiv_gaussianReal_max_of_lt (hv b) hb,
+      expFamilyDiv_gaussianReal_max_of_lt (hv a) hlt] at h_le
     linarith
   · rintro ⟨hlt, ha⟩ b
-    rw [h_lt a hlt]
+    rw [expFamilyDiv_gaussianReal_max_of_lt (hv a) hlt]
     rcases lt_or_ge (μ b) γ with hb | hb
-    · rw [h_lt b hb]
+    · rw [expFamilyDiv_gaussianReal_max_of_lt (hv b) hb]
       linarith [ha b hb]
-    · rw [h_ge b hb]
-      linarith [h_pos a hlt]
+    · rw [expFamilyDiv_gaussianReal_max_of_le _ hb]
+      positivity
 
 /-- **The oracle allocations of Gaussian Any Low Arm with a common variance** [DK19, Example 1].
 For Gaussian arms with a common variance `σ2 ≠ 0` and a vector of means `μ` whose smallest mean
diff --git a/LMLExplore/Identification/Task/ExpFamily.lean b/LMLExplore/Identification/Task/ExpFamily.lean
index a71a8a5..aa7bd69 100644
--- a/LMLExplore/Identification/Task/ExpFamily.lean
+++ b/LMLExplore/Identification/Task/ExpFamily.lean
@@ -36,8 +36,6 @@ parametrization have them (`isDivergenceOn_expFamilyDiv`).
 
 * `LMLExplore.Identification.isDivergenceOn_expFamilyDiv`: the divergence `d(μ, μ')` of an
   exponential family in the mean parametrization is a divergence on its means.
-* `LMLExplore.Identification.klDiv_eq_ofReal_expFamilyDiv_gaussianReal`: Gaussian arms with
-  variances `v c ≠ 0` have the divergences of the exponential families of the `𝒩(0, v c)`.
 * `LMLExplore.Identification.IdentTask.cost_eq_sum_ofReal_mul`: on the vectors of means in `S`,
   `cost_μ(w, μ') = ∑ c, w c d_c(μ c, μ' c)`.
 * `LMLExplore.Identification.IdentTask.cost_eq_sum_ofReal_mul_left`: the cost with the free vector
@@ -174,18 +172,6 @@ theorem isDivergenceOn_expFamilyDiv {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧
   monotoneOn_left _ hy := (strictMonoOn_expFamilyDiv_left hT hy).monotoneOn
   antitoneOn_left _ hy := (strictAntiOn_expFamilyDiv_left hT hy).antitoneOn
 
-/-- For Gaussian arms with variances `v c ≠ 0`, the arm `c` has the divergence of the exponential
-family of `𝒩(0, v c)`: `KL(ν_c(μ), ν_c(μ')) = d_c(μ c, μ' c)` with
-`d_c = (gaussianReal 0 (v c)).expFamilyDiv id`, the divergence on the means of
-`isDivergenceOn_expFamilyDiv`. The Gaussian bandits with arm-dependent known variances
-`fun μ ↦ Bandits.gaussianMeanVarBandit fun a ↦ (μ a, v a)` are such arms. -/
-lemma klDiv_eq_ofReal_expFamilyDiv_gaussianReal {α : Type*} {mα : MeasurableSpace α}
-    {ν : (α → ℝ) → Kernel α ℝ} {v : α → ℝ≥0} (hv : ∀ c, v c ≠ 0)
-    (hν : ∀ μ c, ν μ c = gaussianReal (μ c) (v c)) (μ μ' : α → ℝ) (c : α) :
-    klDiv (ν μ c) (ν μ' c) =
-      ENNReal.ofReal ((gaussianReal 0 (v c)).expFamilyDiv id (μ c) (μ' c)) := by
-  rw [hν, hν, klDiv_gaussianReal_gaussianReal_same_var (hv c), expFamilyDiv_gaussianReal 0 (hv c)]
-
 namespace IdentTask
 
 variable {α 𝓨 ℐ : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨} [Fintype α]
diff --git a/LMLExplore/Identification/Task/Threshold/Basic.lean b/LMLExplore/Identification/Task/Threshold/Basic.lean
index 193bed9..8048265 100644
--- a/LMLExplore/Identification/Task/Threshold/Basic.lean
+++ b/LMLExplore/Identification/Task/Threshold/Basic.lean
@@ -428,6 +428,27 @@ section Gaussian
 
 variable {ν : (α → ℝ) → Kernel α ℝ} [∀ μ, IsMarkovKernel (ν μ)] {v : α → ℝ≥0}
 
+/-- For a mean `x < γ`, the divergence of the exponential family of `𝒩(0, σ2)` from `x` to
+`max x γ`, the mean to which minimum threshold and Any Low Arm move the arms below `γ`, is
+`(x - γ)² / σ2 / 2`. -/
+lemma expFamilyDiv_gaussianReal_max_of_lt {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {x : ℝ} (h : x < γ) :
+    (gaussianReal 0 σ2).expFamilyDiv id x (max x γ) = (x - γ) ^ 2 / σ2 / 2 := by
+  rw [expFamilyDiv_gaussianReal 0 hσ2, max_eq_right h.le, div_mul_eq_div_div_swap]
+
+/-- For a mean `x ≥ γ`, the divergence of the exponential family of `𝒩(0, σ2)` from `x` to
+`max x γ = x` is `0`. -/
+lemma expFamilyDiv_gaussianReal_max_of_le (σ2 : ℝ≥0) {x : ℝ} (h : γ ≤ x) :
+    (gaussianReal 0 σ2).expFamilyDiv id x (max x γ) = 0 := by
+  rw [max_eq_left h, Measure.expFamilyDiv_self]
+
+/-- For a mean `x < γ` and a variance `σ2 ≠ 0`, the divergence of the exponential family of
+`𝒩(0, σ2)` from `x` to `max x γ` is positive. -/
+lemma expFamilyDiv_gaussianReal_max_pos {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {x : ℝ} (h : x < γ) :
+    0 < (gaussianReal 0 σ2).expFamilyDiv id x (max x γ) := by
+  rw [expFamilyDiv_gaussianReal_max_of_lt hσ2 h]
+  exact div_pos (div_pos (sq_pos_of_neg (sub_neg.2 h)) (NNReal.coe_pos.2 (pos_iff_ne_zero.2 hσ2)))
+    two_pos
+
 /-- **The cost of the alternatives in Gaussian thresholding.** For Gaussian arms with variances
 `v a ≠ 0`, a vector of means `μ` with no mean equal to `γ`, whose correct answer is the set `s` of
 the arms with mean above `γ`, and a nonnegative allocation `w`,
@@ -443,7 +464,7 @@ theorem altCost_thresholdingTask_gaussianReal (hv : ∀ a, v a ≠ 0)
       (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
-      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ hs hw]
+      (fun μ' _ ↦ Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ hs hw]
   exact iInf_congr fun a ↦ by rw [expFamilyDiv_gaussianReal 0 (hv a), mul_div_assoc]
 
 /-- **The characteristic time of Gaussian thresholding.** For Gaussian arms with variances
@@ -457,7 +478,7 @@ theorem charTime_thresholdingTask_gaussianReal [Nonempty α] (hv : ∀ a, v a 
       (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
-      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
+      (fun μ' _ ↦ Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
   exact congrArg ENNReal.ofReal (Finset.sum_congr rfl fun a _ ↦ by
     rw [expFamilyDiv_gaussianReal 0 (hv a), inv_div])
 
@@ -474,7 +495,7 @@ theorem charTime_minThresholdTask_gaussianReal_false [Nonempty α] (hv : ∀ a,
       (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
-      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
+      (fun μ' _ ↦ Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') hμγ]
   exact congrArg ENNReal.ofReal (Finset.sum_congr rfl fun a _ ↦ by
     rw [expFamilyDiv_gaussianReal 0 (hv a), inv_div])
 
@@ -493,23 +514,20 @@ theorem charTime_minThresholdTask_gaussianReal_true (hv : ∀ a, v a ≠ 0)
       (fun a ↦ isDivergenceOn_expFamilyDiv (not_ae_eq_const_gaussianReal 0 (hv a)))
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
       (fun a ↦ mem_expFamilyMeans_gaussianReal 0 (hv a) _)
-      (fun μ' _ ↦ klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') ⟨a₀, hγ⟩]
+      (fun μ' _ ↦ Bandits.klDiv_eq_ofReal_expFamilyDiv_gaussianReal hv hν μ μ') ⟨a₀, hγ⟩]
   -- The largest divergence to the alternatives is that of the arm `a₀`.
   have h_sup : ⨆ a, ENNReal.ofReal ((gaussianReal 0 (v a)).expFamilyDiv id (μ a)
-      (max (μ a) γ)) = ENNReal.ofReal ((μ a₀ - γ) ^ 2 / (2 * v a₀)) := by
-    refine le_antisymm (iSup_le fun a ↦ ENNReal.ofReal_le_ofReal ?_)
-      (le_iSup_of_le a₀ (by rw [max_eq_right hγ.le, expFamilyDiv_gaussianReal 0 (hv a₀)]))
-    rw [expFamilyDiv_gaussianReal 0 (hv a)]
+      (max (μ a) γ)) = ENNReal.ofReal ((gaussianReal 0 (v a₀)).expFamilyDiv id (μ a₀)
+      (max (μ a₀) γ)) := by
+    refine le_antisymm (iSup_le fun a ↦ ENNReal.ofReal_le_ofReal ?_) (le_iSup_of_le a₀ le_rfl)
+    rw [expFamilyDiv_gaussianReal_max_of_lt (hv a₀) hγ]
     rcases lt_or_ge (μ a) γ with h | h
-    · rw [max_eq_right h.le, div_mul_eq_div_div_swap, div_mul_eq_div_div_swap]
+    · rw [expFamilyDiv_gaussianReal_max_of_lt (hv a) h]
       exact div_le_div_of_nonneg_right (ha₀ a h) zero_le_two
-    · rw [max_eq_left h, sub_self, zero_pow two_ne_zero, zero_div]
+    · rw [expFamilyDiv_gaussianReal_max_of_le _ h]
       positivity
-  have hpos : 0 < (μ a₀ - γ) ^ 2 / (2 * v a₀) := by
-    have : 0 < (μ a₀ - γ) ^ 2 := by nlinarith [mul_pos (sub_pos.2 hγ) (sub_pos.2 hγ)]
-    have : 0 < (v a₀ : ℝ) := NNReal.coe_pos.2 (pos_iff_ne_zero.2 (hv a₀))
-    positivity
-  rw [h_sup, ← ENNReal.ofReal_inv_of_pos hpos, inv_div]
+  rw [h_sup, ← ENNReal.ofReal_inv_of_pos (expFamilyDiv_gaussianReal_max_pos (hv a₀) hγ),
+    expFamilyDiv_gaussianReal_max_of_lt (hv a₀) hγ, inv_div, div_div_eq_mul_div]
 
 /-- **The cost of the alternatives in Gaussian thresholding with a common variance.** For Gaussian
 arms with a common variance `σ2 ≠ 0`, a vector of means `μ` with no mean equal to `γ`, whose

From 9d9ef4793623e5adcb095bae11b27c914da15c65 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 12 Nov 2026 10:17:15 +0100
Subject: [PATCH 3/3] =?UTF-8?q?refactor:=20inline=20the=20measure-agnostic?=
 =?UTF-8?q?=20max=20x=20=CE=B3=20divergence=20step?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

expFamilyDiv_gaussianReal_max_of_le never used Gaussianity: its proof is
max_eq_left followed by Measure.expFamilyDiv_self. Inline those two
rewrites at its three call sites and remove the helper.

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/Identification/Task/AnyLowArm.lean       | 4 ++--
 LMLExplore/Identification/Task/Threshold/Basic.lean | 8 +-------
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/LMLExplore/Identification/Task/AnyLowArm.lean b/LMLExplore/Identification/Task/AnyLowArm.lean
index 3ef6fdb..37a7d8b 100644
--- a/LMLExplore/Identification/Task/AnyLowArm.lean
+++ b/LMLExplore/Identification/Task/AnyLowArm.lean
@@ -470,7 +470,7 @@ theorem oracleAlloc_anyLowArmTask_gaussianReal [DecidableEq α] (hv : ∀ a, v a
     have hlt : μ a < γ := by
       by_contra hge
       have h_le := ha b₀
-      rw [expFamilyDiv_gaussianReal_max_of_le _ (not_lt.1 hge)] at h_le
+      rw [max_eq_left (not_lt.1 hge), Measure.expFamilyDiv_self] at h_le
       linarith [expFamilyDiv_gaussianReal_max_pos (hv b₀) hb₀]
     refine ⟨hlt, fun b hb ↦ ?_⟩
     have h_le := ha b
@@ -482,7 +482,7 @@ theorem oracleAlloc_anyLowArmTask_gaussianReal [DecidableEq α] (hv : ∀ a, v a
     rcases lt_or_ge (μ b) γ with hb | hb
     · rw [expFamilyDiv_gaussianReal_max_of_lt (hv b) hb]
       linarith [ha b hb]
-    · rw [expFamilyDiv_gaussianReal_max_of_le _ hb]
+    · rw [max_eq_left hb, Measure.expFamilyDiv_self]
       positivity
 
 /-- **The oracle allocations of Gaussian Any Low Arm with a common variance** [DK19, Example 1].
diff --git a/LMLExplore/Identification/Task/Threshold/Basic.lean b/LMLExplore/Identification/Task/Threshold/Basic.lean
index 8048265..5628708 100644
--- a/LMLExplore/Identification/Task/Threshold/Basic.lean
+++ b/LMLExplore/Identification/Task/Threshold/Basic.lean
@@ -435,12 +435,6 @@ lemma expFamilyDiv_gaussianReal_max_of_lt {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {x
     (gaussianReal 0 σ2).expFamilyDiv id x (max x γ) = (x - γ) ^ 2 / σ2 / 2 := by
   rw [expFamilyDiv_gaussianReal 0 hσ2, max_eq_right h.le, div_mul_eq_div_div_swap]
 
-/-- For a mean `x ≥ γ`, the divergence of the exponential family of `𝒩(0, σ2)` from `x` to
-`max x γ = x` is `0`. -/
-lemma expFamilyDiv_gaussianReal_max_of_le (σ2 : ℝ≥0) {x : ℝ} (h : γ ≤ x) :
-    (gaussianReal 0 σ2).expFamilyDiv id x (max x γ) = 0 := by
-  rw [max_eq_left h, Measure.expFamilyDiv_self]
-
 /-- For a mean `x < γ` and a variance `σ2 ≠ 0`, the divergence of the exponential family of
 `𝒩(0, σ2)` from `x` to `max x γ` is positive. -/
 lemma expFamilyDiv_gaussianReal_max_pos {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {x : ℝ} (h : x < γ) :
@@ -524,7 +518,7 @@ theorem charTime_minThresholdTask_gaussianReal_true (hv : ∀ a, v a ≠ 0)
     rcases lt_or_ge (μ a) γ with h | h
     · rw [expFamilyDiv_gaussianReal_max_of_lt (hv a) h]
       exact div_le_div_of_nonneg_right (ha₀ a h) zero_le_two
-    · rw [expFamilyDiv_gaussianReal_max_of_le _ h]
+    · rw [max_eq_left h, Measure.expFamilyDiv_self]
       positivity
   rw [h_sup, ← ENNReal.ofReal_inv_of_pos (expFamilyDiv_gaussianReal_max_pos (hv a₀) hγ),
     expFamilyDiv_gaussianReal_max_of_lt (hv a₀) hγ, inv_div, div_div_eq_mul_div]