Skip to content

Commit 830bad0

Browse files
RemyDegenneRemyDegenne
committed
only two indepedence sorry left
1 parent a548ef2 commit 830bad0

3 files changed

Lines changed: 181 additions & 30 deletions

File tree

‎LeanBandits/Bandit/Bandit.lean‎

Lines changed: 41 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne, Paulo Rauber
55
-/
66
import LeanBandits.ForMathlib.CondIndepFun
7+
import LeanBandits.ForMathlib.IndepFun
78
import LeanBandits.ForMathlib.IndepInfinitePi
89
import LeanBandits.ForMathlib.KernelRepresentation
910
import LeanBandits.SequentialLearning.Deterministic
@@ -885,30 +886,6 @@ lemma reward_ae_eq_cond
885886
simp only [hω.2]
886887
simp [hω.1]
887888

888-
lemma indepFun_cond_of_indepFun {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
889-
{mγ : MeasurableSpace γ} {μ : Measure α}
890-
{X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y) {s : Set γ}
891-
(hs : MeasurableSet s) :
892-
X ⟂ᵢ[μ[|Y ⁻¹' s]] Y := by
893-
by_cases h_zero : μ[|Y ⁻¹' s] = 0
894-
· simp only [h_zero]
895-
-- missing simp lemma : `X ⟂ᵢ[0] Y`
896-
simp [indepFun_iff_measure_inter_preimage_eq_mul]
897-
rw [cond_eq_zero] at h_zero
898-
push_neg at h_zero
899-
rw [indepFun_iff_measure_inter_preimage_eq_mul] at hXY ⊢
900-
intro u t hu ht
901-
rw [cond_apply (hs.preimage hY), cond_apply (hs.preimage hY), cond_apply (hs.preimage hY)]
902-
have h_eq : Y ⁻¹' s ∩ (X ⁻¹' u ∩ Y ⁻¹' t) = X ⁻¹' u ∩ Y ⁻¹' (s ∩ t) := by grind
903-
have hsu := hXY u s hu hs
904-
have hust := hXY u (s ∩ t) hu (hs.inter ht)
905-
rw [Set.inter_comm] at hsu
906-
rw [hsu, h_eq, hust]
907-
simp_rw [mul_assoc]
908-
congr 1
909-
rw [← mul_assoc (μ (Y ⁻¹' s)), ENNReal.mul_inv_cancel h_zero.2 h_zero.1, one_mul]
910-
congr
911-
912889
lemma indepFun_todo {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
913890
{mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure α}
914891
{X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y)
@@ -1019,21 +996,55 @@ lemma condIndepFun_reward_hist (alg : Algorithm α R) (ν : Kernel α R) [IsMark
1019996
h_cond.condDistrib_eq
1020997
exact Measurable.prodMk (by fun_prop) (measurable_pullCount_action_add_one alg ν n)
1021998

999+
omit [Countable α] [StandardBorelSpace R] [Nonempty R] in
1000+
lemma measurable_pullCount_action_add_one_hist (alg : Algorithm α R)
1001+
(ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
1002+
Measurable[MeasurableSpace.comap (fun ω ↦ (action alg (n + 1) ω, hist alg ω n)) inferInstance]
1003+
(fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by
1004+
simp_rw [pullCount_eq_sum]
1005+
refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
1006+
refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_fst)
1007+
simp_rw [hist_eq _ _ n]
1008+
unfold action
1009+
refine Measurable.fst (mγ := inferInstance) ?_
1010+
have : (hist alg · i ⟨i, by grind⟩) =
1011+
(fun ω : α × (Iic n → α × R) ↦ ω.2 ⟨i, by grind⟩) ∘
1012+
(fun ω ↦ (action alg (n + 1) ω, fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩)) := rfl
1013+
rw [this]
1014+
exact measurable_comp_comap _ (Measurable.prodMk (by fun_prop) (by fun_prop))
1015+
10221016
lemma hasCondDistrib_reward' (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
10231017
HasCondDistrib (reward alg (n + 1)) (fun ω ↦ (hist alg ω n, action alg (n + 1) ω))
10241018
(ν.prodMkLeft _) (arrayMeasure ν) := by
1025-
let R := reward alg (n + 1)
1019+
let R' := reward alg (n + 1)
10261020
let H := (hist alg · n)
10271021
let A := action alg (n + 1)
10281022
let P := fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω
10291023
have hP : Measurable P := measurable_pullCount_action_add_one alg ν n
1030-
change HasCondDistrib R (fun ω ↦ (H ω, A ω)) (ν.prodMkLeft _) _
1031-
suffices HasCondDistrib R (fun ω ↦ ((A ω, P ω), H ω))
1024+
change HasCondDistrib R' (fun ω ↦ (H ω, A ω)) (ν.prodMkLeft _) _
1025+
suffices HasCondDistrib R' (fun ω ↦ (A ω, H ω)) (ν.prodMkRight _) (arrayMeasure ν) by
1026+
have h_eq : (fun ω ↦ (H ω, A ω)) = MeasurableEquiv.prodComm ∘ (fun ω ↦ (A ω, H ω)) := rfl
1027+
rw [h_eq]
1028+
exact this.comp_right (κ := ν.prodMkRight _) _
1029+
suffices HasCondDistrib R' (fun ω ↦ ((A ω, H ω), P ω))
10321030
((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by
10331031
-- use that `P` is measurable wrt `(A, H)` to drop it from the conditioning
1034-
sorry
1035-
suffices HasCondDistrib R (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by
1036-
have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R :=
1032+
have hP_meas :
1033+
Measurable[MeasurableSpace.comap (fun ω ↦ (A ω, H ω)) inferInstance] P :=
1034+
measurable_pullCount_action_add_one_hist alg ν n
1035+
obtain ⟨f, hf_meas, hf_eq⟩ := hP_meas.exists_eq_measurable_comp
1036+
simp only [hf_eq, Function.comp_apply] at this
1037+
rwa [hasCondDistrib_prod_right_iff _ _ hf_meas] at this
1038+
suffices HasCondDistrib R' (fun ω ↦ ((A ω, P ω), H ω))
1039+
((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by
1040+
let e : ((α × ℕ) × (Iic n → α × R)) ≃ᵐ ((α × (Iic n → α × R)) × ℕ) :=
1041+
{ toFun := fun x ↦ ((x.1.1, x.2), x.1.2)
1042+
invFun := fun x ↦ ((x.1.1, x.2), x.1.2)
1043+
measurable_toFun := by fun_prop
1044+
measurable_invFun := by fun_prop }
1045+
exact this.comp_right e
1046+
suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by
1047+
have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' :=
10371048
(condIndepFun_reward_hist alg ν n).symm
10381049
have h_condDistrib := this.condDistrib_eq
10391050
rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) (by fun_prop)

‎LeanBandits/ForMathlib/HasCondDistrib.lean‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,117 @@ lemma HasCondDistrib.snd {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [Is
6969
rw [Kernel.snd_eq]
7070
exact HasCondDistrib.comp h measurable_snd
7171

72+
lemma HasCondDistrib.comp_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
73+
(f : β ≃ᵐ γ) :
74+
HasCondDistrib Y (f ∘ X) (κ.comap f.symm (by fun_prop)) μ := by
75+
have hY := h.aemeasurable_fst
76+
have hX := h.aemeasurable_snd
77+
refine ⟨h.aemeasurable_fst, by fun_prop, ?_⟩
78+
have h_eq := h.condDistrib_eq
79+
rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢
80+
calc μ.map (fun ω ↦ ((f ∘ X) ω, Y ω))
81+
_ = μ.map ((fun p ↦ (f p.1, p.2)) ∘ fun ω ↦ (X ω, Y ω)) := by congr
82+
_ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ (f p.1, p.2)) := by
83+
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
84+
_ = (μ.map X ⊗ₘ κ).map (fun p ↦ (f p.1, p.2)) := by rw [h_eq]
85+
_ = μ.map (f ∘ X) ⊗ₘ (κ.comap f.symm (by fun_prop)) := by
86+
-- this is probably very inefficient.
87+
have hX_eq : X = f.symm ∘ (f ∘ X) := by ext; simp
88+
conv_lhs => rw [hX_eq]
89+
rw [← AEMeasurable.map_map_of_aemeasurable, Measure.compProd_eq_comp_prod,
90+
← Measure.deterministic_comp_eq_map (f := f.symm), ← Measure.deterministic_comp_eq_map]
91+
rotate_left
92+
· fun_prop
93+
· fun_prop
94+
· fun_prop
95+
· fun_prop
96+
rw [← Kernel.comp_deterministic_eq_comap, Measure.compProd_eq_comp_prod]
97+
simp_rw [Measure.comp_assoc]
98+
congr 1
99+
ext c : 1
100+
rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.comp_apply]
101+
simp only [Kernel.deterministic_apply, Kernel.id_apply, Measure.dirac_bind κ.measurable,
102+
Measure.dirac_bind (Kernel.id ×ₖ κ).measurable, Kernel.prod_apply,
103+
Measure.deterministic_comp_eq_map]
104+
ext s hs
105+
rw [Measure.map_apply (by fun_prop) hs, Measure.prod_apply, Measure.prod_apply,
106+
lintegral_dirac', lintegral_dirac']
107+
· congr
108+
ext
109+
simp
110+
· exact measurable_measure_prodMk_left hs
111+
· exact measurable_measure_prodMk_left (hs.preimage (by fun_prop))
112+
· exact hs
113+
· exact hs.preimage (by fun_prop)
114+
115+
lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
116+
{f : β → γ} (hf : Measurable f) :
117+
HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ := by
118+
have hY := h.aemeasurable_fst
119+
have hX := h.aemeasurable_snd
120+
refine ⟨h.aemeasurable_fst, by fun_prop, ?_⟩
121+
have h_eq := h.condDistrib_eq
122+
rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢
123+
calc μ.map (fun x ↦ ((X x, f (X x)), Y x))
124+
_ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ ((p.1, f p.1), p.2)) := by
125+
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
126+
congr
127+
_ = (μ.map X ⊗ₘ κ).map (fun p ↦ ((p.1, f p.1), p.2)) := by rw [h_eq]
128+
_ = (μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ := by
129+
rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod,
130+
← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)),
131+
← Measure.deterministic_comp_eq_map, Measure.comp_assoc, Measure.comp_assoc]
132+
swap; · fun_prop
133+
swap; · fun_prop
134+
congr 1
135+
ext b : 1
136+
rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.deterministic_apply,
137+
Kernel.id_apply, Measure.dirac_bind (Kernel.measurable _), Kernel.prod_apply,
138+
Measure.deterministic_comp_eq_map, Kernel.prodMkRight_apply, Kernel.id_apply]
139+
change Measure.map (Prod.map (fun x ↦ (x, f x)) id) ((Measure.dirac b).prod (κ b)) =
140+
(Measure.dirac (b, f b)).prod (κ b)
141+
rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
142+
Measure.map_dirac (by fun_prop)]
143+
_ = μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ := by
144+
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
145+
congr
146+
147+
lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X : α → β) (Y : α → Ω)
148+
{f : β → γ} (hf : Measurable f) :
149+
HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ ↔ HasCondDistrib Y X κ μ := by
150+
refine ⟨fun h ↦ ?_, fun h ↦ h.prod_right hf⟩
151+
have hX : AEMeasurable X μ := by
152+
have := h.aemeasurable_snd
153+
have h_eq : X = (fun p ↦ p.1) ∘ (fun a ↦ (X a, f (X a))) := by ext; simp
154+
rw [h_eq]
155+
exact Measurable.comp_aemeasurable (by fun_prop) (by fun_prop)
156+
have hY := h.aemeasurable_fst
157+
refine ⟨by fun_prop, by fun_prop, ?_⟩
158+
have h_eq := h.condDistrib_eq
159+
rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢
160+
calc μ.map (fun x ↦ (X x, Y x))
161+
_ = (μ.map (fun ω ↦ ((X ω, f (X ω)), Y ω))).map (fun p ↦ (p.1.1, p.2)) := by
162+
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
163+
congr
164+
_ = (μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by rw [h_eq]
165+
_ = ((μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by
166+
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
167+
congr
168+
_ = μ.map X ⊗ₘ κ := by
169+
simp_rw [Measure.compProd_eq_comp_prod,
170+
← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)) (by fun_prop),
171+
← Measure.deterministic_comp_eq_map (f := fun p : (β × γ) × Ω ↦ (p.1.1, p.2)) (by fun_prop),
172+
Measure.comp_assoc]
173+
congr 1
174+
ext b : 1
175+
rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply,
176+
Kernel.deterministic_apply, Measure.dirac_bind (Kernel.measurable _),
177+
Kernel.prod_apply, Measure.deterministic_comp_eq_map, Kernel.prodMkRight_apply,
178+
Kernel.id_apply]
179+
change Measure.map (Prod.map (fun x ↦ x.1) id) ((Measure.dirac (b, f b)).prod (κ b)) = _
180+
rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
181+
Measure.map_dirac (by fun_prop)]
182+
72183
lemma HasLaw.prod_of_hasCondDistrib {P : Measure β} [IsFiniteMeasure μ] [IsSFiniteKernel κ]
73184
(h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
74185
HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ := by

‎LeanBandits/ForMathlib/IndepFun.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,35 @@ variable {α Ω Ω' E ι : Type*} [Countable ι] {mα : MeasurableSpace α}
99
{mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
1010
{mE : MeasurableSpace E} {μ ν : Measure Ω}
1111

12+
@[simp]
13+
lemma indepFun_zero_measure {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
14+
{mγ : MeasurableSpace γ} (X : α → β) (Y : α → γ) :
15+
X ⟂ᵢ[(0 : Measure α)] Y := by
16+
simp [indepFun_iff_measure_inter_preimage_eq_mul]
17+
18+
lemma indepFun_cond_of_indepFun {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
19+
{mγ : MeasurableSpace γ} {μ : Measure α}
20+
{X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y) {s : Set γ}
21+
(hs : MeasurableSet s) :
22+
X ⟂ᵢ[μ[|Y ⁻¹' s]] Y := by
23+
by_cases h_zero : μ[|Y ⁻¹' s] = 0
24+
· simp [h_zero]
25+
rw [cond_eq_zero] at h_zero
26+
push_neg at h_zero -- `h_zero : μ (Y ⁻¹' s) ≠ ⊤ ∧ μ (Y ⁻¹' s) ≠ 0`
27+
rw [indepFun_iff_measure_inter_preimage_eq_mul] at hXY ⊢
28+
intro u t hu ht
29+
rw [cond_apply (hs.preimage hY), cond_apply (hs.preimage hY), cond_apply (hs.preimage hY)]
30+
have h_eq : Y ⁻¹' s ∩ (X ⁻¹' u ∩ Y ⁻¹' t) = X ⁻¹' u ∩ Y ⁻¹' (s ∩ t) := by grind
31+
have hsu : μ (X ⁻¹' u ∩ Y ⁻¹' s) = μ (X ⁻¹' u) * μ (Y ⁻¹' s) := hXY u s hu hs
32+
rw [Set.inter_comm] at hsu
33+
have hust : μ (X ⁻¹' u ∩ Y ⁻¹' (s ∩ t)) = μ (X ⁻¹' u) * μ (Y ⁻¹' (s ∩ t)) :=
34+
hXY u (s ∩ t) hu (hs.inter ht)
35+
rw [hsu, h_eq, hust]
36+
simp_rw [mul_assoc]
37+
congr 1
38+
rw [← mul_assoc (μ (Y ⁻¹' s)), ENNReal.mul_inv_cancel h_zero.2 h_zero.1, one_mul]
39+
congr
40+
1241
lemma iIndepFun_nat_iff_forall_indepFun [IsProbabilityMeasure μ] {X : ℕ → Ω → E}
1342
(hX : ∀ n, AEMeasurable (X n) μ) :
1443
iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by

0 commit comments

Comments
 (0)