From 633490993283063c23e0452ab8047f7cc7542292 Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 20:55:22 +0000 Subject: [PATCH 1/4] feat: the transductive best-answer task and the closure of its alternatives Co-Authored-By: Claude Code --- .../Identification/Task/Transductive.lean | 255 ++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 LMLExplore/Identification/Task/Transductive.lean diff --git a/LMLExplore/Identification/Task/Transductive.lean b/LMLExplore/Identification/Task/Transductive.lean new file mode 100644 index 00000000..8597ce13 --- /dev/null +++ b/LMLExplore/Identification/Task/Transductive.lean @@ -0,0 +1,255 @@ +/- +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.Classical +public import LMLExplore.Identification.Task.TransportationCost +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. Best arm identification in the linear model is the case `ι = α`, `z = φ` +(`transductiveTask_eq_baiTask`), 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.isSingleAnswer_transductiveTask`: the task has a single correct answer + on every admissible model, and `correct_transductiveTask_eq_singleton_iff` characterizes it. +* `LMLExplore.Identification.transductiveTask_eq_baiTask`: with the features as answers, the task is + best arm identification for the mean functional `θ ↦ (⟪φ a, θ⟫)_a`. +* `LMLExplore.Identification.mem_alt_transductiveTask_iff`, + `LMLExplore.Identification.mem_answerSet_transductiveTask_iff`: the alternatives to `i` are the + models with a unique best answer `j ≠ i`, and the models for which `i` is correct are those with + unique best answer `i`. +* `LMLExplore.Identification.isOpen_answerSet_transductiveTask`: for finitely many answers, the + models with unique best answer `i` form an open set. +* `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}`. +* `LMLExplore.Identification.charTime_transductiveTask_eq_inv_answerValue`: if `i` is the unique + best answer of `θ`, then `T*(θ) = D(θ, ¬i)⁻¹`. + +## 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. Linear best arm identification is the case of the features as answers +(`transductiveTask_eq_baiTask`). -/ +noncomputable def transductiveTask : IdentTask α E ι 𝓨 where + M := {θ | ∃ i, ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} + ν := ν + isMarkovKernel_ν _ := inferInstance + correct θ := {i | ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} + +@[simp] +lemma M_transductiveTask : + (transductiveTask ν z).M = {θ | ∃ i, ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := (rfl) + +@[simp] +lemma ν_transductiveTask : (transductiveTask ν z).ν = ν := (rfl) + +@[simp] +lemma correct_transductiveTask (θ : E) : + (transductiveTask ν z).correct θ = {i | ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := (rfl) + +/-- With the features `φ` as answers, the transductive task is best arm identification for the +mean functional `θ ↦ (⟪φ a, θ⟫)_a` of the linear model. -/ +lemma transductiveTask_eq_baiTask (φ : α → E) : + transductiveTask ν φ = baiTask ν (fun θ a ↦ ⟪φ a, θ⟫_ℝ) := by + ext <;> simp + +/-- A model has at most one best answer. -/ +lemma subsingleton_correct_transductiveTask (θ : E) : + ((transductiveTask ν z).correct θ).Subsingleton := by + intro i hi i' hi' + by_contra h + simp only [correct_transductiveTask, Set.mem_ofPred_eq] at hi hi' + exact lt_asymm (hi i' (Ne.symm h)) (hi' i h) + +/-- The answer `i` is the only best answer of `θ` iff every other answer `j` has +`⟪z j, θ⟫ < ⟪z i, θ⟫`. -/ +lemma correct_transductiveTask_eq_singleton_iff : + (transductiveTask ν z).correct θ = {i} ↔ ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ := + ⟨fun h ↦ by simpa using h.symm.subset (Set.mem_singleton i), + fun h ↦ (subsingleton_correct_transductiveTask ν z θ).eq_singleton_of_mem h⟩ + +/-- The transductive task is a single-answer task: every model with a unique best answer has +exactly one correct answer, its best answer. -/ +lemma isSingleAnswer_transductiveTask : (transductiveTask ν z).IsSingleAnswer := by + refine (IdentTask.isSingleAnswer_iff _).2 ?_ + rintro θ ⟨i, hi⟩ + exact ⟨i, (correct_transductiveTask_eq_singleton_iff ν z).2 hi⟩ + +/-- The alternatives to the answer `i` in the transductive task are the models with a unique best +answer `j ≠ i`. -/ +lemma mem_alt_transductiveTask_iff : + θ ∈ (transductiveTask ν z).alt i ↔ ∃ j ≠ i, ∀ k ≠ j, ⟪z k, θ⟫_ℝ < ⟪z j, θ⟫_ℝ := by + simp only [IdentTask.mem_alt_iff, M_transductiveTask, correct_transductiveTask, + Set.mem_ofPred_eq, not_forall, not_lt, exists_prop] + constructor + · rintro ⟨⟨j, hj⟩, k, hki, hk⟩ + refine ⟨j, ?_, hj⟩ + rintro rfl + exact (hj k hki).not_ge hk + · rintro ⟨j, hji, hj⟩ + exact ⟨⟨j, hj⟩, j, hji, (hj i hji.symm).le⟩ + +/-- The models for which the answer `i` is correct in the transductive task are those with unique +best answer `i`. -/ +lemma mem_answerSet_transductiveTask_iff : + θ ∈ (transductiveTask ν z).answerSet i ↔ ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ := by + rw [IdentTask.mem_answerSet_iff, M_transductiveTask, correct_transductiveTask] + exact ⟨fun h ↦ h.2, fun h ↦ ⟨⟨i, h⟩, h⟩⟩ + +/-- For finitely many answers, the models with unique best answer `i` form an open set. -/ +lemma isOpen_answerSet_transductiveTask [Finite ι] (i : ι) : + IsOpen ((transductiveTask ν z).answerSet i) := by + have h : (transductiveTask ν z).answerSet i = + ⋂ j ∈ ({i}ᶜ : Set ι), {θ | ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := by + ext θ + rw [mem_answerSet_transductiveTask_iff] + simp + rw [h] + exact (Set.toFinite _).isOpen_biInter fun j _ ↦ + isOpen_lt (continuous_const.inner continuous_id) (continuous_const.inner continuous_id) + +/-! ### The closure of the alternatives -/ + +/-- 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`, and the direction `d = z j - z i`: moving + -- `θ'` along `d` 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 + set d := z j - z i + have h_ev : ∀ᶠ t in 𝓝[>] (0 : ℝ), ∀ k ≠ j, ⟪z k, θ' + t • d⟫_ℝ < ⟪z j, θ' + t • d⟫_ℝ := by + 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)⟩ + have h_ne : 0 < ‖d - (z k - z i)‖ := by + rw [norm_pos_iff, sub_sub_sub_cancel_right, sub_ne_zero] + exact hz.ne (Ne.symm hkj) + 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, real_inner_comm] + nlinarith [norm_sub_sq_real d (z k - z i), norm_nonneg (z k - z i), norm_nonneg d] + 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) + have h_tendsto : Tendsto (fun t : ℝ ↦ θ' + t • d) (𝓝[>] 0) (𝓝 θ') := by + have hc : Continuous fun t : ℝ ↦ θ' + t • d := 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_transductiveTask_iff ν z).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_transductiveTask_iff ν z).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] + +/-- If `i` is the unique best answer of `θ`, then `T*(θ) = D(θ, ¬i)⁻¹` in the transductive task. -/ +theorem charTime_transductiveTask_eq_inv_answerValue [Fintype α] + (hi : ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ) : + (transductiveTask ν z).charTime θ = ((transductiveTask ν z).answerValue θ i)⁻¹ := + IdentTask.charTime_eq_inv_answerValue _ ((correct_transductiveTask_eq_singleton_iff ν z).2 hi) + +end LMLExplore.Identification From 898f4d8733f837be70cdd634e2ec0b18a382a2f4 Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 21:27:21 +0000 Subject: [PATCH 2/4] refactor: derive the transductive task from an answer-generic baiTask MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize `baiTask` and its answer-agnostic lemmas (`M_`, `ν_`, `correct_`, `comap_`, `subsingleton_correct_`, `correct_baiTask_eq_singleton_iff`, `isSingleAnswer_`, `mem_alt_`, `mem_answerSet_`, `charTime_..._eq_inv_answerValue`) from the arm type to any answer type `ι`, make `transductiveTask` an abbreviation of `baiTask` for the values `⟪z i, θ⟫`, and delete its copied API. Prove the slope step of the closure argument with Mathlib's `eq_of_norm_le_re_inner_eq_norm_sq` and split it into a private lemma. Co-Authored-By: Claude Code --- .../Identification/Task/BestArm/Basic.lean | 7 +- LMLExplore/Identification/Task/Classical.lean | 26 ++- .../Identification/Task/Transductive.lean | 188 ++++++------------ 3 files changed, 85 insertions(+), 136 deletions(-) diff --git a/LMLExplore/Identification/Task/BestArm/Basic.lean b/LMLExplore/Identification/Task/BestArm/Basic.lean index 86b1ad05..33f9f7e3 100644 --- a/LMLExplore/Identification/Task/BestArm/Basic.lean +++ b/LMLExplore/Identification/Task/BestArm/Basic.lean @@ -183,11 +183,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`. -/ @@ -230,7 +231,7 @@ 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. -/ diff --git a/LMLExplore/Identification/Task/Classical.lean b/LMLExplore/Identification/Task/Classical.lean index c0d9ddb2..68b7a109 100644 --- a/LMLExplore/Identification/Task/Classical.lean +++ b/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,23 @@ 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 +means is `baiTask ν id`. + +More generally, the answers form any type `ι`, with the value `mean θ a` of the answer `a` under +`θ`, and the correct answer is the one with the largest value. Best arm identification is the case +`ι = α`. -/ +noncomputable def baiTask : IdentTask α Θ ι 𝓨 where M := {θ | ∃ a, ∀ b ≠ a, mean θ b < mean θ a} ν := ν isMarkovKernel_ν _ := inferInstance @@ -146,7 +152,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 +164,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 diff --git a/LMLExplore/Identification/Task/Transductive.lean b/LMLExplore/Identification/Task/Transductive.lean index 8597ce13..e8f8dd15 100644 --- a/LMLExplore/Identification/Task/Transductive.lean +++ b/LMLExplore/Identification/Task/Transductive.lean @@ -5,8 +5,7 @@ Authors: LMLExplore contributors -/ module -public import LMLExplore.Identification.Task.Classical -public import LMLExplore.Identification.Task.TransportationCost +public import LMLExplore.Identification.Task.BestArm.Basic public import Mathlib.Analysis.InnerProductSpace.Basic /-! @@ -19,9 +18,10 @@ identification, thresholding and the other classical tasks are those of 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. Best arm identification in the linear model is the case `ι = α`, `z = φ` -(`transductiveTask_eq_baiTask`), and a finite set `𝒵 ⊆ E` of answers is the family -`(↑) : 𝒵 → E`. +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 @@ -38,14 +38,6 @@ the characteristic time of linear identification with Gaussian noise ## Main statements -* `LMLExplore.Identification.isSingleAnswer_transductiveTask`: the task has a single correct answer - on every admissible model, and `correct_transductiveTask_eq_singleton_iff` characterizes it. -* `LMLExplore.Identification.transductiveTask_eq_baiTask`: with the features as answers, the task is - best arm identification for the mean functional `θ ↦ (⟪φ a, θ⟫)_a`. -* `LMLExplore.Identification.mem_alt_transductiveTask_iff`, - `LMLExplore.Identification.mem_answerSet_transductiveTask_iff`: the alternatives to `i` are the - models with a unique best answer `j ≠ i`, and the models for which `i` is correct are those with - unique best answer `i`. * `LMLExplore.Identification.isOpen_answerSet_transductiveTask`: for finitely many answers, the models with unique best answer `i` form an open set. * `LMLExplore.Identification.closure_alt_transductiveTask`: for finitely many distinct answers, the @@ -54,8 +46,10 @@ the characteristic time of linear identification with Gaussian noise * `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}`. -* `LMLExplore.Identification.charTime_transductiveTask_eq_inv_answerValue`: if `i` is the unique - best answer of `θ`, then `T*(θ) = D(θ, ¬i)⁻¹`. + +The single answer (`isSingleAnswer_baiTask`), the alternatives (`mem_alt_baiTask_iff`), the answer +sets (`mem_answerSet_baiTask_iff`) and the characteristic time +(`charTime_baiTask_eq_inv_answerValue`) are those of `baiTask`. ## References @@ -78,73 +72,10 @@ variable {α ι E 𝓨 : Type*} {mα : MeasurableSpace α} {m𝓨 : MeasurableSp /-- 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. Linear best arm identification is the case of the features as answers -(`transductiveTask_eq_baiTask`). -/ -noncomputable def transductiveTask : IdentTask α E ι 𝓨 where - M := {θ | ∃ i, ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} - ν := ν - isMarkovKernel_ν _ := inferInstance - correct θ := {i | ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} - -@[simp] -lemma M_transductiveTask : - (transductiveTask ν z).M = {θ | ∃ i, ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := (rfl) - -@[simp] -lemma ν_transductiveTask : (transductiveTask ν z).ν = ν := (rfl) - -@[simp] -lemma correct_transductiveTask (θ : E) : - (transductiveTask ν z).correct θ = {i | ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := (rfl) - -/-- With the features `φ` as answers, the transductive task is best arm identification for the -mean functional `θ ↦ (⟪φ a, θ⟫)_a` of the linear model. -/ -lemma transductiveTask_eq_baiTask (φ : α → E) : - transductiveTask ν φ = baiTask ν (fun θ a ↦ ⟪φ a, θ⟫_ℝ) := by - ext <;> simp - -/-- A model has at most one best answer. -/ -lemma subsingleton_correct_transductiveTask (θ : E) : - ((transductiveTask ν z).correct θ).Subsingleton := by - intro i hi i' hi' - by_contra h - simp only [correct_transductiveTask, Set.mem_ofPred_eq] at hi hi' - exact lt_asymm (hi i' (Ne.symm h)) (hi' i h) - -/-- The answer `i` is the only best answer of `θ` iff every other answer `j` has -`⟪z j, θ⟫ < ⟪z i, θ⟫`. -/ -lemma correct_transductiveTask_eq_singleton_iff : - (transductiveTask ν z).correct θ = {i} ↔ ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ := - ⟨fun h ↦ by simpa using h.symm.subset (Set.mem_singleton i), - fun h ↦ (subsingleton_correct_transductiveTask ν z θ).eq_singleton_of_mem h⟩ - -/-- The transductive task is a single-answer task: every model with a unique best answer has -exactly one correct answer, its best answer. -/ -lemma isSingleAnswer_transductiveTask : (transductiveTask ν z).IsSingleAnswer := by - refine (IdentTask.isSingleAnswer_iff _).2 ?_ - rintro θ ⟨i, hi⟩ - exact ⟨i, (correct_transductiveTask_eq_singleton_iff ν z).2 hi⟩ - -/-- The alternatives to the answer `i` in the transductive task are the models with a unique best -answer `j ≠ i`. -/ -lemma mem_alt_transductiveTask_iff : - θ ∈ (transductiveTask ν z).alt i ↔ ∃ j ≠ i, ∀ k ≠ j, ⟪z k, θ⟫_ℝ < ⟪z j, θ⟫_ℝ := by - simp only [IdentTask.mem_alt_iff, M_transductiveTask, correct_transductiveTask, - Set.mem_ofPred_eq, not_forall, not_lt, exists_prop] - constructor - · rintro ⟨⟨j, hj⟩, k, hki, hk⟩ - refine ⟨j, ?_, hj⟩ - rintro rfl - exact (hj k hki).not_ge hk - · rintro ⟨j, hji, hj⟩ - exact ⟨⟨j, hj⟩, j, hji, (hj i hji.symm).le⟩ - -/-- The models for which the answer `i` is correct in the transductive task are those with unique -best answer `i`. -/ -lemma mem_answerSet_transductiveTask_iff : - θ ∈ (transductiveTask ν z).answerSet i ↔ ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ := by - rw [IdentTask.mem_answerSet_iff, M_transductiveTask, correct_transductiveTask] - exact ⟨fun h ↦ h.2, fun h ↦ ⟨⟨i, h⟩, h⟩⟩ +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, θ⟫_ℝ) /-- For finitely many answers, the models with unique best answer `i` form an open set. -/ lemma isOpen_answerSet_transductiveTask [Finite ι] (i : ι) : @@ -152,7 +83,7 @@ lemma isOpen_answerSet_transductiveTask [Finite ι] (i : ι) : have h : (transductiveTask ν z).answerSet i = ⋂ j ∈ ({i}ᶜ : Set ι), {θ | ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := by ext θ - rw [mem_answerSet_transductiveTask_iff] + rw [mem_answerSet_baiTask_iff] simp rw [h] exact (Set.toFinite _).isOpen_biInter fun j _ ↦ @@ -160,6 +91,47 @@ lemma isOpen_answerSet_transductiveTask [Finite ι] (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} @@ -174,46 +146,16 @@ lemma mem_closure_alt_transductiveTask [Finite ι] (hz : Function.Injective z) { 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`, and the direction `d = z j - z i`: moving - -- `θ'` along `d` makes `j` the unique best answer. + -- 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 - set d := z j - z i - have h_ev : ∀ᶠ t in 𝓝[>] (0 : ℝ), ∀ k ≠ j, ⟪z k, θ' + t • d⟫_ℝ < ⟪z j, θ' + t • d⟫_ℝ := by - 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)⟩ - have h_ne : 0 < ‖d - (z k - z i)‖ := by - rw [norm_pos_iff, sub_sub_sub_cancel_right, sub_ne_zero] - exact hz.ne (Ne.symm hkj) - 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, real_inner_comm] - nlinarith [norm_sub_sq_real d (z k - z i), norm_nonneg (z k - z i), norm_nonneg d] - 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) - have h_tendsto : Tendsto (fun t : ℝ ↦ θ' + t • d) (𝓝[>] 0) (𝓝 θ') := by - have hc : Continuous fun t : ℝ ↦ θ' + t • d := by fun_prop + 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_transductiveTask_iff ν z).2 ⟨j, hji, 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 @@ -222,7 +164,7 @@ 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_transductiveTask_iff ν z).1 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 @@ -246,10 +188,4 @@ theorem altCost_transductiveTask_eq_iInf [Fintype α] [Finite ι] (hz : Function rw [IdentTask.altCost_eq_biInf_of_subset_closure _ (h_eq ▸ subset_closure) h_eq.ge hc, iInf_iUnion] -/-- If `i` is the unique best answer of `θ`, then `T*(θ) = D(θ, ¬i)⁻¹` in the transductive task. -/ -theorem charTime_transductiveTask_eq_inv_answerValue [Fintype α] - (hi : ∀ j ≠ i, ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ) : - (transductiveTask ν z).charTime θ = ((transductiveTask ν z).answerValue θ i)⁻¹ := - IdentTask.charTime_eq_inv_answerValue _ ((correct_transductiveTask_eq_singleton_iff ν z).2 hi) - end LMLExplore.Identification From e357071b71bfddc43ba8a332704335d8661c2fad Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 21:46:40 +0000 Subject: [PATCH 3/4] refactor: prove openness of baiTask answer sets for any continuous mean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add isOpen_answerSet_baiTask_of_continuous, derive isOpen_answerSet_baiTask from it, and drop isOpen_answerSet_transductiveTask, which is now its instance for the continuous maps θ ↦ ⟪z i, θ⟫. Co-Authored-By: Claude Code --- .../Identification/Task/BestArm/Basic.lean | 24 ++++++++++++------- .../Identification/Task/Transductive.lean | 19 +++------------ 2 files changed, 19 insertions(+), 24 deletions(-) diff --git a/LMLExplore/Identification/Task/BestArm/Basic.lean b/LMLExplore/Identification/Task/BestArm/Basic.lean index 33f9f7e3..2f544aba 100644 --- a/LMLExplore/Identification/Task/BestArm/Basic.lean +++ b/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 @@ -211,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 @@ -235,14 +249,8 @@ variable {a : α} (ν : (α → ℝ) → Kernel α 𝓨) [∀ μ, IsMarkovKernel {μ' : α → ℝ} /-- 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. -/ diff --git a/LMLExplore/Identification/Task/Transductive.lean b/LMLExplore/Identification/Task/Transductive.lean index e8f8dd15..ed893a2f 100644 --- a/LMLExplore/Identification/Task/Transductive.lean +++ b/LMLExplore/Identification/Task/Transductive.lean @@ -38,8 +38,6 @@ the characteristic time of linear identification with Gaussian noise ## Main statements -* `LMLExplore.Identification.isOpen_answerSet_transductiveTask`: for finitely many answers, the - models with unique best answer `i` form an open set. * `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`. @@ -48,8 +46,9 @@ the characteristic time of linear identification with Gaussian noise 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`) and the characteristic time -(`charTime_baiTask_eq_inv_answerValue`) are those of `baiTask`. +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 @@ -77,18 +76,6 @@ case of the features as answers, `transductiveTask ν φ = baiTask ν (fun θ a noncomputable abbrev transductiveTask : IdentTask α E ι 𝓨 := baiTask ν (fun θ i ↦ ⟪z i, θ⟫_ℝ) -/-- For finitely many answers, the models with unique best answer `i` form an open set. -/ -lemma isOpen_answerSet_transductiveTask [Finite ι] (i : ι) : - IsOpen ((transductiveTask ν z).answerSet i) := by - have h : (transductiveTask ν z).answerSet i = - ⋂ j ∈ ({i}ᶜ : Set ι), {θ | ⟪z j, θ⟫_ℝ < ⟪z i, θ⟫_ℝ} := by - ext θ - rw [mem_answerSet_baiTask_iff] - simp - rw [h] - exact (Set.toFinite _).isOpen_biInter fun j _ ↦ - isOpen_lt (continuous_const.inner continuous_id) (continuous_const.inner continuous_id) - /-! ### The closure of the alternatives -/ /-- Let `j ≠ i` be a best answer at `θ'` that is, among the best answers other than `i`, the From 6a7acb6f78d00a6aa54984f9737127c4197d8a64 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:07:46 +0100 Subject: [PATCH 4/4] doc: state the generalised signature in the baiTask docstring Co-Authored-By: Claude Code --- LMLExplore/Identification/Task/Classical.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/LMLExplore/Identification/Task/Classical.lean b/LMLExplore/Identification/Task/Classical.lean index 68b7a109..22387a54 100644 --- a/LMLExplore/Identification/Task/Classical.lean +++ b/LMLExplore/Identification/Task/Classical.lean @@ -110,14 +110,11 @@ section BestArm 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`. - -More generally, the answers form any type `ι`, with the value `mean θ a` of the answer `a` under -`θ`, and the correct answer is the one with the largest value. Best arm identification is the case -`ι = α`. -/ +/-- *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} ν := ν