Skip to content

Commit 8a729aa

Browse files
RemyDegenneRemyDegenne
committed
fix
1 parent f331f56 commit 8a729aa

8 files changed

Lines changed: 45 additions & 18 deletions

File tree

‎LeanMachineLearning.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ public import LeanMachineLearning.BanditAlgorithms.UCB
1212
public import LeanMachineLearning.BanditAlgorithms.Uniform
1313
public import LeanMachineLearning.ForMathlib.CondDistrib
1414
public import LeanMachineLearning.ForMathlib.CondIndepFun
15+
public import LeanMachineLearning.ForMathlib.FullSupport
1516
public import LeanMachineLearning.ForMathlib.HasCondDistrib
1617
public import LeanMachineLearning.ForMathlib.IndepFun
1718
public import LeanMachineLearning.ForMathlib.IndepInfinitePi
@@ -22,6 +23,7 @@ public import LeanMachineLearning.ForMathlib.MeasurableArgMax
2223
public import LeanMachineLearning.ForMathlib.StandardBorel
2324
public import LeanMachineLearning.ForMathlib.SubGaussian
2425
public import LeanMachineLearning.ForMathlib.Traj
26+
public import LeanMachineLearning.ForMathlib.WithDensity
2527
public import LeanMachineLearning.SequentialLearning.Algorithm
2628
public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
2729
public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv

‎LeanMachineLearning/Bandit/SumRewards.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -414,7 +414,7 @@ private lemma exp_neg_sqrt_sq_div_le {σ2 : ℝ≥0} (hσ2 : 0 < σ2) {δ : ℝ}
414414
rw [Real.sq_sqrt (by positivity)]
415415
field_simp
416416
simp [Real.exp_log hδ]
417-
· push_neg at hd
417+
· push Not at hd
418418
have hl : Real.log (1 / δ) ≤ 0 := Real.log_nonpos (by positivity) (div_le_one_of_le₀ hd (hδ.le))
419419
rw [Real.sqrt_eq_zero_of_nonpos (mul_nonpos_of_nonneg_of_nonpos (by positivity) hl)]
420420
simp [hd]

‎LeanMachineLearning/BanditAlgorithms/TS.lean‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,16 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import LeanBandits.Bandit.SumRewards
7-
import LeanBandits.BanditAlgorithms.Uniform
8-
import LeanBandits.SequentialLearning.AlgorithmDensity
6+
module
7+
8+
public import LeanMachineLearning.Bandit.SumRewards
9+
public import LeanMachineLearning.BanditAlgorithms.Uniform
10+
public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
911

1012
/-! # The Thompson Sampling Algorithm -/
1113

14+
@[expose] public section
15+
1216
open MeasureTheory ProbabilityTheory Finset Learning
1317

1418
open scoped NNReal
@@ -309,7 +313,7 @@ private lemma abs_sumRewards_sub_pullCount_mul_ge {a : Fin K} {n : ℕ} {ω : Ω
309313
2 * σ2 * Real.log (1 / δ) / pullCount A a n ω * pullCount A a n ω ^ 2 := by
310314
field_simp
311315
rw [this, Real.sqrt_mul (div_nonneg hc hk.le), Real.sqrt_sq hk.le]
312-
· rw [Real.sqrt_eq_zero_of_nonpos (by push_neg at hc; nlinarith)]
316+
· rw [Real.sqrt_eq_zero_of_nonpos (by push Not at hc; nlinarith)]
313317
exact mul_nonneg (Real.sqrt_nonneg _) hk.le
314318
_ ≤ |sumRewards A R' a n ω / pullCount A a n ω - μ| * pullCount A a n ω :=
315319
mul_le_mul_of_nonneg_right h hk.le
@@ -561,7 +565,7 @@ lemma bayesRegret_le_of_delta [Nonempty (Fin K)] [StandardBorelSpace Ω] [Nonemp
561565
have : Eδᶜ = {ω | ∃ s < n, ∃ a, pullCount A a s ω ≠ 0 ∧
562566
√(2 * ↑σ2 * Real.log (1 / δ) / (pullCount A a s ω : ℝ)) ≤
563567
|empMean A R' a s ω - armMean a ω|} := by
564-
ext ω; simp only [Eδ, Set.mem_compl_iff, Set.mem_setOf_eq]; push_neg; rfl
568+
ext ω; simp only [Eδ, Set.mem_compl_iff, Set.mem_setOf_eq]; push Not; rfl
565569
rw [this]
566570
exact (h.prob_abs_empMean_sub_actionMean_ge_le hσ2 hs hδ n).trans
567571
(ENNReal.ofReal_le_ofReal (by nlinarith [hδ.le, Nat.cast_nonneg (α := ℝ) K]))
@@ -598,7 +602,7 @@ lemma bayesRegret_le_of_delta [Nonempty (Fin K)] [StandardBorelSpace Ω] [Nonemp
598602
have : Fδᶜ = {ω | ∃ s < n, pullCount A (bestArm ω) s ω ≠ 0 ∧
599603
√(2 * ↑σ2 * Real.log (1 / δ) / (pullCount A (bestArm ω) s ω : ℝ)) ≤
600604
|empMean A R' (bestArm ω) s ω - armMean (bestArm ω) ω|} := by
601-
ext ω; simp only [Fδ, Set.mem_compl_iff, Set.mem_setOf_eq]; push_neg; rfl
605+
ext ω; simp only [Fδ, Set.mem_compl_iff, Set.mem_setOf_eq]; push Not; rfl
602606
rw [this]
603607
exact (h.prob_abs_empMean_bestAction_sub_actionMean_ge_le hσ2 hs hδ n).trans
604608
(ENNReal.ofReal_le_ofReal (by nlinarith [hδ.le]))

‎LeanMachineLearning/BanditAlgorithms/Uniform.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,15 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import LeanBandits.ForMathlib.FullSupport
7-
import LeanBandits.SequentialLearning.Algorithm
6+
module
7+
8+
public import LeanMachineLearning.ForMathlib.FullSupport
9+
public import LeanMachineLearning.SequentialLearning.Algorithm
810

911
/-! # The Uniform Algorithm -/
1012

13+
@[expose] public section
14+
1115
open MeasureTheory ProbabilityTheory Learning
1216

1317
namespace Bandits

‎LeanMachineLearning/ForMathlib/FullSupport.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,11 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import Mathlib.Probability.Kernel.Composition.MeasureCompProd
6+
module
7+
8+
public import Mathlib.Probability.Kernel.Composition.MeasureCompProd
9+
10+
@[expose] public section
711

812
open MeasureTheory ProbabilityTheory
913

‎LeanMachineLearning/ForMathlib/WithDensity.lean‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,20 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import Mathlib.Probability.Kernel.CompProdEqIff
7-
import Mathlib.Probability.Kernel.Composition.MeasureComp
6+
module
7+
8+
public import Mathlib.Probability.Kernel.CompProdEqIff
9+
public import Mathlib.Probability.Kernel.Composition.MeasureComp
10+
811
/-!
912
# Interactions of `withDensity` with `compProd`, `map`, and `swap`
1013
1114
Lemmas for pushing `Measure.withDensity` and `Kernel.withDensity` through
1215
`compProd`, `MeasurableEquiv.map`, `Prod.swap`, and composition.
1316
-/
1417

18+
@[expose] public section
19+
1520
open MeasureTheory ProbabilityTheory
1621

1722
open scoped ENNReal

‎LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,13 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import LeanBandits.ForMathlib.FullSupport
7-
import LeanBandits.ForMathlib.WithDensity
8-
import LeanBandits.SequentialLearning.BayesStationaryEnv
6+
module
7+
8+
public import LeanMachineLearning.ForMathlib.FullSupport
9+
public import LeanMachineLearning.ForMathlib.WithDensity
10+
public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv
11+
12+
@[expose] public section
913

1014
open MeasureTheory ProbabilityTheory Finset
1115

‎LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,16 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
6-
import LeanBandits.Bandit.Regret
7-
import LeanBandits.ForMathlib.MeasurableArgMax
8-
import LeanBandits.SequentialLearning.StationaryEnv
6+
module
7+
8+
public import LeanMachineLearning.Bandit.Regret
9+
public import LeanMachineLearning.ForMathlib.MeasurableArgMax
10+
public import LeanMachineLearning.SequentialLearning.StationaryEnv
911

1012
/-! # Bayesian stationary environments -/
1113

14+
@[expose] public section
15+
1216
open MeasureTheory ProbabilityTheory Finset
1317

1418
namespace Learning

0 commit comments

Comments
 (0)