From d16a55dfae157764020ff6f7c84b0907707ab3a8 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Fri, 12 Dec 2025 15:03:43 +0000 Subject: [PATCH 1/5] Prove indepFun_proj_infinitePi_infinitePi --- LeanBandits/Bandit/Bandit.lean | 6 ++-- LeanBandits/ForMathlib/IndepInfinitePi.lean | 37 +++++++++++++++++++++ 2 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 LeanBandits/ForMathlib/IndepInfinitePi.lean diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index 9192439b..0b88c9bc 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne, Paulo Rauber -/ import LeanBandits.SequentialLearning.Deterministic +import LeanBandits.ForMathlib.IndepInfinitePi import Mathlib.Probability.IdentDistrib -import Mathlib.Probability.Independence.InfinitePi /-! # Bandit @@ -143,8 +143,8 @@ lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : exact (iIndepFun_eval_streamMeasure ν).indepFun (by grind) lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : - IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := by - sorry + IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := + indepFun_proj_infinitePi_infinitePi h lemma indepFun_eval_snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : diff --git a/LeanBandits/ForMathlib/IndepInfinitePi.lean b/LeanBandits/ForMathlib/IndepInfinitePi.lean new file mode 100644 index 00000000..2d934046 --- /dev/null +++ b/LeanBandits/ForMathlib/IndepInfinitePi.lean @@ -0,0 +1,37 @@ +import Mathlib.Probability.Independence.InfinitePi + +open MeasureTheory Measure ProbabilityTheory Set + +namespace MeasurableSpace + +variable {δ : Type*} {X : δ → Type*} [m : ∀ a, MeasurableSpace (X a)] {α : Type*} + +-- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean after MeasurableSpace.pi +theorem comap_pi {g : α → ∀ a, X a} : + MeasurableSpace.comap g MeasurableSpace.pi = + ⨆ a, MeasurableSpace.comap (fun x ↦ g x a) (m a) := by + simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp] + rfl + +end MeasurableSpace + +namespace ProbabilityTheory + +variable {ι κ : Type*} {𝓧 : Type*} [MeasurableSpace 𝓧] + {μ : ι → κ → Measure 𝓧} [∀ i j, IsProbabilityMeasure (μ i j)] + +-- Mathlib/Probability/Independence/InfinitePi.lean after iIndepFun_uncurry_infinitePi' +lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (hab : a ≠ b) : + IndepFun (fun (ω : ι → κ → 𝓧) i ↦ ω i a) + (fun (ω : ι → κ → 𝓧) i ↦ ω i b) + (infinitePi (fun i ↦ infinitePi (μ i))) := by + have hi : iIndepFun (fun (p : ι × κ) (ω : ι → κ → 𝓧) ↦ ω p.1 p.2) + (infinitePi (fun i ↦ infinitePi (μ i))) := + iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) μ (by fun_prop) + have hd : Disjoint (range fun i : ι ↦ (i, a)) (range fun i : ι ↦ (i, b)) := by + simp [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, hab.symm] + simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi] + convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) hi hd + all_goals rw [iSup_range] + +end ProbabilityTheory From 8a19adc967a12209729005f6b954eeff9ffa2587 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Fri, 12 Dec 2025 17:11:45 +0000 Subject: [PATCH 2/5] Refactor --- LeanBandits/Bandit/Bandit.lean | 2 +- LeanBandits/ForMathlib/IndepInfinitePi.lean | 34 ++++++++++++--------- 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index 0b88c9bc..2a4c1f3a 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -144,7 +144,7 @@ lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := - indepFun_proj_infinitePi_infinitePi h + indepFun_proj_infinitePi_infinitePi (μ := fun _ ↦ ν) h lemma indepFun_eval_snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : diff --git a/LeanBandits/ForMathlib/IndepInfinitePi.lean b/LeanBandits/ForMathlib/IndepInfinitePi.lean index 2d934046..3974bf14 100644 --- a/LeanBandits/ForMathlib/IndepInfinitePi.lean +++ b/LeanBandits/ForMathlib/IndepInfinitePi.lean @@ -6,7 +6,7 @@ namespace MeasurableSpace variable {δ : Type*} {X : δ → Type*} [m : ∀ a, MeasurableSpace (X a)] {α : Type*} --- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean after MeasurableSpace.pi +-- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean theorem comap_pi {g : α → ∀ a, X a} : MeasurableSpace.comap g MeasurableSpace.pi = ⨆ a, MeasurableSpace.comap (fun x ↦ g x a) (m a) := by @@ -17,21 +17,25 @@ end MeasurableSpace namespace ProbabilityTheory -variable {ι κ : Type*} {𝓧 : Type*} [MeasurableSpace 𝓧] - {μ : ι → κ → Measure 𝓧} [∀ i j, IsProbabilityMeasure (μ i j)] - --- Mathlib/Probability/Independence/InfinitePi.lean after iIndepFun_uncurry_infinitePi' -lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (hab : a ≠ b) : - IndepFun (fun (ω : ι → κ → 𝓧) i ↦ ω i a) - (fun (ω : ι → κ → 𝓧) i ↦ ω i b) - (infinitePi (fun i ↦ infinitePi (μ i))) := by - have hi : iIndepFun (fun (p : ι × κ) (ω : ι → κ → 𝓧) ↦ ω p.1 p.2) - (infinitePi (fun i ↦ infinitePi (μ i))) := - iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) μ (by fun_prop) - have hd : Disjoint (range fun i : ι ↦ (i, a)) (range fun i : ι ↦ (i, b)) := by - simp [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, hab.symm] +variable {ι κ : Type*} {𝓧 : ι → κ → Type*} [m𝓧 : ∀ i j, MeasurableSpace (𝓧 i j)] + {μ : (i : ι) → (j : κ) → Measure (𝓧 i j)} [∀ i j, IsProbabilityMeasure (μ i j)] + +-- Mathlib/Probability/Independence/InfinitePi.lean +lemma indep_iSup_infinitePi_infinitePi {S T : Set (ι × κ)} (hd : Disjoint S T) : + Indep (⨆ p ∈ S, MeasurableSpace.comap (fun ω ↦ ω p.1 p.2) (m𝓧 p.1 p.2)) + (⨆ p ∈ T, MeasurableSpace.comap (fun ω ↦ ω p.1 p.2) (m𝓧 p.1 p.2)) + (infinitePi (fun i ↦ infinitePi (μ i))) := + indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) + (iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) μ (by fun_prop)) hd + +-- Mathlib/Probability/Independence/InfinitePi.lean +lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) : + IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) + (infinitePi (fun i ↦ infinitePi (μ i))) := by + have hd : Disjoint (Set.range fun i : ι ↦ (i, a)) (Set.range fun i ↦ (i, b)) := by + simp [Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem, h.symm] simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi] - convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) hi hd + convert indep_iSup_infinitePi_infinitePi (μ := μ) hd all_goals rw [iSup_range] end ProbabilityTheory From a3c9cbdbe4bdc17d3ab5031537c75412e458c970 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Sat, 13 Dec 2025 09:21:33 +0000 Subject: [PATCH 3/5] Remove lemma --- LeanBandits/ForMathlib/IndepInfinitePi.lean | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/LeanBandits/ForMathlib/IndepInfinitePi.lean b/LeanBandits/ForMathlib/IndepInfinitePi.lean index 3974bf14..f801c6ae 100644 --- a/LeanBandits/ForMathlib/IndepInfinitePi.lean +++ b/LeanBandits/ForMathlib/IndepInfinitePi.lean @@ -20,14 +20,6 @@ namespace ProbabilityTheory variable {ι κ : Type*} {𝓧 : ι → κ → Type*} [m𝓧 : ∀ i j, MeasurableSpace (𝓧 i j)] {μ : (i : ι) → (j : κ) → Measure (𝓧 i j)} [∀ i j, IsProbabilityMeasure (μ i j)] --- Mathlib/Probability/Independence/InfinitePi.lean -lemma indep_iSup_infinitePi_infinitePi {S T : Set (ι × κ)} (hd : Disjoint S T) : - Indep (⨆ p ∈ S, MeasurableSpace.comap (fun ω ↦ ω p.1 p.2) (m𝓧 p.1 p.2)) - (⨆ p ∈ T, MeasurableSpace.comap (fun ω ↦ ω p.1 p.2) (m𝓧 p.1 p.2)) - (infinitePi (fun i ↦ infinitePi (μ i))) := - indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) - (iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) μ (by fun_prop)) hd - -- Mathlib/Probability/Independence/InfinitePi.lean lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) : IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) @@ -35,7 +27,8 @@ lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) : have hd : Disjoint (Set.range fun i : ι ↦ (i, a)) (Set.range fun i ↦ (i, b)) := by simp [Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem, h.symm] simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi] - convert indep_iSup_infinitePi_infinitePi (μ := μ) hd - all_goals rw [iSup_range] + convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) + (iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (μ := μ) (by fun_prop)) hd + all_goals simp_rw [iSup_range, id_eq] end ProbabilityTheory From 7ffe863fdeefcebe1edb715be9cc8115662a980f Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 15 Dec 2025 10:18:29 +0000 Subject: [PATCH 4/5] Improve proofs --- LeanBandits/Bandit/Bandit.lean | 2 +- LeanBandits/ForMathlib/IndepInfinitePi.lean | 20 ++++++++------------ 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index 2a4c1f3a..0b88c9bc 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -144,7 +144,7 @@ lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := - indepFun_proj_infinitePi_infinitePi (μ := fun _ ↦ ν) h + indepFun_proj_infinitePi_infinitePi h lemma indepFun_eval_snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : diff --git a/LeanBandits/ForMathlib/IndepInfinitePi.lean b/LeanBandits/ForMathlib/IndepInfinitePi.lean index f801c6ae..b18bd4ba 100644 --- a/LeanBandits/ForMathlib/IndepInfinitePi.lean +++ b/LeanBandits/ForMathlib/IndepInfinitePi.lean @@ -1,17 +1,14 @@ import Mathlib.Probability.Independence.InfinitePi -open MeasureTheory Measure ProbabilityTheory Set +open MeasureTheory Measure ProbabilityTheory Set Function namespace MeasurableSpace variable {δ : Type*} {X : δ → Type*} [m : ∀ a, MeasurableSpace (X a)] {α : Type*} -- Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean -theorem comap_pi {g : α → ∀ a, X a} : - MeasurableSpace.comap g MeasurableSpace.pi = - ⨆ a, MeasurableSpace.comap (fun x ↦ g x a) (m a) := by - simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp] - rfl +theorem comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a) := by + simp_rw [pi, comap_iSup, comap_comp, comp_def] end MeasurableSpace @@ -22,13 +19,12 @@ variable {ι κ : Type*} {𝓧 : ι → κ → Type*} [m𝓧 : ∀ i j, Measurab -- Mathlib/Probability/Independence/InfinitePi.lean lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) : - IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) - (infinitePi (fun i ↦ infinitePi (μ i))) := by - have hd : Disjoint (Set.range fun i : ι ↦ (i, a)) (Set.range fun i ↦ (i, b)) := by - simp [Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem, h.symm] + IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) (infinitePi (fun i ↦ infinitePi (μ i))) := by simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi] + have hd : Disjoint (range fun i : ι ↦ (i, a)) (range fun i ↦ (i, b)) := by + simp [disjoint_range_iff, h] convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop)) - (iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (μ := μ) (by fun_prop)) hd - all_goals simp_rw [iSup_range, id_eq] + (iIndepFun_uncurry_infinitePi' (X := fun _ _ x ↦ x) μ (by fun_prop)) hd + all_goals rw [iSup_range] end ProbabilityTheory From becd8a34cc72eed7eb8d626dea6aace784563127 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 15 Dec 2025 10:25:44 +0000 Subject: [PATCH 5/5] Import new file --- LeanBandits.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanBandits.lean b/LeanBandits.lean index 69143345..86dda7b8 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -7,6 +7,7 @@ import LeanBandits.BanditAlgorithms.UCB import LeanBandits.ForMathlib.CondDistrib import LeanBandits.ForMathlib.IdentDistrib import LeanBandits.ForMathlib.IndepFun +import LeanBandits.ForMathlib.IndepInfinitePi import LeanBandits.ForMathlib.KernelSub import LeanBandits.ForMathlib.Measurable import LeanBandits.ForMathlib.MeasurableArgMax