Benchmark / LML

LML: Mathlib v4.32.0 → v4.35.0

lake build passes after repair. The bump spans 3 Mathlib releases and produced 30 raw build errors in 3 files; an alias rewrite resolves 0 of them.

Project: LeanMachineLearning/LML. First build after the bump: 50.6 s, 3 deprecation warnings (2 with a replacement an alias rewrite would apply).

Changed what it proves. The repair that made lake build pass also changed the project itself:

LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean::map_swap_compProd_map_condDistrib: statement weakened

Review these before you treat the build as a proof of the original statement.

Repairs

Arm	lake build	Rebuilds	Agent min	Labelled changes
Arm A (diagnosing session, not blind)	green	11	120	3 signature change, 1 rename, 1 reproof

What changed, labelled

Label	File	What changed in Mathlib, and the repair
signature change	ForMathlib/Probability/HasCondDistrib.lean, ForMathlib/Probability/Independence/CondDistrib.lean, Independence/IndepFun.lean, ForMathlib/Probability/WithDensity.lean	compProd_map_condDistrib, condDistrib_comp, condDistrib_ae_eq_*, fst_map_prodMk, snd_map_prodMk now take both hX and hY as hypotheses (X was explicit); callers updated. Two lemmas moved to modules no longer re-exported: new `public import` lines added.
signature change	Online/Bandit/Algorithms/TS.lean, SequentialLearning/AlgorithmDensityBayes.lean, BayesStationaryEnv.lean, StationaryEnv.lean, FiniteActions.lean, Algorithms/RoundRobin.lean	Same hX/hY change at call sites; Measure.map of a non-AEMeasurable function is now a dirac junk value (not 0); isProbabilityMeasure_map is now an instance (explicit use replaced); stoppedValue is now a def (unfold instead of rw).
rename	Online/Bandit/ArrayProbSpace.lean	measurable_pi_lambda deprecated -> Measurable.of_eval, but the explicit function argument was dropped: a plain alias rewrite fails to elaborate (10 call sites).
reproof	Online/Bandit/ArrayProbSpace.lean	rw [Measure.fst/snd, map_map] no longer matches across the probSpace/product instance; replaced by exact terms. simp leaves an rfl goal; indepFun rewrite reordered before unfold; convert replaced by an explicit set-equality lemma.
signature change	Online/Bandit/SumRewards.lean, RewardByCountMeasure.lean, Regret/BayesRegretTS.lean	condDistrib_fst_prod and compProd_map_condDistrib second hypothesis added at 5 call sites; simp leaves rfl goals (2).

The diff

diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

index 9d6da91..49b85f5 100644

--- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

+++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

@@ -151,14 +151,14 @@ variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempt

lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]

(h : HasCondDistrib Y X κ μ) :

condDistrib Y X μ =ᵐ[μ.map X] κ := by

- rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq]

+ rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop), h.map_eq]

lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]

(hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)

(h : condDistrib Y X μ =ᵐ[μ.map X] κ) :

HasCondDistrib Y X κ μ where

aemeasurable := by fun_prop

- map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h]

+ map_eq := by rw [← compProd_map_condDistrib hX hY, Measure.compProd_congr h]

lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]

{W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω}

@@ -172,8 +172,9 @@ lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpa

exact hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) hz

have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ

=ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by

- rw [← Measure.compProd_congr (condDistrib_comp Z hW hf),

- compProd_map_condDistrib (hf.comp_aemeasurable hW)]

+ have hZ : AEMeasurable Z μ := hcd.aemeasurable_fst.fst

+ rw [← Measure.compProd_congr (condDistrib_comp hZ hW hf),

+ compProd_map_condDistrib hZ (hf.comp_aemeasurable hW)]

exact hcd.condDistrib_eq

filter_upwards [

condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_fst.fst,

diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean

index 9925b4e..1a0ad7b 100644

--- a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean

+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean

@@ -9,6 +9,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub

public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure

public import Mathlib.Probability.Independence.Basic

public import Mathlib.Probability.Independence.Conditional

+public import Mathlib.Probability.Kernel.CompProdEqIff

/-!

# Lemmas about conditional distributions

@@ -33,22 +34,18 @@ section CondDistrib

variable [IsFiniteMeasure μ]

-lemma map_swap_compProd_map_condDistrib (hY : AEMeasurable Y μ) :

+lemma map_swap_compProd_map_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :

(μ.map X ⊗ₘ condDistrib Y X μ).map Prod.swap = μ.map (fun a ↦ (Y a, X a)) := by

- by_cases hX : AEMeasurable X μ

- · rw [compProd_map_condDistrib hY,

- AEMeasurable.map_map_of_aemeasurable measurable_swap.aemeasurable (hX.prodMk hY)]

- rfl

- · have hYX : ¬ AEMeasurable (fun a ↦ (Y a, X a)) μ :=

- fun h ↦ hX (measurable_snd.comp_aemeasurable h)

- simp [hX, hYX]

+ rw [compProd_map_condDistrib hX hY,

+ AEMeasurable.map_map_of_aemeasurable measurable_swap.aemeasurable (hX.prodMk hY)]

+ rfl

lemma condDistrib_prod_left [StandardBorelSpace β] [Nonempty β]

(hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :

condDistrib (fun ω ↦ (X ω, Y ω)) T μ

=ᵐ[μ.map T] condDistrib X T μ ⊗ₖ condDistrib Y (fun ω ↦ (T ω, X ω)) μ := by

- refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) T (by fun_prop) ?_

- rw [← Measure.compProd_assoc', compProd_map_condDistrib hX, compProd_map_condDistrib hY,

+ refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) hT (by fun_prop) ?_

+ rw [← Measure.compProd_assoc', compProd_map_condDistrib hT hX, compProd_map_condDistrib (hT.prodMk hX) hY,

AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]

rfl

@@ -60,8 +57,8 @@ lemma condDistrib_condDistrib_ae_eq_sectR_condDistrib [StandardBorelSpace β] [N

(condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t := by

filter_upwards [

condDistrib_prod_left (hf.comp_aemeasurable hZ) (hg.comp_aemeasurable hZ) hT,

- condDistrib_comp T hZ (hf.prodMk hg), condDistrib_comp T hZ hf] with t h_prod h_pair h_fst

- rw [condDistrib_ae_eq_iff_measure_eq_compProd f hg.aemeasurable]

+ condDistrib_comp hT hZ (hf.prodMk hg), condDistrib_comp hT hZ hf] with t h_prod h_pair h_fst

+ rw [condDistrib_ae_eq_iff_measure_eq_compProd hf.aemeasurable hg.aemeasurable]

calc (condDistrib Z T μ t).map (fun ω' ↦ (f ω', g ω'))

_ = condDistrib (fun a ↦ ((f ∘ Z) a, (g ∘ Z) a)) T μ t := by

rw [← Kernel.map_apply _ (hf.prodMk hg)]

@@ -75,8 +72,8 @@ lemma condDistrib_prod_self_left [StandardBorelSpace β] [Nonempty β] [Standard

(hX : AEMeasurable X μ) (hT : AEMeasurable T μ) :

condDistrib (fun ω ↦ (X ω, T ω)) T μ =ᵐ[μ.map T] condDistrib X T μ ×ₖ Kernel.id := by

have h_prod := condDistrib_prod_left hX hT hT (μ := μ)

- have h_fst := condDistrib_comp_self (μ := μ) (fun ω ↦ (T ω, X ω)) (f := Prod.fst) (by fun_prop)

- rw [(compProd_map_condDistrib hX).symm] at h_fst

+ have h_fst := condDistrib_comp_self (μ := μ) (hT.prodMk hX) (f := Prod.fst) (by fun_prop)

+ rw [(compProd_map_condDistrib hT hX).symm] at h_fst

have h_fst' := (Measure.ae_compProd_iff (Kernel.measurableSet_eq _ _)).mp h_fst

filter_upwards [h_prod, h_fst'] with z hz1 hz2

rw [hz1]

@@ -104,9 +101,9 @@ lemma CondIndepFun.prod_right [StandardBorelSpace α] [StandardBorelSpace β] [N

(h : X ⟂ᵢ[Z, hZ; μ] Y) :

X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, Z ω)) := by

rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ,

- condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h

+ condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h

rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) hX hZ,

- condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]

+ condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)]

-- Key: condDistrib (Y, Z) Z μ z = (condDistrib Y Z μ z).map (y ↦ (y, z))

have h_cond : condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ =ᵐ[μ.map Z]

fun z ↦ (condDistrib Y Z μ z).map (fun y ↦ (y, z)) := by

@@ -149,14 +146,14 @@ lemma fst_condDistrib_prod [StandardBorelSpace β] [Nonempty β]

lemma condDistrib_of_indepFun (h : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :

condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by

- refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) X hY ?_

+ refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) hX hY ?_

simp only [Measure.compProd_const]

exact (indepFun_iff_map_prod_eq_prod_map_map hX hY).mp h

lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :

IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y) := by

refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩

- rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY,

+ rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hX hY,

Measure.compProd_congr h]

simp

@@ -275,9 +272,9 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight

(h : condDistrib Y (fun ω ↦ (Z ω, X ω)) μ =ᵐ[μ.map (fun ω ↦ (Z ω, X ω))] η.prodMkRight _) :

Y ⟂ᵢ[Z, hZ; μ] X := by

have hη_eq : condDistrib Y Z μ =ᵐ[μ.map Z] η := by

- rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h ⊢

+ rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h ⊢

have h_fst : μ.map Z = (μ.map (fun ω ↦ (Z ω, X ω))).fst := by

- rw [Measure.fst_map_prodMk hX]

+ rw [Measure.fst_map_prodMk hZ hX]

rw [h_fst, ← Measure.map_swap_comprod_eq_fst_compProd, ← h,

Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop),

Measure.fst,

@@ -286,7 +283,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight

symm

rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ]

refine h.trans ?_

- rw [Kernel.prodMkRight_ae_eq_iff, Measure.fst_map_prodMk (by fun_prop)]

+ rw [Kernel.prodMkRight_ae_eq_iff, Measure.fst_map_prodMk (by fun_prop) (by fun_prop)]

exact hη_eq.symm

omit [StandardBorelSpace Ω'] [Nonempty Ω'] in

@@ -297,7 +294,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft

(h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :

Y ⟂ᵢ[Z, hZ; μ] X := by

refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight hX hY hZ ?_ (η := η)

- rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop)] at h ⊢

+ rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop) (by fun_prop)] at h ⊢

have : μ.map (fun a ↦ ((Z a, X a), Y a))

= (μ.map (fun a ↦ ((X a, Z a), Y a))).map (fun p ↦ ((p.1.2, p.1.1), p.2)) := by

rw [Measure.map_map (by fun_prop) (by fun_prop)]

@@ -333,9 +330,9 @@ lemma condIndepFun_fst_prod [StandardBorelSpace α] [StandardBorelSpace β] [Non

rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib (by fun_prop)

(by fun_prop) (by fun_prop)] at h_indep ⊢

have h1 : 𝓛[fun ω ↦ Y ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[Y | Z; μ] :=

- condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop)

+ condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)

have h2 : 𝓛[fun ω ↦ X ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[X | Z; μ] :=

- condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop)

+ condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop) (by fun_prop)

have h_fst1 : (μ.prod ν).map (fun ω ↦ Z ω.1) = μ.map Z := by

conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,

Measure.map_map (by fun_prop) (by fun_prop)]

@@ -417,8 +414,8 @@ lemma ae_eq_of_map_prodMk_eq {β Ω : Type*} {_ : MeasurableSpace β} {_ : Measu

lemma ae_eq_of_condDistrib_eq_deterministic {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)

(hY : AEMeasurable Y μ) (h : condDistrib Y X μ =ᵐ[μ.map X] Kernel.deterministic f hf) :

Y =ᵐ[μ] f ∘ X := by

- have hfX := condDistrib_comp_self (μ := μ) X hf

- rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h hfX

+ have hfX := condDistrib_comp_self (μ := μ) hX hf

+ rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h hfX

exact ae_eq_of_map_prodMk_eq hf hX hY (hfX ▸ h)

end CondDistrib

@@ -432,7 +429,7 @@ lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β]

rw [Filter.EventuallyEq, ae_iff_of_countable]

intro b hb

ext s hs

- rw [condDistrib_apply_of_ne_zero hY,

+ rw [condDistrib_apply_of_ne_zero hX hY,

Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs,

Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs),

cond_apply (hX (measurableSet_singleton _))]

@@ -451,7 +448,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu

(h_cond : ∀ b, μ (Z ⁻¹' {b}) ≠ 0 → condDistrib Y X μ[|Z ⁻¹' {b}] =ᵐ[μ[|Z ⁻¹' {b}].map X]

(κ.comap (fun ω ↦ (ω, b)) (by fun_prop) : Kernel β Ω)) :

condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] κ := by

- refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_

+ refine condDistrib_ae_eq_of_measure_eq_compProd (by fun_prop) (by fun_prop) ?_

ext s hs

suffices ∀ b, (Measure.map (fun x ↦ ((X x, Z x), Y x)) μ) (s ∩ {p | p.1.2 = b}) =

(Measure.map (fun ω ↦ (X ω, Z ω)) μ ⊗ₘ κ) (s ∩ {p | p.1.2 = b}) by

@@ -503,8 +500,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu

exact .inr hb

rw [h_left, h_right]

specialize h_cond b hb

- rw [condDistrib_ae_eq_iff_measure_eq_compProd] at h_cond

- swap; · fun_prop

+ rw [condDistrib_ae_eq_iff_measure_eq_compProd (by fun_prop) (by fun_prop)] at h_cond

rw [Measure.ext_iff] at h_cond

have hs' : MeasurableSet {p : β × Ω | ((p.1, b), p.2) ∈ s} := hs.preimage (by fun_prop)

have h1 := h_cond {p | ((p.1, b), p.2) ∈ s} hs'

diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean

index 80df7df..1bf6bc1 100644

--- a/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean

+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean

@@ -103,7 +103,7 @@ lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f :

lemma iIndepFun_map_iff [IsProbabilityMeasure μ] {X : ι → Ω' → E} {f : Ω → Ω'}

(hf : AEMeasurable f μ) (hX : ∀ n, AEMeasurable (X n) (μ.map f)) :

iIndepFun X (μ.map f) ↔ iIndepFun (fun n ↦ X n ∘ f) μ := by

- have := Measure.isProbabilityMeasure_map hf (μ := μ)

+ have : IsProbabilityMeasure (μ.map f) := inferInstance

rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀' hX,

iIndepFun_iff_map_fun_eq_infinitePi_map₀' (by fun_prop)]

rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]

diff --git a/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean b/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean

index 8471c6f..997bac7 100644

--- a/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean

+++ b/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean

@@ -6,6 +6,7 @@ Authors: Paulo Rauber

module

public import Mathlib.Probability.Kernel.CompProdEqIff

+public import Mathlib.Probability.Kernel.Composition.WithDensity

public import Mathlib.Probability.Kernel.Composition.MeasureComp

/-! # Lemmas about kernels and measures with density

diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean

index 444f290..f434dd6 100644

--- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean

+++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean

@@ -333,7 +333,7 @@ lemma integral_ucb_action_eq_integral_ucb_bestAction (hK : 0 < K)

_ = ∫ ha, uc ha ∂P.map (fun ω ↦ (history A R n ω, A (n + 1) ω)) := by

rw [← integral_map (by fun_prop) (by fun_prop)]

_ = ∫ ha, uc ha ∂P.map (fun ω ↦ (history A R n ω, bestAction κ E ω)) := by

- rw [← compProd_map_condDistrib (by fun_prop), ← compProd_map_condDistrib (by fun_prop),

+ rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop), ← compProd_map_condDistrib (by fun_prop) (by fun_prop),

Measure.compProd_congr (hasCondDistrib_action hK h n).condDistrib_eq]

_ = P[fun ω ↦ ucb A R l u σ2 δ (bestAction κ E ω) (n + 1) ω] := by

rw [integral_map (by fun_prop) (by fun_prop)]

diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean

index 586502c..e0e54d1 100644

--- a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean

+++ b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean

@@ -64,7 +64,8 @@ def TS.initialPolicy (hK : 0 < K) (Q : Measure 𝓔) (κ : Kernel (𝓔 × Fin K

instance {hK : 0 < K} {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × Fin K) ℝ} :

IsProbabilityMeasure (TS.initialPolicy hK Q κ) :=

- Measure.isProbabilityMeasure_map (by fun_prop)

+ have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK

+ inferInstanceAs (IsProbabilityMeasure (Q.map (bestAction κ id)))

/-- The Thompson sampling algorithm with actions in `Fin K`, where `Q : Measure 𝓔` is a prior

distribution over parameters, and `κ : Kernel (𝓔 × Fin K) ℝ` is a Markov kernel that defines the

@@ -112,6 +113,7 @@ lemma TS.hasCondDistrib_action (hK : 0 < K) (h : IsBayesAlgEnvSeq Q κ (tsAlgori

simp_rw [Kernel.map_apply _ hm, IT.bayesTrajMeasurePosterior, hc]

Showing the first 260 of 582 lines. The full diff is the download below.

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup lml      # clone LeanMachineLearning/LML at v4.32.0, bump the Mathlib pin to v4.35.0
python3 bench/lbbench.py build lml      # cache get + lake build; writes the raw errors to bench/runs/lml/v4.35.0/errors.json
git -C bench/work/lml/proj apply ../../../runs/lml/v4.35.0/armA.diff   # replay the recorded repair
python3 bench/lbbench.py build lml --pass replay        # a green replay prints "build rc=0"

Files

Correct this page

Something wrong on this row, or you maintain this project and want it off the benchmark? Correct this row or remove my project.