From 9aa7b78eb54052d27f07ad527b72abeb4ad68d74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Thu, 20 Aug 2026 11:24:50 +0200 Subject: [PATCH 1/2] Fix warnings --- .../ForMathlib/Probability/Kernel/KernelSub.lean | 2 +- LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean | 4 ++-- LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean | 2 +- LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean | 2 +- .../SequentialLearning/FiniteActions.lean | 10 +++++----- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean index bf8cc83d..2bd57160 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean @@ -74,7 +74,7 @@ lemma sub_of_not_isSFiniteKernel_right [∀ η : Kernel α β, Decidable (IsSFin lemma sub_of_isSFiniteKernel [IsSFiniteKernel κ] [IsSFiniteKernel η] [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] : κ - η = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η := by - rw [sub_def, dif_pos] + rw [sub_def, dite_eq_left] exact ⟨inferInstance, inferInstance⟩ -- todo name diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean index bcba73ed..97a1ba05 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean @@ -105,7 +105,7 @@ lemma arm_mul [Nonempty (Fin K)] grind rw [this] filter_upwards [arm_ae_eq_etcNextArm h (K * m - 1)] with ω hn_eq - rw [hn_eq, nextArm, dif_neg (by simp), dif_pos rfl] + rw [hn_eq, nextArm, dite_eq_right (by simp), dite_eq_left rfl] exact this ▸ rfl /-- For `n ≥ K * m`, the arm pulled at time `n + 1` is the same as the arm pulled at time `n`. -/ @@ -113,7 +113,7 @@ lemma arm_add_one_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv {n : ℕ} (hm : m ≠ 0) (hn : K * m ≤ n) : A (n + 1) =ᵐ[P] fun ω ↦ A n ω := by filter_upwards [arm_ae_eq_etcNextArm h n] with ω hn_eq - rw [hn_eq, nextArm, dif_neg (by grind), dif_neg] + rw [hn_eq, nextArm, dite_eq_right (by grind), dite_eq_right] · rfl · have : 0 < K * m := Nat.mul_pos hK hm.bot_lt grind diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean index cdda9e1f..19f74348 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean @@ -132,7 +132,7 @@ lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationa | zero => exact arm_zero h | succ n _ => filter_upwards [arm_ae_eq_ucbNextArm h n] with h h_eq - rw [h_eq, nextArm, if_pos] + rw [h_eq, nextArm, ite_eq_left] · rfl · grind diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index c76aa2df..a3ff3bf9 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -495,7 +495,7 @@ lemma measurable_hist_truePast [Countable 𝓐] (alg : Algorithm 𝓐 R) by_cases hb : b = a · subst hb simp only [truePast, ↓reduceIte] - rw [min_eq_left, if_pos (by grind)] + rw [min_eq_left, ite_eq_left (by grind)] grind · simp [truePast, hb] rw [h_eq] diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean index f9723003..1da04e72 100644 --- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean +++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean @@ -324,7 +324,7 @@ lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) : exact exists_pullCount_eq_of_le hs hm by_cases h_exists : ∃ s, m ≤ pullCount A a (s + 1) ω swap; · simp_rw [h_iff]; simp [h_exists] - rw [if_pos h_exists, dif_pos] + rw [ite_eq_left h_exists, dite_eq_left] swap; · rwa [h_iff] simp only [ENat.some_eq_natCast, Nat.cast_inj] rw [Nat.find_eq_iff] @@ -476,7 +476,7 @@ lemma stepsUntil_eq_iff {ω : Ω} (n : ℕ) : refine ⟨pullCount_add_one_eq_of_stepsUntil_eq_coe h, fun k hk ↦ ?_⟩ exact pullCount_lt_of_le_stepsUntil a ω h_exists (by rw [h]; exact mod_cast hk) · classical - rw [stepsUntil_eq_dite a m ω, dif_pos ⟨n, h.1⟩] + rw [stepsUntil_eq_dite a m ω, dite_eq_left ⟨n, h.1⟩] simp only [Nat.cast_inj] rw [Nat.find_eq_iff] exact ⟨h.1, fun k hk ↦ (h.2 k hk).ne⟩ @@ -810,7 +810,7 @@ lemma sumRewards_eq_of_pullCount_eq {R' : ℕ → Ω → ℝ} {s t : ℕ} intro ha have h1 := ha ▸ pullCount_action_eq_pullCount_add_one (A := A) t ω lia - rw [sumRewards_add_one, if_neg hne, add_zero, ih h_eq_t] + rw [sumRewards_add_one, ite_eq_right hne, add_zero, ih h_eq_t] lemma sumRewards_eq_pullCount_mul_empMean {R' : ℕ → Ω → ℝ} {ω : Ω} (h_pull : pullCount A a t ω ≠ 0) : @@ -825,9 +825,9 @@ lemma sum_rewardByCount_eq_sumRewards {R' : ℕ → Ω → ℝ} (a : 𝓐) (t : · rw [← hta] at ht ⊢ rw [pullCount_action_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht] unfold sumRewards - rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward] + rw [sum_range_succ, ite_eq_left rfl, rewardByCount_pullCount_add_one_eq_reward] · unfold sumRewards - rwa [pullCount_eq_pullCount_of_action_ne hta, sum_range_succ, if_neg hta, add_zero] + rwa [pullCount_eq_pullCount_of_action_ne hta, sum_range_succ, ite_eq_right hta, add_zero] lemma sumRewards_add_one_eq_sumRewards' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} : sumRewards A R' a (n + 1) ω = sumRewards' n (fun i ↦ (A i ω, R' i ω)) a := by From 9312925086cca2650375342efbc8c249e214ec50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Thu, 20 Aug 2026 11:25:01 +0200 Subject: [PATCH 2/2] Add `--wfail` build arg --- .github/workflows/blueprint.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 6e04f9c5..7b5fd73d 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -104,6 +104,7 @@ jobs: uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 with: build: true + build-args: "--wfail" lint: true mk_all-check: true