From 774ce01d3bb20f169a33f4ff3848aa4456267fdd Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 15 Sep 2025 13:17:14 +0100 Subject: [PATCH 01/11] Refactor lemmas --- .../ForMathlib/KernelCompositionLemmas.lean | 21 +++++ .../KernelCompositionParallelComp.lean | 26 +++++++ LeanBandits/ForMathlib/Traj.lean | 78 +++++++++++++++++++ 3 files changed, 125 insertions(+) create mode 100644 LeanBandits/ForMathlib/KernelCompositionLemmas.lean create mode 100644 LeanBandits/ForMathlib/KernelCompositionParallelComp.lean create mode 100644 LeanBandits/ForMathlib/Traj.lean diff --git a/LeanBandits/ForMathlib/KernelCompositionLemmas.lean b/LeanBandits/ForMathlib/KernelCompositionLemmas.lean new file mode 100644 index 00000000..154af51f --- /dev/null +++ b/LeanBandits/ForMathlib/KernelCompositionLemmas.lean @@ -0,0 +1,21 @@ +import Mathlib.Probability.Kernel.Composition.Lemmas +import LeanBandits.ForMathlib.KernelCompositionParallelComp + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} + {μ : Measure α} {ν : Measure β} {κ : Kernel α β} + +-- PR: https://github.com/leanprover-community/mathlib4/pull/29555 +lemma MeasureTheory.Measure.compProd_map [SFinite μ] [IsSFiniteKernel κ] + {f : β → γ} (hf : Measurable f) : + μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f) := by + calc μ ⊗ₘ (κ.map f) + _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by + rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod, + Kernel.id_comp, Kernel.deterministic_comp_eq_map] + _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod] + _ = (μ ⊗ₘ κ).map (Prod.map id f) := by + rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map] diff --git a/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean b/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean new file mode 100644 index 00000000..4dd863f8 --- /dev/null +++ b/LeanBandits/ForMathlib/KernelCompositionParallelComp.lean @@ -0,0 +1,26 @@ +import Mathlib.Probability.Kernel.Composition.ParallelComp + +open MeasureTheory +open scoped ENNReal + +namespace ProbabilityTheory.Kernel + +variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} + {κ : Kernel α β} {η : Kernel γ δ} {x : α × γ} + +-- PR: https://github.com/leanprover-community/mathlib4/pull/29555 +lemma parallelComp_apply_prod [IsSFiniteKernel κ] [IsSFiniteKernel η] (s : Set β) (t : Set δ) : + (κ ∥ₖ η) x (s ×ˢ t) = (κ x.1 s) * (η x.2 t) := by + rw [parallelComp_apply, Measure.prod_prod] + +-- PR: https://github.com/leanprover-community/mathlib4/pull/29555 +lemma deterministic_parallelComp_deterministic + {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) : + (deterministic f hf) ∥ₖ (deterministic g hg) + = deterministic (Prod.map f g) (hf.prodMap hg) := by + ext x : 1 + rw [parallelComp_apply, deterministic_apply, deterministic_apply, deterministic_apply, Prod.map, + Measure.dirac_prod_dirac] + +end ProbabilityTheory.Kernel diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean new file mode 100644 index 00000000..ce90255c --- /dev/null +++ b/LeanBandits/ForMathlib/Traj.lean @@ -0,0 +1,78 @@ +import Mathlib.Probability.Kernel.IonescuTulcea.Traj +import Mathlib.Probability.Kernel.CondDistrib +import LeanBandits.ForMathlib.CondDistrib +import LeanBandits.ForMathlib.KernelCompositionLemmas + +open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory + +variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] +variable {κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)] +variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀] + +-- (Generalize for Embedding.lean?) Probability/Kernel/IonescuTulcea/Traj.lean +def MeasurableEquiv.piIicZero : X 0 ≃ᵐ (Π n : Iic 0, X n) := + have : Unique (Iic 0) := by simp_rw [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 + have e (n : Iic 0) : X n ≃ᵐ X 0 := + (congrArg (X · ≃ᵐ X 0) (nonpos_iff_eq_zero.1 (mem_Iic.1 n.2))).mpr (refl (X 0)) + ((piCongrRight e).trans (piUnique _)).symm + +namespace ProbabilityTheory.Kernel + +-- Probability/Kernel/IonescuTulcea/Traj.lean +noncomputable +def trajMeasure (μ₀ : Measure (X 0)) [IsProbabilityMeasure μ₀] + (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) [∀ n, IsMarkovKernel (κ n)] : + Measure (Π n, X n) := + (traj κ 0) ∘ₘ (μ₀.map MeasurableEquiv.piIicZero) + +-- Probability/Kernel/IonescuTulcea/Traj.lean +instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by + rw [trajMeasure] + have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero)) := + isProbabilityMeasure_map <| by fun_prop + infer_instance + +-- Probability/Kernel/IonescuTulcea/Traj.lean +lemma traj_map_eq_kernel {a : ℕ} : (traj κ a).map (fun x ↦ x (a + 1)) = κ a := by + set f : (Π n, X n) → X (a + 1) := fun x ↦ x (a + 1) + set g : (Π n : Iic (a + 1), X n) → X (a + 1) := fun x ↦ x ⟨a + 1, by simp⟩ + have hf : f = g ∘ (frestrictLe (a + 1)) := by rfl + have hp : g ∘ IicProdIoc a (a + 1) = (piSingleton a).symm ∘ Prod.snd := by + ext + simp [g, _root_.IicProdIoc, piSingleton] + rw [hf, map_comp_right, traj_map_frestrictLe, partialTraj_succ_self, ← map_comp_right, hp, + map_comp_right, ← snd_eq, snd_prod, ← map_comp_right] + all_goals measurability + +-- Probability/Kernel/IonescuTulcea/Traj.lean +lemma partialTraj_compProd_kernel_eq_traj_map {a : ℕ} {x₀ : Π n : Iic 0, X n} : + (partialTraj κ 0 a x₀) ⊗ₘ (κ a) = (traj κ 0 x₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by + set f := fun x ↦ (frestrictLe a x, x (a + 1)) + set g := fun x ↦ (frestrictLe a x, x) + have hf : f = (Prod.map id (fun x ↦ x (a + 1))) ∘ g := rfl + rw [hf, ← Measure.map_map, ← partialTraj_compProd_traj, ← MeasureTheory.Measure.compProd_map, + traj_map_eq_kernel] + all_goals measurability + +-- (Extract kernel lemmas from rewrites?) Probability/Kernel/IonescuTulcea/Traj.lean +lemma trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map {a : ℕ} : + (trajMeasure μ₀ κ).map (frestrictLe a) ⊗ₘ κ a = + (trajMeasure μ₀ κ).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by + rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp, traj_map_frestrictLe, + Measure.comp_assoc, Measure.map_comp] + any_goals fun_prop + congr + ext1 x₀ + rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply, + partialTraj_compProd_kernel_eq_traj_map] + fun_prop + +-- Probability/Kernel/IonescuTulcea/Traj.lean +lemma trajMeasure_condDistrib_ae_eq_kernel {a : ℕ} + [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] : + condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (trajMeasure μ₀ κ) + =ᵐ[(trajMeasure μ₀ κ).map (frestrictLe a)] κ a := by + apply condDistrib_ae_eq_of_measure_eq_compProd₀ (by measurability) (by measurability) + exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm + +end ProbabilityTheory.Kernel From d0d2960222a09098c52fb6bb559c098dae8cca21 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 15 Sep 2025 14:14:27 +0100 Subject: [PATCH 02/11] Remove redundant content --- LeanBandits/Bandit.lean | 14 +------------- LeanBandits/ForMathlib/CondDistrib.lean | 10 +--------- 2 files changed, 2 insertions(+), 22 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index f7ad7733..859fb1b1 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -5,6 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ import Mathlib import LeanBandits.ForMathlib.CondDistrib +import LeanBandits.ForMathlib.KernelCompositionLemmas /-! # Bandit @@ -171,19 +172,6 @@ open Kernel Preorder variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : { x // x ∈ Iic n }) → X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)] -lemma Measure.compProd_map {X Y Z : Type*} {mX : MeasurableSpace X} {mY : MeasurableSpace Y} - {mZ : MeasurableSpace Z} {μ : Measure X} {κ : Kernel X Y} [SFinite μ] [IsSFiniteKernel κ] - {f : Y → Z} (hf : Measurable f) : - μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f) := by - calc μ ⊗ₘ (κ.map f) - _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by - rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Measure.compProd_eq_comp_prod, - Kernel.id_comp, Kernel.deterministic_comp_eq_map] - _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [Measure.compProd_eq_comp_prod] - _ = (μ ⊗ₘ κ).map (Prod.map id f) := by - rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, - Measure.deterministic_comp_eq_map] - lemma partialTraj_compProd_eq_traj_map_frestrictLe (a : ℕ) (x₀ : (i : Iic 0) → X i) : (partialTraj κ 0 a x₀) ⊗ₘ (κ a) = (traj κ 0 x₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index 6e5812de..008dae02 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -8,7 +8,7 @@ import Mathlib.Probability.Independence.Conditional import Mathlib.Probability.Kernel.Composition.Lemmas import Mathlib.Probability.Kernel.CompProdEqIff import Mathlib.Probability.Kernel.Condexp - +import LeanBandits.ForMathlib.KernelCompositionParallelComp open MeasureTheory ProbabilityTheory Finset open scoped ENNReal NNReal @@ -68,14 +68,6 @@ end MeasureTheory.Measure namespace ProbabilityTheory -lemma Kernel.deterministic_parallelComp_deterministic - {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) : - (deterministic f hf) ∥ₖ (deterministic g hg) - = deterministic (Prod.map f g) (hf.prodMap hg) := by - ext x : 1 - rw [parallelComp_apply, deterministic_apply, deterministic_apply, deterministic_apply, Prod.map, - Measure.dirac_prod_dirac] - lemma Kernel.prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} : (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by From ab60b2622057d3b6656aad78578815095823afee Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 15 Sep 2025 14:58:59 +0100 Subject: [PATCH 03/11] Ready to start replacing trajMeasure on Bandit.lean --- LeanBandits.lean | 3 +++ LeanBandits/ForMathlib/Traj.lean | 6 +++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/LeanBandits.lean b/LeanBandits.lean index c2443ec0..aa4d81cb 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -2,6 +2,9 @@ import LeanBandits.AlgorithmBuilding import LeanBandits.Bandit import LeanBandits.ETC import LeanBandits.ForMathlib.CondDistrib +import LeanBandits.ForMathlib.KernelCompositionLemmas +import LeanBandits.ForMathlib.KernelCompositionParallelComp +import LeanBandits.ForMathlib.Traj import LeanBandits.Regret import LeanBandits.RewardByCountMeasure import LeanBandits.UCB diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index ce90255c..4c420441 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -10,7 +10,7 @@ variable {κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))} [∀ n, IsM variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀] -- (Generalize for Embedding.lean?) Probability/Kernel/IonescuTulcea/Traj.lean -def MeasurableEquiv.piIicZero : X 0 ≃ᵐ (Π n : Iic 0, X n) := +def MeasurableEquiv.piIicZero' : X 0 ≃ᵐ (Π n : Iic 0, X n) := have : Unique (Iic 0) := by simp_rw [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 have e (n : Iic 0) : X n ≃ᵐ X 0 := (congrArg (X · ≃ᵐ X 0) (nonpos_iff_eq_zero.1 (mem_Iic.1 n.2))).mpr (refl (X 0)) @@ -23,12 +23,12 @@ noncomputable def trajMeasure (μ₀ : Measure (X 0)) [IsProbabilityMeasure μ₀] (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) [∀ n, IsMarkovKernel (κ n)] : Measure (Π n, X n) := - (traj κ 0) ∘ₘ (μ₀.map MeasurableEquiv.piIicZero) + (traj κ 0) ∘ₘ (μ₀.map MeasurableEquiv.piIicZero') -- Probability/Kernel/IonescuTulcea/Traj.lean instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by rw [trajMeasure] - have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero)) := + have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero')) := isProbabilityMeasure_map <| by fun_prop infer_instance From c910ea6f75abb4f50c1ac9b50213d517c9b607bc Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 16 Sep 2025 09:24:07 +0100 Subject: [PATCH 04/11] Merged with trajMeasure --- LeanBandits/Bandit.lean | 34 +++++++------------------------- LeanBandits/ForMathlib/Traj.lean | 24 ++++++++++++++-------- 2 files changed, 23 insertions(+), 35 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 859fb1b1..eea54b30 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -6,27 +6,16 @@ Authors: Rémy Degenne, Paulo Rauber import Mathlib import LeanBandits.ForMathlib.CondDistrib import LeanBandits.ForMathlib.KernelCompositionLemmas +import LeanBandits.ForMathlib.Traj /-! # Bandit - -/ open MeasureTheory ProbabilityTheory Filter Real Finset open scoped ENNReal NNReal -instance : Unique (Iic 0) := by simp only [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 - -lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := by - calc _ = ((⟨0, by simp⟩ : Iic 0) : ℕ) := by congr; exact (Unique.eq_default _).symm - _ = _ := by simp - -/-- Measurable equivalence between `Iic 0 → X i` and `X 0`. -/ -def MeasurableEquiv.piIicZero (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] : - ((i : Iic 0) → X i) ≃ᵐ X 0 := - (MeasurableEquiv.piUnique _).trans (coe_default_Iic_zero.symm ▸ MeasurableEquiv.refl _) - namespace Bandits variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} @@ -85,7 +74,8 @@ deriving IsMarkovKernel /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/ noncomputable def trajMeasure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α × R) := - (traj alg ν 0) ∘ₘ ((alg.p0 ⊗ₘ ν).map (MeasurableEquiv.piIicZero (fun _ ↦ α × R)).symm) + ProbabilityTheory.Kernel.trajMeasure (alg.p0 ⊗ₘ ν) (stepKernel alg ν) +deriving IsProbabilityMeasure /-- Measure of an infinite stream of rewards from each arm. -/ noncomputable @@ -93,14 +83,6 @@ def streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α Measure.infinitePi fun _ ↦ Measure.infinitePi ν deriving IsProbabilityMeasure -instance (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - IsProbabilityMeasure (trajMeasure alg ν) := by - rw [trajMeasure] - have : IsProbabilityMeasure - ((alg.p0 ⊗ₘ ν).map (MeasurableEquiv.piIicZero (fun _ ↦ α × R)).symm) := - isProbabilityMeasure_map <| by fun_prop - infer_instance - /-- Joint distribution of the sequence of arm pulled and rewards, and a stream of independent rewards from all arms. -/ noncomputable @@ -227,10 +209,8 @@ end Traj lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) - =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := - condDistrib_lemma (X := fun _ ↦ α × R) - ((alg.p0 ⊗ₘ ν).map (MeasurableEquiv.piIicZero (fun _ ↦ α × R)).symm) - (κ := Bandit.stepKernel alg ν) n + =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := by + exact ProbabilityTheory.Kernel.trajMeasure_condDistrib_ae_eq_kernel lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : @@ -255,9 +235,9 @@ lemma hasLaw_step_zero HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) where aemeasurable := Measurable.aemeasurable (by fun_prop) map_eq := by - simp only [Bandit.trajMeasure] + simp only [Bandit.trajMeasure, ProbabilityTheory.Kernel.trajMeasure] rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, - Kernel.deterministic_comp_eq_map, Bandit.traj, traj_zero_map_eval_zero, + Kernel.deterministic_comp_eq_map, traj_zero_map_eval_zero, Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] simp diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index 4c420441..e23416e0 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -9,12 +9,20 @@ variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] variable {κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)] variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀] --- (Generalize for Embedding.lean?) Probability/Kernel/IonescuTulcea/Traj.lean -def MeasurableEquiv.piIicZero' : X 0 ≃ᵐ (Π n : Iic 0, X n) := - have : Unique (Iic 0) := by simp_rw [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 - have e (n : Iic 0) : X n ≃ᵐ X 0 := - (congrArg (X · ≃ᵐ X 0) (nonpos_iff_eq_zero.1 (mem_Iic.1 n.2))).mpr (refl (X 0)) - ((piCongrRight e).trans (piUnique _)).symm +section MeasurableEquiv + +instance : Unique (Iic 0) := by simp only [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 + +lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := by + calc _ = ((⟨0, by simp⟩ : Iic 0) : ℕ) := by congr; exact (Unique.eq_default _).symm + _ = _ := by simp + +/-- Measurable equivalence between `Iic 0 → X i` and `X 0`. -/ +def MeasurableEquiv.piIicZero (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] : + ((i : Iic 0) → X i) ≃ᵐ X 0 := + (MeasurableEquiv.piUnique _).trans (coe_default_Iic_zero.symm ▸ MeasurableEquiv.refl _) + +end MeasurableEquiv namespace ProbabilityTheory.Kernel @@ -23,12 +31,12 @@ noncomputable def trajMeasure (μ₀ : Measure (X 0)) [IsProbabilityMeasure μ₀] (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) [∀ n, IsMarkovKernel (κ n)] : Measure (Π n, X n) := - (traj κ 0) ∘ₘ (μ₀.map MeasurableEquiv.piIicZero') + (traj κ 0) ∘ₘ (μ₀.map (MeasurableEquiv.piIicZero _).symm) -- Probability/Kernel/IonescuTulcea/Traj.lean instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by rw [trajMeasure] - have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero')) := + have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero _).symm) := isProbabilityMeasure_map <| by fun_prop infer_instance From 1deb375d2335ea42360ccccbee9ededfbc07eea7 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 16 Sep 2025 09:54:18 +0100 Subject: [PATCH 05/11] Fix lint --- LeanBandits/ForMathlib/Traj.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index e23416e0..efd2aebe 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -27,9 +27,10 @@ end MeasurableEquiv namespace ProbabilityTheory.Kernel -- Probability/Kernel/IonescuTulcea/Traj.lean +/- Distribution of the infinite trajectory given the distribution of `X 0`. -/ noncomputable -def trajMeasure (μ₀ : Measure (X 0)) [IsProbabilityMeasure μ₀] - (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) [∀ n, IsMarkovKernel (κ n)] : +def trajMeasure (μ₀ : Measure (X 0)) (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) + [∀ n, IsMarkovKernel (κ n)] : Measure (Π n, X n) := (traj κ 0) ∘ₘ (μ₀.map (MeasurableEquiv.piIicZero _).symm) From d85c7850b428a2dfa5a2747cea8dc245c59ce482 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 16 Sep 2025 09:58:34 +0100 Subject: [PATCH 06/11] Fix lint --- LeanBandits/ForMathlib/Traj.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index efd2aebe..68cd7752 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -27,7 +27,7 @@ end MeasurableEquiv namespace ProbabilityTheory.Kernel -- Probability/Kernel/IonescuTulcea/Traj.lean -/- Distribution of the infinite trajectory given the distribution of `X 0`. -/ +/-- Distribution of the infinite trajectory given the distribution of `X 0`. -/ noncomputable def trajMeasure (μ₀ : Measure (X 0)) (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) [∀ n, IsMarkovKernel (κ n)] : From f01d769d2a6d735de26c47618da0a2d5657488c2 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 16 Sep 2025 10:08:36 +0100 Subject: [PATCH 07/11] Remove redundant results --- LeanBandits/Bandit.lean | 38 -------------------------------------- 1 file changed, 38 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index eea54b30..5da9da0d 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -154,44 +154,6 @@ open Kernel Preorder variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : { x // x ∈ Iic n }) → X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)] -lemma partialTraj_compProd_eq_traj_map_frestrictLe (a : ℕ) (x₀ : (i : Iic 0) → X i) : - (partialTraj κ 0 a x₀) ⊗ₘ (κ a) = - (traj κ 0 x₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by - have h1 := partialTraj_compProd_traj (κ := κ) (zero_le a) x₀ - have h2 : (fun x : Π n, X n ↦ (frestrictLe a x, x (a + 1))) = - (Prod.map id (fun x ↦ x (a + 1))) ∘ (fun x ↦ (frestrictLe a x, x)) := by ext <;> simp - rw [h2, ← Measure.map_map (by fun_prop) (by fun_prop), ← h1, ← Measure.compProd_map (by fun_prop)] - congr - have : (fun x : Π n, X n ↦ x (a + 1)) = - (fun x : Π i : Iic (a + 1), X i ↦ x ⟨a+1, by simp⟩) ∘ (frestrictLe (a + 1)) := by ext; simp - rw [this, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe, - partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop)] - have : (fun x : Π i : Iic (a + 1), X i ↦ x ⟨a+1, by simp⟩) ∘ IicProdIoc a (a + 1) - = (MeasurableEquiv.piSingleton a).symm ∘ Prod.snd := by - ext; simp [_root_.IicProdIoc, MeasurableEquiv.piSingleton] - rw [this, map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod, - ← map_comp_right _ (by fun_prop) (by fun_prop)] - simp - -lemma traj_cond_lemma1 {a : ℕ} (μ₀ : Measure ((i : Iic 0) → X i)) [IsFiniteMeasure μ₀] : - (traj κ 0 ∘ₘ μ₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) - = (traj κ 0 ∘ₘ μ₀).map (frestrictLe a) ⊗ₘ κ a := by - rw [Measure.compProd_eq_comp_prod, Measure.map_comp _ _ (by fun_prop), - Measure.map_comp _ _ (by fun_prop), Measure.comp_assoc, traj_map_frestrictLe] - congr - ext x₀ : 1 - rw [ProbabilityTheory.Kernel.comp_apply, ← Measure.compProd_eq_comp_prod] - symm - rw [Kernel.map_apply _ (by fun_prop)] - exact partialTraj_compProd_eq_traj_map_frestrictLe a x₀ - -lemma condDistrib_lemma (μ₀ : Measure ((i : Iic 0) → X i)) [IsFiniteMeasure μ₀] (a : ℕ) - [Nonempty (X (a + 1))] [StandardBorelSpace (X (a + 1))] : - condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (traj κ 0 ∘ₘ μ₀) - =ᵐ[(traj κ 0 ∘ₘ μ₀).map (frestrictLe a)] κ a := by - symm - exact condDistrib_ae_eq_of_measure_eq_compProd (by fun_prop) (by fun_prop) _ (traj_cond_lemma1 μ₀) - lemma traj_zero_map_eval_zero : (Kernel.traj κ 0).map (fun h ↦ h 0) = Kernel.deterministic (MeasurableEquiv.piIicZero X) From 184dd99429c676a9fa023749ff8bbd72e7ddccdb Mon Sep 17 00:00:00 2001 From: paulorauber Date: Tue, 16 Sep 2025 10:23:09 +0100 Subject: [PATCH 08/11] Update LeanBandits/Bandit.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Rémy Degenne --- LeanBandits/Bandit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 5da9da0d..596caa41 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -74,7 +74,7 @@ deriving IsMarkovKernel /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/ noncomputable def trajMeasure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α × R) := - ProbabilityTheory.Kernel.trajMeasure (alg.p0 ⊗ₘ ν) (stepKernel alg ν) + Kernel.trajMeasure (alg.p0 ⊗ₘ ν) (stepKernel alg ν) deriving IsProbabilityMeasure /-- Measure of an infinite stream of rewards from each arm. -/ From 93a4cbe68bb96ddb59de909f3ddbbd8ecd0cef2f Mon Sep 17 00:00:00 2001 From: paulorauber Date: Tue, 16 Sep 2025 10:23:21 +0100 Subject: [PATCH 09/11] Update LeanBandits/Bandit.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Rémy Degenne --- LeanBandits/Bandit.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 596caa41..958786ee 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -171,8 +171,8 @@ end Traj lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) - =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := by - exact ProbabilityTheory.Kernel.trajMeasure_condDistrib_ae_eq_kernel + =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := + Kernel.trajMeasure_condDistrib_ae_eq_kernel lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : From cd6dbfd377a8fa5c8bed91c218a7ca0a9c369c64 Mon Sep 17 00:00:00 2001 From: paulorauber Date: Tue, 16 Sep 2025 10:24:38 +0100 Subject: [PATCH 10/11] Update LeanBandits/Bandit.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Rémy Degenne --- LeanBandits/Bandit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 958786ee..ca1501c7 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -197,7 +197,7 @@ lemma hasLaw_step_zero HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) where aemeasurable := Measurable.aemeasurable (by fun_prop) map_eq := by - simp only [Bandit.trajMeasure, ProbabilityTheory.Kernel.trajMeasure] + simp only [Bandit.trajMeasure, Kernel.trajMeasure] rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, Kernel.deterministic_comp_eq_map, traj_zero_map_eval_zero, Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] From cda4b01c0786071e3f8697a01958cfdaee0da6ef Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 16 Sep 2025 10:27:06 +0100 Subject: [PATCH 11/11] Change lemma name --- LeanBandits/Bandit.lean | 2 +- LeanBandits/ForMathlib/Traj.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index ca1501c7..517debd5 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -172,7 +172,7 @@ lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBore (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν) =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n := - Kernel.trajMeasure_condDistrib_ae_eq_kernel + Kernel.condDistrib_trajMeasure_ae_eq_kernel lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index 68cd7752..f8ee9d34 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -77,7 +77,7 @@ lemma trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map {a : ℕ} : fun_prop -- Probability/Kernel/IonescuTulcea/Traj.lean -lemma trajMeasure_condDistrib_ae_eq_kernel {a : ℕ} +lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ} [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] : condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (trajMeasure μ₀ κ) =ᵐ[(trajMeasure μ₀ κ).map (frestrictLe a)] κ a := by