feat: the transductive best-answer task and the closure of its alternatives

LMLExplore/Identification/Task/BestArm/Basic.lean

@@ -81,6 +81,8 @@ within a factor `2` of the complexity `H(μ) = ∑ c, 2 σ2 / Δ_c²`, where `Δ
 * `LMLExplore.Identification.mem_answerSet_baiTask_iff`,
   `LMLExplore.Identification.isOpen_answerSet_baiTask`: the vectors of means for which `a` is
   correct, those with unique best arm `a`, form an open set;
+  `LMLExplore.Identification.isOpen_answerSet_baiTask_of_continuous` is the same for finitely many
+  arms and any mean functional continuous in the model;
   `LMLExplore.Identification.isOpen_answerSet_baiTask_restrict` is the same within an open set `S`
   of vectors of means.
 * `LMLExplore.Identification.closure_alt_baiTask_restrict_inter`: for `S` open, the closure of the
@@ -183,11 +185,12 @@ open scoped ENNReal NNReal
 
 namespace LMLExplore.Identification
 
-variable {α Θ 𝓨 : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨} {a : α}
+variable {α Θ 𝓨 : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨}
 
 section MeanFunctional
 
-variable (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → α → ℝ) {θ : Θ}
+variable {ι : Type*} (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → ι → ℝ)
+  {θ : Θ} {a : ι}
 
 /-- The alternatives to the arm `a` in best arm identification are the models with a unique best
 arm `b ≠ a`. -/
@@ -210,6 +213,18 @@ lemma mem_answerSet_baiTask_iff :
   rw [IdentTask.mem_answerSet_iff, M_baiTask, correct_baiTask]
   exact ⟨fun h ↦ h.2, fun h ↦ ⟨⟨a, h⟩, h⟩⟩
 
+/-- For finitely many arms and means continuous in the model, the models with unique best arm `a`
+form an open set. -/
+lemma isOpen_answerSet_baiTask_of_continuous [TopologicalSpace Θ] [Finite ι]
+    (hmean : ∀ b, Continuous fun θ ↦ mean θ b) (a : ι) :
+    IsOpen ((baiTask ν mean).answerSet a) := by
+  have h : (baiTask ν mean).answerSet a = ⋂ b ∈ ({a}ᶜ : Set ι), {θ | mean θ b < mean θ a} := by
+    ext θ
+    rw [mem_answerSet_baiTask_iff]
+    simp
+  rw [h]
+  exact (Set.toFinite _).isOpen_biInter fun b _ ↦ isOpen_lt (hmean b) (hmean a)
+
 variable [Fintype α]
 
 /-- If `a` is the unique best arm of `θ`, then `T*(θ) = D(θ, ¬a)⁻¹` in best arm identification
@@ -230,18 +245,12 @@ theorem charTime_baiTask_eq_inv_answerValue (ha : ∀ b ≠ a, mean θ b < mean
 
 end MeanFunctional
 
-variable (ν : (α → ℝ) → Kernel α 𝓨) [∀ μ, IsMarkovKernel (ν μ)] {S : Set (α → ℝ)}
+variable {a : α} (ν : (α → ℝ) → Kernel α 𝓨) [∀ μ, IsMarkovKernel (ν μ)] {S : Set (α → ℝ)}
   {μ' : α → ℝ}
 
 /-- The vectors of means with unique best arm `a` form an open set. -/
-lemma isOpen_answerSet_baiTask [Finite α] (a : α) : IsOpen ((baiTask ν id).answerSet a) := by
-  have h : (baiTask ν id).answerSet a = ⋂ b ∈ ({a}ᶜ : Set α), {μ' | μ' b < μ' a} := by
-    ext μ'
-    rw [mem_answerSet_baiTask_iff]
-    simp
-  rw [h]
-  exact (Set.toFinite _).isOpen_biInter fun b _ ↦
-    isOpen_lt (continuous_apply b) (continuous_apply a)
+lemma isOpen_answerSet_baiTask [Finite α] (a : α) : IsOpen ((baiTask ν id).answerSet a) :=
+  isOpen_answerSet_baiTask_of_continuous ν id continuous_apply a
 
 /-- For an open set `S` of vectors of means, the models of best arm identification restricted to
 `S` with unique best arm `a` form an open set. -/

LMLExplore/Identification/Task/Classical.lean

@@ -24,7 +24,9 @@ are the models `θ : α → ℝ × ℝ≥0` with `mean θ a = (θ a).1`. The tas
 of mean `μ a`, for example `ν μ = gaussianBandit μ σ2`.
 
 * `baiTask ν mean`: best arm identification. The answer is the arm with the largest mean, on the
-  models with a unique best arm.
+  models with a unique best arm. The answers may form any type `ι`, with `mean : Θ → ι → ℝ`: the
+  answer is then the one with the largest value, as in the transductive task of linear
+  identification.
 * `epsBaiTask ν mean ε`: `ε`-best arm identification. The correct answers are the arms whose mean
   is within `ε` of the largest mean, on every model. Several answers may be correct.
 * `mulEpsBaiTask ν mean ε`: multiplicative `ε`-best arm identification [JDK23b]. The correct
@@ -100,19 +102,20 @@ open MeasureTheory ProbabilityTheory
 
 namespace LMLExplore.Identification
 
-variable {α Θ Θ' 𝓨 : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨}
+variable {α Θ Θ' 𝓨 ι : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨}
 
-section MeanFunctional
+section BestArm
 
 /-! ### Best arm identification -/
 
-variable (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → α → ℝ) {θ : Θ}
+variable (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → ι → ℝ) {θ : Θ}
 
-/-- *Best arm identification* [GK16] on a type `Θ` of models with the mean functional
-`mean : Θ → α → ℝ`: the correct answer of a model `θ` is its arm with the largest mean
-`mean θ a`, and the admissible models are those with a unique best arm. The task on vectors of
-means is `baiTask ν id`. -/
-noncomputable def baiTask : IdentTask α Θ α 𝓨 where
+/-- *Best arm identification* [GK16] on a type `Θ` of models with answers in a type `ι` and the
+mean functional `mean : Θ → ι → ℝ`: the correct answer of a model `θ` is the answer `a` with the
+largest value `mean θ a`, and the admissible models are those with a unique best answer.
+Classical best arm identification is the case `ι = α`, where `mean θ a` is the mean of the arm
+`a`; the task on vectors of means is then `baiTask ν id`. -/
+noncomputable def baiTask : IdentTask α Θ ι 𝓨 where
   M := {θ | ∃ a, ∀ b ≠ a, mean θ b < mean θ a}
   ν := ν
   isMarkovKernel_ν _ := inferInstance
@@ -146,7 +149,7 @@ lemma subsingleton_correct_baiTask (θ : Θ) : ((baiTask ν mean).correct θ).Su
   exact lt_asymm (ha a' (Ne.symm h)) (ha' a h)
 
 /-- The arm `a` is the only best arm of `θ` iff every other arm `b` has `mean θ b < mean θ a`. -/
-lemma correct_baiTask_eq_singleton_iff {a : α} :
+lemma correct_baiTask_eq_singleton_iff {a : ι} :
     (baiTask ν mean).correct θ = {a} ↔ ∀ b ≠ a, mean θ b < mean θ a :=
   ⟨fun h ↦ by simpa using h.symm.subset (Set.mem_singleton a),
     fun h ↦ (subsingleton_correct_baiTask ν mean θ).eq_singleton_of_mem h⟩
@@ -158,6 +161,12 @@ lemma isSingleAnswer_baiTask : (baiTask ν mean).IsSingleAnswer := by
   rintro θ ⟨a, ha⟩
   exact ⟨a, (correct_baiTask_eq_singleton_iff ν mean).2 ha⟩
 
+end BestArm
+
+section MeanFunctional
+
+variable (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → α → ℝ) {θ : Θ}
+
 /-! ### `ε`-best arm identification -/
 
 /-- *`ε`-best arm identification* on a type `Θ` of models with the mean functional

LMLExplore/Identification/Task/Transductive.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import LMLExplore.Identification.Task.BestArm.Basic
+public import Mathlib.Analysis.InnerProductSpace.Basic
+
+/-!
+# Transductive best-answer identification
+
+In a linear model, the models are the vectors `θ` of a real inner product space `E`, and the arm
+`a` of `θ` typically has mean `⟪φ a, θ⟫` for features `φ : α → E`. Linear best arm
+identification, thresholding and the other classical tasks are those of
+`LMLExplore.Identification.Task.Classical` for the mean functional `θ ↦ (⟪φ a, θ⟫)_a`. The
+transductive task of Fiez, Jain, Jamieson and Ratliff (2019) asks a different question: given a
+family `z : ι → E` of answers, which is not required to be the family of features, find the
+answer `z i` with the largest value `⟪z i, θ⟫`. The admissible models are those with a unique
+best answer. This is best arm identification (`baiTask`) with the answers `ι` in place of the arms
+and the values `⟪z i, θ⟫` in place of the means, so that its API is that of `baiTask`. Best arm
+identification in the linear model is the case `ι = α`, `z = φ`, and a finite set `𝒵 ⊆ E` of
+answers is the family `(↑) : 𝒵 → E`.
+
+The alternatives to the answer `i` are the models with a unique best answer `j ≠ i`. For
+finitely many distinct answers, the closure of this set is the union of the half-spaces
+`{λ | ⟪z i - z j, λ⟫ ≤ 0}`, `j ≠ i`, so that the cost of the alternatives
+`D(θ, w, ¬i) = inf_{λ ∈ ¬i} cost_θ(w, λ)` is, for a transportation cost continuous in the
+alternative, the smallest cost of these half-spaces. These are the half-spaces whose costs give
+the characteristic time of linear identification with Gaussian noise
+`T*(θ)⁻¹ = max_w min_{z ≠ z*} ⟪z* - z, θ⟫² / (2 ‖z* - z‖²_{V_w⁻¹})` [FJJR19, Theorem 1].
+
+## Main definitions
+
+* `LMLExplore.Identification.transductiveTask ν z`: the transductive best-answer task with bandits
+  `ν θ` and answers `z i`.
+
+## Main statements
+
+* `LMLExplore.Identification.closure_alt_transductiveTask`: for finitely many distinct answers, the
+  closure of the alternatives to `i` is the union of the half-spaces `{λ | ⟪z i - z j, λ⟫ ≤ 0}`,
+  `j ≠ i`.
+* `LMLExplore.Identification.altCost_transductiveTask_eq_iInf`: for a transportation cost continuous
+  on these half-spaces, `D(θ, w, ¬i)` is the infimum over `j ≠ i` of the smallest cost of the
+  half-space `{λ | ⟪z i - z j, λ⟫ ≤ 0}`.
+
+The single answer (`isSingleAnswer_baiTask`), the alternatives (`mem_alt_baiTask_iff`), the answer
+sets (`mem_answerSet_baiTask_iff`, open for finitely many answers by
+`isOpen_answerSet_baiTask_of_continuous` since each `θ ↦ ⟪z i, θ⟫` is continuous) and the
+characteristic time (`charTime_baiTask_eq_inv_answerValue`) are those of `baiTask`.
+
+## References
+
+* [FJJR19] T. Fiez, L. Jain, K. Jamieson and L. Ratliff, *Sequential experimental design for
+  transductive linear bandits*, NeurIPS 2019, Section 2 and Theorem 1.
+-/
+
+public section
+
+open MeasureTheory ProbabilityTheory Filter Topology
+
+open scoped InnerProductSpace ENNReal
+
+namespace LMLExplore.Identification
+
+variable {α ι E 𝓨 : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSpace 𝓨}
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  (ν : E → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (z : ι → E) {θ : E} {i : ι}
+
+/-- The *transductive best-answer task* [FJJR19] on the models `θ` of a real inner product space
+`E`, with bandits `ν θ` and the family `z : ι → E` of answers: the correct answer of `θ` is the
+answer `i` with the largest value `⟪z i, θ⟫`, and the admissible models are those with a unique
+best answer. This is `baiTask` for the values `⟪z i, θ⟫`. Linear best arm identification is the
+case of the features as answers, `transductiveTask ν φ = baiTask ν (fun θ a ↦ ⟪φ a, θ⟫)`. -/
+noncomputable abbrev transductiveTask : IdentTask α E ι 𝓨 :=
+  baiTask ν (fun θ i ↦ ⟪z i, θ⟫_ℝ)
+
+/-! ### The closure of the alternatives -/
+
+/-- Let `j ≠ i` be a best answer at `θ'` that is, among the best answers other than `i`, the
+farthest from `z i`. If the answers are distinct, then moving `θ'` along the direction
+`z j - z i` makes `j` the unique best answer. -/
+private lemma eventually_forall_inner_lt_inner_add_smul [Finite ι] (hz : Function.Injective z)
+    {θ' : E} {j : ι} (hj : ∀ l, ⟪z l, θ'⟫_ℝ ≤ ⟪z j, θ'⟫_ℝ)
+    (hj_far : ∀ k ≠ i, (∀ l, ⟪z l, θ'⟫_ℝ ≤ ⟪z k, θ'⟫_ℝ) → ‖z k - z i‖ ≤ ‖z j - z i‖) :
+    ∀ᶠ t in 𝓝[>] (0 : ℝ), ∀ k ≠ j,
+      ⟪z k, θ' + t • (z j - z i)⟫_ℝ < ⟪z j, θ' + t • (z j - z i)⟫_ℝ := by
+  set d := z j - z i
+  refine eventually_all.2 fun k ↦ ?_
+  by_cases hkj : k = j
+  · exact Eventually.of_forall fun _ h ↦ absurd hkj h
+  -- The gap `⟪z j - z k, θ' + t • d⟫` is affine in `t`, nonnegative at `t = 0`.
+  suffices ∀ᶠ t in 𝓝[>] (0 : ℝ), 0 < ⟪z j - z k, θ'⟫_ℝ + t * ⟪z j - z k, d⟫_ℝ by
+    filter_upwards [this] with t ht _
+    simp only [inner_add_right, inner_smul_right, inner_sub_left] at ht ⊢
+    linarith
+  rcases (sub_nonneg.2 (hj k)).eq_or_lt with h0 | h0
+  · -- If `k` ties with `j` at `θ'`, the slope `⟪z j - z k, d⟫` is positive, since
+    -- `‖z k - z i‖ ≤ ‖d‖` by the choice of `j` and `z k ≠ z j`.
+    have h_le : ‖z k - z i‖ ≤ ‖d‖ := by
+      by_cases hki : k = i
+      · simp [hki]
+      · exact hj_far k hki fun l ↦ (hj l).trans (by linarith)
+    -- By Cauchy–Schwarz, `⟪z k - z i, d⟫ ≤ ‖d‖ ^ 2`, with equality only at `z k - z i = d`.
+    have h_lt : ⟪z k - z i, d⟫_ℝ < ‖d‖ ^ 2 := by
+      refine ((real_inner_le_norm _ _).trans (by nlinarith [norm_nonneg d])).lt_of_ne fun h ↦ ?_
+      have h_eq := eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := ℝ) h_le (by rwa [RCLike.re_to_real])
+      exact hkj (hz (sub_left_injective h_eq))
+    have h_slope : 0 < ⟪z j - z k, d⟫_ℝ := by
+      rw [← sub_sub_sub_cancel_right (z j) (z k) (z i), inner_sub_left,
+        real_inner_self_eq_norm_sq]
+      linarith
+    filter_upwards [self_mem_nhdsWithin] with t ht
+    rw [inner_sub_left, ← h0, zero_add]
+    exact mul_pos ht h_slope
+  · -- Otherwise the gap is positive at `t = 0`, hence for small `t`.
+    rw [← inner_sub_left] at h0
+    refine nhdsWithin_le_nhds ?_
+    exact continuousAt_const.eventually_lt (by fun_prop) (by simpa using h0)
+
+/-- If the answers are distinct and some answer `j ≠ i` has `⟪z i, θ'⟫ ≤ ⟪z j, θ'⟫`, then `θ'` is
+a limit of models with a unique best answer different from `i`. -/
+lemma mem_closure_alt_transductiveTask [Finite ι] (hz : Function.Injective z) {θ' : E}
+    (h : ∃ j ≠ i, ⟪z i, θ'⟫_ℝ ≤ ⟪z j, θ'⟫_ℝ) :
+    θ' ∈ closure ((transductiveTask ν z).alt i) := by
+  -- The answers `k ≠ i` with the largest value at `θ'`.
+  set A : Set ι := {k | k ≠ i ∧ ∀ l, ⟪z l, θ'⟫_ℝ ≤ ⟪z k, θ'⟫_ℝ}
+  have hA : A.Nonempty := by
+    obtain ⟨j, hji, hj⟩ := h
+    have : Nonempty ι := ⟨i⟩
+    obtain ⟨k, hk⟩ := Finite.exists_max fun k ↦ ⟪z k, θ'⟫_ℝ
+    by_cases hki : k = i
+    · exact ⟨j, hji, fun l ↦ (hk l).trans (hki ▸ hj)⟩
+    · exact ⟨k, hki, hk⟩
+  -- Among them, the answer `j` farthest from `z i`: moving `θ'` along `z j - z i` makes `j` the
+  -- unique best answer.
+  obtain ⟨j, ⟨hji, hj⟩, hj_far⟩ := Set.exists_max_image A (fun k ↦ ‖z k - z i‖) A.toFinite hA
+  have h_ev := eventually_forall_inner_lt_inner_add_smul z hz hj fun k hki hk ↦ hj_far k ⟨hki, hk⟩
+  have h_tendsto : Tendsto (fun t : ℝ ↦ θ' + t • (z j - z i)) (𝓝[>] 0) (𝓝 θ') := by
+    have hc : Continuous fun t : ℝ ↦ θ' + t • (z j - z i) := by fun_prop
+    simpa using hc.continuousWithinAt.tendsto (x := 0) (s := Set.Ioi 0)
+  refine mem_closure_of_tendsto h_tendsto ?_
+  filter_upwards [h_ev] with t ht
+  exact (mem_alt_baiTask_iff ν _).2 ⟨j, hji, ht⟩
+
+/-- For finitely many distinct answers, the closure of the alternatives to the answer `i` in the
+transductive task is the union of the half-spaces `{λ | ⟪z i - z j, λ⟫ ≤ 0}`, `j ≠ i`: the models
+in which some answer `j ≠ i` scores at least as much as `i`. -/
+theorem closure_alt_transductiveTask [Finite ι] (hz : Function.Injective z) (i : ι) :
+    closure ((transductiveTask ν z).alt i) =
+      ⋃ j : {j // j ≠ i}, {θ' | ⟪z i - z j, θ'⟫_ℝ ≤ 0} := by
+  refine Set.Subset.antisymm (closure_minimal (fun θ' hθ' ↦ ?_) ?_) fun θ' hθ' ↦ ?_
+  · obtain ⟨j, hji, hj⟩ := (mem_alt_baiTask_iff ν _).1 hθ'
+    refine Set.mem_iUnion.2 ⟨⟨j, hji⟩, ?_⟩
+    rw [Set.mem_ofPred_eq, inner_sub_left, sub_nonpos]
+    exact (hj i hji.symm).le
+  · exact isClosed_iUnion_of_finite fun j ↦
+      isClosed_le (continuous_const.inner continuous_id) continuous_const
+  · obtain ⟨⟨j, hji⟩, hj⟩ := Set.mem_iUnion.1 hθ'
+    rw [Set.mem_ofPred_eq, inner_sub_left, sub_nonpos] at hj
+    exact mem_closure_alt_transductiveTask ν z hz ⟨j, hji, hj⟩
+
+/-- For finitely many distinct answers and a transportation cost from `θ` continuous on the
+half-spaces `{λ | ⟪z i - z j, λ⟫ ≤ 0}`, `j ≠ i`, the cost of the alternatives to `i` is the
+smallest cost of these half-spaces,
+`D(θ, w, ¬i) = min_{j ≠ i} inf {cost_θ(w, λ) | ⟪z i - z j, λ⟫ ≤ 0}` [FJJR19, Theorem 1]. -/
+theorem altCost_transductiveTask_eq_iInf [Fintype α] [Finite ι] (hz : Function.Injective z)
+    {w : α → ℝ} (hc : ContinuousOn ((transductiveTask ν z).cost w θ)
+      (⋃ j : {j // j ≠ i}, {θ' | ⟪z i - z j, θ'⟫_ℝ ≤ 0})) :
+    (transductiveTask ν z).altCost θ w i =
+      ⨅ (j : {j // j ≠ i}) (θ' ∈ {θ' | ⟪z i - z j, θ'⟫_ℝ ≤ 0}),
+        (transductiveTask ν z).cost w θ θ' := by
+  have h_eq := closure_alt_transductiveTask ν z hz i
+  rw [IdentTask.altCost_eq_biInf_of_subset_closure _ (h_eq ▸ subset_closure) h_eq.ge hc,
+    iInf_iUnion]
+
+end LMLExplore.Identification