Skip to content

CI fix #47

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 3 commits into from
Dec 29, 2025
Merged

CI fix #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
dd1df07
CI fix
RemyDegenne Dec 29, 2025
2fd1f07
add lintDriver
RemyDegenne Dec 29, 2025
a8d6476
manifest update
RemyDegenne Dec 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 21 additions & 10 deletions .github/workflows/blueprint.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,24 +25,35 @@ jobs:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Cleanup to free disk space
uses: jlumbroso/free-disk-space@main
with:
# this might remove tools that are actually needed,
# if set to "true" but frees about 6 GB
tool-cache: false
# all of these default to true, but feel free to set to
# "false" if necessary for your workflow
android: true
dotnet: false
haskell: false
large-packages: false
docker-images: false
swap-storage: false

- name: Checkout project
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
with:
fetch-depth: 0 # Fetch all history for all branches and tags

- name: Build the project
uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
- name: Build and lint project
uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # 2025-07-02
with:
use-github-cache: false

- name: check that LeanBandits.lean is up to date
run: ~/.elan/bin/lake exe mk_all --check

- name: Lint project
run: env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter LeanBandits
build: true
lint: true
mk_all-check: true

- name: Compile blueprint and documentation
uses: leanprover-community/docgen-action@1417dc7f90338c875da5e5870c03a287d8348896 # docgen-action#11
uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
with:
blueprint: true
homepage: home_page
3 changes: 2 additions & 1 deletion LeanBandits/ForMathlib/CondDistrib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,8 @@ lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
X ⟂ᵢ[Z, hZ; μ] Y :=
Kernel.IndepFun.of_prod_left h

lemma CondIndepFun.prod_right [StandardBorelSpace α] [IsFiniteMeasure μ]
lemma CondIndepFun.prod_right [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
[StandardBorelSpace γ] [Nonempty γ] [StandardBorelSpace δ] [Nonempty δ] [IsFiniteMeasure μ]
{X : α → β} {Y : α → γ} {Z : α → δ}
(hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
(h : X ⟂ᵢ[Z, hZ; μ] Y) :
Expand Down
122 changes: 52 additions & 70 deletions LeanBandits/RewardByCountMeasure.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,34 +117,34 @@ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s
/-- Law of `Y` conditioned on the event that `X` equals `x`. -/
notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}])

local notation "𝔓t" => Bandit.trajMeasure alg ν
local notation "𝔓" => Bandit.measure alg ν

omit [DecidableEq α] [MeasurableSingletonClass α] in
lemma condDistrib_reward'' [StandardBorelSpace α] [Nonempty α] (n : ℕ) :
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν]
=ᵐ[(Bandit.measure alg ν).map (fun ω ↦ arm n ω.1)] ν := by
let μ := Bandit.measure alg ν
have h_ra' : 𝓛[reward n | arm n; Bandit.trajMeasure alg ν]
=ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := condDistrib_reward alg ν n
have h_law : μ.map (fun ω ↦ arm n ω.1) = (Bandit.trajMeasure alg ν).map (arm n) := by
calc μ.map (fun ω ↦ arm n ω.1)
_ = (μ.map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓]
=ᵐ[(𝔓).map (fun ω ↦ arm n ω.1)] ν := by
have h_ra' : 𝓛[reward n | arm n; 𝔓t] =ᵐ[(𝔓t).map (arm n)] ν := condDistrib_reward alg ν n
have h_law : (𝔓).map (fun ω ↦ arm n ω.1) = (𝔓t).map (arm n) := by
calc (𝔓).map (fun ω ↦ arm n ω.1)
_ = ((𝔓).map (fun ω ↦ ω.1)).map (fun ω ↦ arm n ω) := by
rw [Measure.map_map (by fun_prop) (by fun_prop)]
rfl
_ = _ := by unfold μ Bandit.measure; simp [Measure.map_fst_prod]
_ = _ := by unfold Bandit.measure; simp [Measure.map_fst_prod]
rw [h_law]
have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ]
=ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] 𝓛[reward n | arm n; Bandit.trajMeasure alg ν] :=
have h_prod : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓]
=ᵐ[(𝔓t).map (arm n)] 𝓛[reward n | arm n; 𝔓t] :=
condDistrib_fst_prod _ (by fun_prop) _
filter_upwards [h_ra', h_prod] with ω h_eq h_prod
rw [h_prod, h_eq]

omit [DecidableEq α] in
lemma reward_cond_arm [StandardBorelSpace α] [Nonempty α] [Countable α] (a : α) (n : ℕ)
(hμa : (Bandit.measure alg ν).map (fun ω ↦ arm n ω.1) {a} ≠ 0) :
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by
let μ := Bandit.measure alg ν
have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν :=
(hμa : (𝔓).map (fun ω ↦ arm n ω.1) {a} ≠ 0) :
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; 𝔓] = ν a := by
have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ arm n ω.1)] ν :=
condDistrib_reward'' n
have h_eq := condDistrib_ae_eq_cond (μ := μ)
have h_eq := condDistrib_ae_eq_cond (μ := 𝔓)
(X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop)
rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq
specialize h_ra a hμa
Expand Down Expand Up @@ -194,9 +194,7 @@ lemma measurableSet_stepsUntil_eq (a : α) (m n : ℕ) :

lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α] [Nonempty α]
(a : α) (m n : ℕ) (hm : m ≠ 0) :
CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le
(reward n) ({ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1))
(Bandit.trajMeasure alg ν) := by
reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] {ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1) := by
-- the indicator of `stepsUntil ... = n` is a function of
-- `hist (n-1)` and `arm n`.
-- It thus suffices to prove the independence of `reward n` and `hist (n-1)` conditionally
Expand All @@ -207,20 +205,18 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
by_cases hm1 : m = 1
· simp only [hm1, true_and]
have h_indep := condIndepFun_self_right (X := reward 0) (Z := arm 0)
(mβ := inferInstance) (mβ' := inferInstance) (μ := Bandit.trajMeasure alg ν)
(mβ := inferInstance) (mβ' := inferInstance) (μ := 𝔓t)
(by fun_prop) (by fun_prop)
have : {ω : ℕ → α × ℝ | arm 0 ω = a}.indicator (fun x ↦ 1)
= {b | b = a}.indicator (fun _ ↦ 1) ∘ arm 0 := by ext; simp [Set.indicator]
rw [this]
exact h_indep.comp measurable_id (by fun_prop)
· simp only [hm1, false_and, Set.setOf_false, Set.indicator_empty]
exact condIndepFun_const_right (reward 0) 0
have h_indep : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n)
(hist (n - 1)) (Bandit.trajMeasure alg ν) := by
have h_indep : reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] hist (n - 1) := by
convert condIndepFun_reward_hist_arm (alg := alg) (ν := ν) (n - 1)
<;> rw [Nat.sub_add_cancel (by grind)]
have h_indep' : CondIndepFun (mα.comap (arm n)) (measurable_arm n).comap_le (reward n)
(fun ω ↦ (hist (n - 1) ω, arm n ω)) (Bandit.trajMeasure alg ν) :=
have h_indep' : reward n ⟂ᵢ[arm n, measurable_arm n; 𝔓t] fun ω ↦ (hist (n - 1) ω, arm n ω) :=
h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop)
obtain ⟨φ, hφ_meas, h_eq⟩ : ∃ φ : ((Iic (n - 1) → α × ℝ) × α) → ℕ, Measurable φ ∧
{ω | stepsUntil a m ω = ↑n}.indicator (fun _ ↦ 1) = φ ∘ (fun ω ↦ (hist (n - 1) ω, arm n ω)) :=
Expand All @@ -231,44 +227,41 @@ lemma condIndepFun_reward_stepsUntil_arm' [StandardBorelSpace α] [Countable α]
lemma condIndepFun_reward_stepsUntil_arm [StandardBorelSpace α] [Countable α] [Nonempty α]
(a : α) (m n : ℕ) (hm : m ≠ 0) :
CondIndepFun (mα.comap (fun ω ↦ arm n ω.1)) ((measurable_arm n).comp measurable_fst).comap_le
(fun ω ↦ reward n ω.1) ({ω | stepsUntil a m ω.1 = ↑n}.indicator (fun _ ↦ 1))
(Bandit.measure alg ν) :=
(fun ω ↦ reward n ω.1) ({ω | stepsUntil a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓 :=
condIndepFun_fst_prod (ν := Bandit.streamMeasure ν)
(measurable_indicator_stepsUntil_eq a m n) (by fun_prop) (by fun_prop)
(condIndepFun_reward_stepsUntil_arm' a m n hm)

lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α] (a : α) (m n : ℕ)
(hm : m ≠ 0)
(hμn : (Bandit.measure alg ν) ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n}) ≠ 0) :
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← ↑n; Bandit.measure alg ν] = ν a := by
let μ := Bandit.measure alg ν
(hm : m ≠ 0) (hμn : 𝔓 ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n}) ≠ 0) :
𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← ↑n; 𝔓] = ν a := by
have hμna :
μ ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) ≠ 0 := by
𝔓 ((fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}) ≠ 0 := by
suffices ((fun ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) ↦
stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a})
= (fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} by simpa [this] using hμn
ext ω
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, and_iff_left_iff_imp]
exact arm_eq_of_stepsUntil_eq_coe hm
have hμa : μ.map (fun ω ↦ arm n ω.1) {a} ≠ 0 := by
have hμa : (𝔓).map (fun ω ↦ arm n ω.1) {a} ≠ 0 := by
rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)]
refine fun h_zero ↦ hμn (measure_mono_null (fun ω ↦ ?_) h_zero)
simp only [Set.mem_preimage, Set.mem_singleton_iff]
exact arm_eq_of_stepsUntil_eq_coe hm
calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← (n : ℕ∞); μ]
_ = (μ[|(fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map
calc 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ stepsUntil a m ω.1 ← (n : ℕ∞); 𝔓]
_ = (𝔓[|(fun ω ↦ stepsUntil a m ω.1) ⁻¹' {↑n} ∩ (fun ω ↦ arm n ω.1) ⁻¹' {a}]).map
(fun ω ↦ reward n ω.1) := by
congr with ω
simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_inter_iff, iff_self_and]
exact arm_eq_of_stepsUntil_eq_coe hm
_ = (μ[|(fun ω ↦ arm n ω.1) ⁻¹' {a}
_ = (𝔓[|(fun ω ↦ arm n ω.1) ⁻¹' {a}
∩ {ω : (ℕ → α × ℝ) × (ℕ → α → ℝ) | stepsUntil a m ω.1 = ↑n}.indicator 1 ⁻¹' {1} ]).map
(fun ω ↦ reward n ω.1) := by
congr 2 with ω
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.indicator_apply,
Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
rw [and_comm]
_ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; μ] := by
_ = 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; 𝔓] := by
rw [cond_of_condIndepFun (by fun_prop)]
· exact condIndepFun_reward_stepsUntil_arm a m n hm
· refine measurable_one.indicator ?_
Expand All @@ -282,11 +275,9 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α

lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) (m : ℕ) (hm : m ≠ 0) :
condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
(Bandit.measure alg ν)
=ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)] Kernel.const _ (ν a) := by
let μ := Bandit.measure alg ν
refine (condDistrib_ae_eq_cond (μ := μ)
condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓
=ᵐ[(𝔓).map (fun ω ↦ stepsUntil a m ω.1)] Kernel.const _ (ν a) := by
refine (condDistrib_ae_eq_cond (μ := 𝔓)
(X := fun ω ↦ stepsUntil a m ω.1) (by fun_prop) (by fun_prop)).trans ?_
rw [Filter.EventuallyEq, ae_iff_of_countable]
intro n hn
Expand Down Expand Up @@ -315,51 +306,45 @@ lemma condDistrib_rewardByCount_stepsUntil [Countable α] [StandardBorelSpace α
/-- The reward received at the `m`-th pull of arm `a` has law `ν a`. -/
lemma hasLaw_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) (m : ℕ) (hm : m ≠ 0) :
HasLaw (rewardByCount a m) (ν a) (Bandit.measure alg ν) where
HasLaw (rewardByCount a m) (ν a) 𝔓 where
map_eq := by
have h_condDistrib :
condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
(Bandit.measure alg ν)
=ᵐ[(Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)]
condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓
=ᵐ[(𝔓).map (fun ω ↦ stepsUntil a m ω.1)]
Kernel.const _ (ν a) := condDistrib_rewardByCount_stepsUntil a m hm
calc (Bandit.measure alg ν).map (rewardByCount a m)
_ = (condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1)
(Bandit.measure alg ν))
∘ₘ ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) := by
calc (𝔓).map (rewardByCount a m)
_ = (condDistrib (rewardByCount a m) (fun ω ↦ stepsUntil a m ω.1) 𝔓)
∘ₘ ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) := by
rw [condDistrib_comp_map (by fun_prop) (by fun_prop)]
_ = (Kernel.const _ (ν a))
∘ₘ ((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) :=
_ = (Kernel.const _ (ν a)) ∘ₘ ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) :=
Measure.comp_congr h_condDistrib
_ = ν a := by
have : IsProbabilityMeasure
((Bandit.measure alg ν).map (fun ω ↦ stepsUntil a m ω.1)) :=
have : IsProbabilityMeasure ((𝔓).map (fun ω ↦ stepsUntil a m ω.1)) :=
Measure.isProbabilityMeasure_map (by fun_prop)
simp

lemma identDistrib_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempty α] (a : α) (n m : ℕ)
(hn : n ≠ 0) (hm : m ≠ 0) :
IdentDistrib (rewardByCount a n) (rewardByCount a m)
(Bandit.measure alg ν) (Bandit.measure alg ν) where
IdentDistrib (rewardByCount a n) (rewardByCount a m) 𝔓 𝔓 where
aemeasurable_fst := by fun_prop
aemeasurable_snd := by fun_prop
map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, (hasLaw_rewardByCount a m hm).map_eq]

lemma identDistrib_rewardByCount_id [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) (n : ℕ) (hn : n ≠ 0) :
IdentDistrib (rewardByCount a n) id (Bandit.measure alg ν) (ν a) where
IdentDistrib (rewardByCount a n) id 𝔓 (ν a) where
aemeasurable_fst := by fun_prop
aemeasurable_snd := Measurable.aemeasurable <| by fun_prop
map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, Measure.map_id]

lemma identDistrib_rewardByCount_eval [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) (n m : ℕ) (hn : n ≠ 0) :
IdentDistrib (rewardByCount a n) (fun ω ↦ ω m a)
(Bandit.measure alg ν) (Bandit.streamMeasure ν) :=
IdentDistrib (rewardByCount a n) (fun ω ↦ ω m a) 𝔓 (Bandit.streamMeasure ν) :=
(identDistrib_rewardByCount_id a n hn).trans (identDistrib_eval_eval_id_streamMeasure ν m a).symm

lemma indepFun_rewardByCount_Iic (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] (a : α)
(n : ℕ) :
(rewardByCount a (n + 1)) ⟂ᵢ[Bandit.measure alg ν] fun ω (i : Iic n) ↦ rewardByCount a i ω := by
(rewardByCount a (n + 1)) ⟂ᵢ[𝔓] fun ω (i : Iic n) ↦ rewardByCount a i ω := by
sorry

lemma iIndepFun_rewardByCount' (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] (a : α) :
Expand All @@ -368,13 +353,13 @@ lemma iIndepFun_rewardByCount' (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [Is
exact indepFun_rewardByCount_Iic alg ν a

lemma iIndepFun_rewardByCount (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] :
iIndepFun (fun (p : α × ℕ) ↦ rewardByCount p.1 p.2) (Bandit.measure alg ν) := by
iIndepFun (fun (p : α × ℕ) ↦ rewardByCount p.1 p.2) 𝔓 := by
sorry

lemma identDistrib_rewardByCount_stream' [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) :
IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω n a)
(Bandit.measure alg ν) (Bandit.streamMeasure ν) := by
𝔓 (Bandit.streamMeasure ν) := by
refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
· refine identDistrib_rewardByCount_eval a (n + 1) n (by simp) (ν := ν)
· have h_indep := iIndepFun_rewardByCount' alg ν a
Expand All @@ -384,35 +369,32 @@ lemma identDistrib_rewardByCount_stream' [Countable α] [StandardBorelSpace α]
omit [DecidableEq α] [MeasurableSingletonClass α] in
lemma identDistrib_eval_streamMeasure_measure (a : α) :
IdentDistrib (fun ω n ↦ ω n a) (fun ω n ↦ ω.2 n a)
(Bandit.streamMeasure ν) (Bandit.measure alg ν) := by
(Bandit.streamMeasure ν) 𝔓 := by
refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_
· rw [← Bandit.snd_measure alg ν, Measure.snd,
identDistrib_map_left_iff (by fun_prop) (by fun_prop)
(Measurable.aemeasurable <| by fun_prop)]
exact IdentDistrib.refl (by fun_prop)
· exact iIndepFun_eval_streamMeasure'' ν a
· change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) (Bandit.measure alg ν)
· change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) 𝔓
rw [← iIndepFun_map_iff (by fun_prop) (fun _ ↦ Measurable.aemeasurable (by fun_prop))]
rw [← Measure.snd, Bandit.snd_measure]
exact iIndepFun_eval_streamMeasure'' ν a

lemma identDistrib_rewardByCount_stream [Countable α] [StandardBorelSpace α] [Nonempty α]
(a : α) :
IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω.2 n a)
(Bandit.measure alg ν) (Bandit.measure alg ν) :=
IdentDistrib (fun ω n ↦ rewardByCount a (n + 1) ω) (fun ω n ↦ ω.2 n a) 𝔓 𝔓 :=
(identDistrib_rewardByCount_stream' a).trans (identDistrib_eval_streamMeasure_measure a)

lemma indepFun_rewardByCount_of_ne {a b : α} (hab : a ≠ b) :
IndepFun (fun ω s ↦ rewardByCount a s ω) (fun ω s ↦ rewardByCount b s ω)
(Bandit.measure alg ν) := by
IndepFun (fun ω s ↦ rewardByCount a s ω) (fun ω s ↦ rewardByCount b s ω) 𝔓 := by
sorry

lemma identDistrib_sum_Icc_rewardByCount [Nonempty α] [Countable α] (m : ℕ) (a : α) :
IdentDistrib (fun ω ↦ ∑ s ∈ Icc 1 m, rewardByCount a s ω)
(fun ω ↦ ∑ s ∈ range m, ω.2 s a) (Bandit.measure alg ν) (Bandit.measure alg ν) := by
(fun ω ↦ ∑ s ∈ range m, ω.2 s a) 𝔓 𝔓 := by
have h1 (a : α) :
IdentDistrib (fun ω s ↦ rewardByCount a (s + 1) ω) (fun ω s ↦ ω.2 s a)
(Bandit.measure alg ν) (Bandit.measure alg ν) :=
IdentDistrib (fun ω s ↦ rewardByCount a (s + 1) ω) (fun ω s ↦ ω.2 s a) 𝔓 𝔓 :=
identDistrib_rewardByCount_stream a
have h_eq (ω : (ℕ → α × ℝ) × (ℕ → α → ℝ)) : ∑ s ∈ Icc 1 m, rewardByCount a s ω
= ∑ s ∈ range m, rewardByCount a (s + 1) ω := by
Expand Down
Loading