From 521b547b1ea7bc2389d2774a50f40992933250e0 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Mon, 25 May 2026 11:05:16 +0100 Subject: [PATCH 1/2] Add AlgorithmDensity --- LeanMachineLearning.lean | 3 + .../Kernel/Composition/MeasureCompProd.lean | 31 ++++ .../Probability/WithDensity.lean | 127 ++++++++++++++++ .../SequentialLearning/Algorithm.lean | 16 +++ .../SequentialLearning/AlgorithmDensity.lean | 135 ++++++++++++++++++ 5 files changed, 312 insertions(+) create mode 100644 LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean create mode 100644 LeanMachineLearning/Probability/WithDensity.lean create mode 100644 LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 7d539fc3..3dbb4310 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -17,10 +17,13 @@ public import LeanMachineLearning.Probability.Independence.IndepInfinitePi public import LeanMachineLearning.Probability.Integrable public import LeanMachineLearning.Probability.Kernel.Basic public import LeanMachineLearning.Probability.Kernel.Composition.MapComap +public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj public import LeanMachineLearning.Probability.Kernel.KernelSub public import LeanMachineLearning.Probability.Moments.SubGaussian +public import LeanMachineLearning.Probability.WithDensity public import LeanMachineLearning.SequentialLearning.Algorithm +public import LeanMachineLearning.SequentialLearning.AlgorithmDensity public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin public import LeanMachineLearning.SequentialLearning.Deterministic diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean new file mode 100644 index 00000000..74690c0f --- /dev/null +++ b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Paulo Rauber +-/ +module + +public import Mathlib.Probability.Kernel.Composition.MeasureCompProd + +@[expose] public section + +open ProbabilityTheory + +namespace MeasureTheory.Measure + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} + +section AbsolutelyContinuous + +lemma AbsolutelyContinuous.compProd_left_apply {γ : Type*} {mγ : MeasurableSpace γ} + [IsSFiniteKernel η] {a : α} (hac : κ a ≪ η a) (ξ : Kernel (α × β) γ) : + (κ ⊗ₖ ξ) a ≪ (η ⊗ₖ ξ) a := by + by_cases hκ : IsSFiniteKernel κ + · by_cases hξ : IsSFiniteKernel ξ + · simp_rw [Kernel.compProd_apply_eq_compProd_sectR, hac.compProd_left _] + · simp [Kernel.compProd_of_not_isSFiniteKernel_right _ _ hξ] + · simp [Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ] + +end AbsolutelyContinuous + +end MeasureTheory.Measure diff --git a/LeanMachineLearning/Probability/WithDensity.lean b/LeanMachineLearning/Probability/WithDensity.lean new file mode 100644 index 00000000..8869a422 --- /dev/null +++ b/LeanMachineLearning/Probability/WithDensity.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Paulo Rauber +-/ +module + +public import Mathlib.Probability.Kernel.CompProdEqIff +public import Mathlib.Probability.Kernel.Composition.MeasureComp + +@[expose] public section + +open MeasureTheory ProbabilityTheory + +open scoped ENNReal + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} +variable {μ : Measure α} + +namespace MeasureTheory + +lemma map_withDensity_comp {g : α → γ} {f : γ → ℝ≥0∞} (hg : Measurable g) (hf : Measurable f) : + (μ.withDensity (f ∘ g)).map g = (μ.map g).withDensity f := by + ext s hs + rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs, + setLIntegral_map hs hf hg] + rfl + +lemma map_equiv_withDensity {e : α ≃ᵐ β} {f : α → ℝ≥0∞} (hf : Measurable f) : + (μ.withDensity f).map e = (μ.map e).withDensity (f ∘ e.symm) := by + simp_rw [← map_withDensity_comp e.measurable (hf.comp e.symm.measurable), + Function.comp_assoc, MeasurableEquiv.symm_comp_self] + rfl + +lemma map_swap_withDensity_comp_snd {μ : Measure (α × β)} {f : β → ℝ≥0∞} (hf : Measurable f) : + (μ.withDensity (fun ab ↦ f ab.2)).map Prod.swap = + (μ.map Prod.swap).withDensity (fun ba ↦ f ba.1) := by + rw [← map_withDensity_comp measurable_swap (by fun_prop)] + rfl + +end MeasureTheory + +namespace MeasureTheory.Measure + +lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞} + (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1) := by + refine ext_of_lintegral _ fun g hg ↦ ?_ + calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ) + = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) := + lintegral_compProd hg + _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ := + lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right' + _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ := + lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm + _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) := + (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm + _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) := + (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm + +lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] + {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g)) + [IsSFiniteKernel (κ.withDensity g)] : + (μ.withDensity f) ⊗ₘ (κ.withDensity g) = + (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2) := by + rw [compProd_withDensity hg, compProd_withDensity_left hf] + exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm + +/-- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/ +lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ] + [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f) + (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) : + μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2) := by + refine ext_of_lintegral _ fun g hg ↦ ?_ + calc ∫⁻ ab, g ab ∂(μ ⊗ₘ κ) + = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂μ := + lintegral_compProd hg + _ = ∫⁻ a, ∫⁻ b, g (a, b) ∂((η a).withDensity f) ∂μ := by + apply lintegral_congr_ae + filter_upwards [h] with a ha + rw [ha, Kernel.withDensity_apply _ (by fun_prop)] + _ = ∫⁻ a, ∫⁻ b, f b * g (a, b) ∂η a ∂μ := by + congr + ext a + exact lintegral_withDensity_eq_lintegral_mul _ hf (by fun_prop) + _ = ∫⁻ ab, f ab.2 * g ab ∂(μ ⊗ₘ η) := + (lintegral_compProd ((hf.comp measurable_snd).mul hg)).symm + _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2)) := + (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_snd) hg).symm + +end MeasureTheory.Measure + +namespace ProbabilityTheory.Kernel + +lemma bind_withDensity_eq_withDensity_bind {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞} + (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f := by + refine Measure.ext_of_lintegral _ fun g hg ↦ ?_ + calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ) + = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ := + Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable + _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by + congr + ext a + exact lintegral_withDensity _ (by fun_prop) _ hg + _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) := + (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm + _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) := + (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm + +lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞} + [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)] + (hf : Measurable (Function.uncurry f)) : + (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1) := by + ext a : 1 + calc ((κ.withDensity f) ⊗ₖ η) a + = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by + rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf] + _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) := + Measure.compProd_withDensity_left (by fun_prop) + _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by + rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)] + +lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β] + [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) : + η.withDensity (κ.rnDeriv η) = κ := + Kernel.ext fun a ↦ withDensity_rnDeriv_eq (h a) + +end ProbabilityTheory.Kernel diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index 2662ecf6..31495e2c 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -55,6 +55,22 @@ structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace instance (alg : Algorithm 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0 +/-- For every time and history, the distribution over actions according to `alg` is absolutely +continuous with respect to the distribution over actions according to `alg₀`. -/ +structure Algorithm.AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where + p0 : alg.p0 ≪ alg₀.p0 + policy n h : alg.policy n h ≪ alg₀.policy n h + +@[inherit_doc Algorithm.AbsolutelyContinuous] +scoped notation:50 alg " ≪ₐ " alg₀ => Algorithm.AbsolutelyContinuous alg alg₀ + +/-- An algorithm with observations in `𝓧 × 𝓨` obtained from an algorithm with observations in `𝓨` +by ignoring the `𝓧` component of each observation. -/ +def Algorithm.prod_left (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) : + Algorithm 𝓐 (𝓧 × 𝓨) where + policy n := (alg.policy n).comap (fun h i ↦ ((h i).1, (h i).2.2)) (by fun_prop) + p0 := alg.p0 + /-- A stochastic environment. -/ -- ANCHOR: Environment structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean new file mode 100644 index 00000000..77ba7f25 --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Paulo Rauber +-/ +module + +public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd +public import LeanMachineLearning.Probability.WithDensity +public import LeanMachineLearning.SequentialLearning.Algorithm + +@[expose] public section + +open MeasureTheory ProbabilityTheory Finset + +open scoped ENNReal + +namespace Learning + +variable {α R : Type*} [MeasurableSpace α] [MeasurableSpace R] + +namespace Algorithm + +/-- If the algorithm `alg` is absolutely continuous with respect to the algorithm `alg₀` and they +are both interacting with the same environment, then the law of the history at time `n` under `alg` +is the law of the history at time `n` under `alg₀` with density `alg.density alg₀ n`. -/ +noncomputable +def density [MeasurableSpace.CountablyGenerated α] (alg alg₀ : Algorithm α R) : + (n : ℕ) → (Iic n → α × R) → ℝ≥0∞ + | 0, h => (alg.p0.rnDeriv alg₀.p0 (h ⟨0, by simp⟩).1) + | n + 1, h => + let p := MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n h + alg.density alg₀ n p.1 * (alg.policy n).rnDeriv (alg₀.policy n) p.1 p.2.1 + +@[fun_prop] +lemma measurable_density [MeasurableSpace.CountablyGenerated α] (alg alg₀ : Algorithm α R) (n : ℕ) : + Measurable (alg.density alg₀ n) := by + induction n with + | zero => + simp_rw [density] + fun_prop + | succ n ih => + simp_rw [density] + fun_prop + +end Algorithm + +namespace IsAlgEnvSeq + +variable {Ω : Type*} [MeasurableSpace Ω] +variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] +variable {alg : Algorithm α R} {env : Environment α R} +variable {A : ℕ → Ω → α} {R' : ℕ → Ω → R} +variable {P : Measure Ω} [IsFiniteMeasure P] + +lemma hasLaw_hist_zero (h : IsAlgEnvSeq A R' alg env P) : HasLaw (hist A R' 0) + ((P.map (step A R' 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ α × R)).symm) P where + aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback 0).aemeasurable + map_eq := by + have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ α × R)).symm ∘ step A R' 0 = + hist A R' 0 := by + funext _ ⟨0, _⟩ + rfl + rw [← he] + have hA := h.measurable_action + have hR := h.measurable_feedback + exact (Measure.map_map (by fun_prop) (by fun_prop)).symm + +lemma hasLaw_hist_succ (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) : HasLaw (hist A R' (n + 1)) + ((P.map (hist A R' n) ⊗ₘ condDistrib (step A R' (n + 1)) (hist A R' n) P).map + (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm) P where + aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback (n + 1)).aemeasurable + map_eq := by + have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm ∘ + (fun ω ↦ (hist A R' n ω, step A R' (n + 1) ω)) = hist A R' (n + 1) := by + funext ω + exact (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm_apply_apply (hist A R' (n + 1) ω) + have hA := h.measurable_action + have hR := h.measurable_feedback + rw [← he, ← Measure.map_map (by fun_prop) (by fun_prop)] + congr + exact (compProd_map_condDistrib (by fun_prop)).symm + +variable {Ω₀ : Type*} [MeasurableSpace Ω₀] +variable {alg₀ : Algorithm α R} +variable {A₀ : ℕ → Ω₀ → α} {R₀ : ℕ → Ω₀ → R} +variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀] + +lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A R' alg env P) + (h₀ : IsAlgEnvSeq A₀ R₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : + P.map (IsAlgEnvSeq.hist A R' n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ R₀ n) := by + induction n with + | zero => + rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_zero.map_eq] + apply Measure.AbsolutelyContinuous.map _ (by fun_prop) + rw [h.hasLaw_step_zero.map_eq, h₀.hasLaw_step_zero.map_eq] + exact Measure.AbsolutelyContinuous.compProd_left hc.p0 _ + | succ n ih => + rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq] + apply Measure.AbsolutelyContinuous.map _ (by fun_prop) + rw [Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq, + Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq] + apply Measure.AbsolutelyContinuous.compProd ih + filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _ + +lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A R' alg env P) (h₀ : IsAlgEnvSeq A₀ R₀ alg₀ env P₀) + (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (IsAlgEnvSeq.hist A R' n) + ((P₀.map (IsAlgEnvSeq.hist A₀ R₀ n)).withDensity (alg.density alg₀ n)) P where + aemeasurable := + (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable + map_eq := by + induction n with + | zero => + rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_zero.map_eq, h.hasLaw_step_zero.map_eq, + h₀.hasLaw_step_zero.map_eq] + rw [← Measure.withDensity_rnDeriv_eq _ _ hc.p0, + Measure.compProd_withDensity_left (by fun_prop)] + exact map_equiv_withDensity (by fun_prop) + | succ n ih => + let ρ h' (ar : α × R) := Kernel.rnDeriv (alg.policy n) (alg₀.policy n) h' ar.1 + have hs : stepKernel alg env n = (stepKernel alg₀ env n).withDensity ρ := by + rw [stepKernel, ← Kernel.withDensity_rnDeriv_eq' (hc.policy n)] + exact Kernel.compProd_withDensity_left (Kernel.measurable_rnDeriv _ _) + have : IsMarkovKernel ((stepKernel alg₀ env n).withDensity ρ) := by + rw [← hs] + infer_instance + rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq, + Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq, + Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq, ih, hs, + Measure.compProd_withDensity_withDensity (by fun_prop) (by fun_prop)] + exact map_equiv_withDensity (by fun_prop) + +end IsAlgEnvSeq + +end Learning From 3764dea966011ecedde8929a1042796fe606fb29 Mon Sep 17 00:00:00 2001 From: Paulo Rauber Date: Tue, 26 May 2026 11:21:13 +0100 Subject: [PATCH 2/2] Adopt feedback --- .../Kernel/Composition/MeasureCompProd.lean | 4 +- .../Probability/WithDensity.lean | 14 +-- .../SequentialLearning/Algorithm.lean | 42 +++++-- .../SequentialLearning/AlgorithmDensity.lean | 114 ++++++++++-------- 4 files changed, 101 insertions(+), 73 deletions(-) diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean index 74690c0f..7caf1a15 100644 --- a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean +++ b/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 Paulo Rauber. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne, Paulo Rauber +Authors: Paulo Rauber -/ module diff --git a/LeanMachineLearning/Probability/WithDensity.lean b/LeanMachineLearning/Probability/WithDensity.lean index 8869a422..bc378c8f 100644 --- a/LeanMachineLearning/Probability/WithDensity.lean +++ b/LeanMachineLearning/Probability/WithDensity.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 Paulo Rauber. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne, Paulo Rauber +Authors: Paulo Rauber -/ module @@ -65,11 +65,11 @@ lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFini rw [compProd_withDensity hg, compProd_withDensity_left hf] exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm -/-- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/ lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ] [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f) (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2) := by + /- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/ refine ext_of_lintegral _ fun g hg ↦ ?_ calc ∫⁻ ab, g ab ∂(μ ⊗ₘ κ) = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂μ := @@ -79,8 +79,7 @@ lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α filter_upwards [h] with a ha rw [ha, Kernel.withDensity_apply _ (by fun_prop)] _ = ∫⁻ a, ∫⁻ b, f b * g (a, b) ∂η a ∂μ := by - congr - ext a + congr with a exact lintegral_withDensity_eq_lintegral_mul _ hf (by fun_prop) _ = ∫⁻ ab, f ab.2 * g ab ∂(μ ⊗ₘ η) := (lintegral_compProd ((hf.comp measurable_snd).mul hg)).symm @@ -91,15 +90,14 @@ end MeasureTheory.Measure namespace ProbabilityTheory.Kernel -lemma bind_withDensity_eq_withDensity_bind {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞} +lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞} (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f := by refine Measure.ext_of_lintegral _ fun g hg ↦ ?_ calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ) = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ := Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by - congr - ext a + congr with a exact lintegral_withDensity _ (by fun_prop) _ hg _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) := (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index 31495e2c..f2d67863 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -19,11 +19,13 @@ an algorithm interacting with an environment. * `Algorithm 𝓐 𝓨`: a stochastic, sequential algorithm. * `Environment 𝓐 𝓨`: a stochastic environment. -* `IsAlgEnvSeq A 𝓨' alg env P`: an algorithm-environment sequence. That is, a sequence of +* `IsAlgEnvSeq A 𝓨 alg env P`: an algorithm-environment sequence. That is, a sequence of actions `A` and feedback `Y` that have the correct conditional distributions to be generated by an algorithm `alg` interacting with an environment `env`, defined on a probability space `(Ω, P)`. * `IsAlgEnvSeqUntil A Y alg env P N`: `A` and `Y` form an algorithm-environment sequence until time `N`. +* `prod_left alg`: an `Algorithm 𝓐 (𝓧 × 𝓨)` obtained from an algorithm `alg : Algorithm 𝓐 𝓨` by + ignoring the `𝓧` component of each observation. ## Notes @@ -55,15 +57,6 @@ structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace instance (alg : Algorithm 𝓐 𝓨) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0 := alg.hp0 -/-- For every time and history, the distribution over actions according to `alg` is absolutely -continuous with respect to the distribution over actions according to `alg₀`. -/ -structure Algorithm.AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where - p0 : alg.p0 ≪ alg₀.p0 - policy n h : alg.policy n h ≪ alg₀.policy n h - -@[inherit_doc Algorithm.AbsolutelyContinuous] -scoped notation:50 alg " ≪ₐ " alg₀ => Algorithm.AbsolutelyContinuous alg alg₀ - /-- An algorithm with observations in `𝓧 × 𝓨` obtained from an algorithm with observations in `𝓨` by ignoring the `𝓧` component of each observation. -/ def Algorithm.prod_left (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) : @@ -206,6 +199,35 @@ lemma IsAlgEnvSeqUntil.hasCondDistrib_step (h : IsAlgEnvSeqUntil A Y alg env P N (stepKernel alg env n) P := HasCondDistrib.prod (h.hasCondDistrib_action n hn) (h.hasCondDistrib_feedback n hn) +lemma IsAlgEnvSeq.hasLaw_hist_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (hist A Y 0) + ((P.map (step A Y 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm) P where + aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback 0).aemeasurable + map_eq := by + have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm ∘ step A Y 0 = + hist A Y 0 := by + funext _ ⟨0, _⟩ + rfl + rw [← he] + have hA := h.measurable_action + have hY := h.measurable_feedback + exact (Measure.map_map (by fun_prop) (by fun_prop)).symm + +lemma IsAlgEnvSeq.hasLaw_hist_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : + HasLaw (hist A Y (n + 1)) + ((P.map (hist A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (hist A Y n) P).map + (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm) P where + aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback (n + 1)).aemeasurable + map_eq := by + have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm ∘ + (fun ω ↦ (hist A Y n ω, step A Y (n + 1) ω)) = hist A Y (n + 1) := by + funext ω + exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (hist A Y (n + 1) ω) + have hA := h.measurable_action + have hY := h.measurable_feedback + rw [← he, ← Measure.map_map (by fun_prop) (by fun_prop)] + congr + exact (compProd_map_condDistrib (by fun_prop)).symm + end IsAlgEnvSeq /-- Filtration generated by the history up to time `n`. -/ diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean index 77ba7f25..cb2b1fb7 100644 --- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Rémy Degenne. All rights reserved. +Copyright (c) 2026 Paulo Rauber. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne, Paulo Rauber +Authors: Paulo Rauber -/ module @@ -9,6 +9,35 @@ public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd public import LeanMachineLearning.Probability.WithDensity public import LeanMachineLearning.SequentialLearning.Algorithm +/-! +# Algorithm density + +We define a density function that allows obtaining the law of the history under one algorithm from +the law of the history under another algorithm when they are interacting with the same +environment. This also requires one algorithm to be absolutely continuous with respect to another, a +concept that we also introduce here. + +## Main definitions + +* `AbsolutelyContinuous alg alg₀`: `alg` is absolutely continuous with respect to `alg₀` (also + denoted `alg ≪ₐ alg₀`) when, in every situation, a set of actions with probability zero under + `alg₀` also has probability zero under `alg`. Intuitively, `alg` never acts in a way that `alg₀` + would never act. +* `density alg alg₀ n`: a density function that allows obtaining the law of the history at time `n` + under `alg` from the law of the history at time `n` under `alg₀` when they are interacting with + the same environment and `alg ≪ₐ alg₀`. + +## Main results + +* `absolutelyContinuous_map_hist`: the law of the history at time `n` under `alg` is absolutely + continuous with respect to the law of the history at time `n` under `alg₀` when they + are interacting with the same environment and `alg ≪ₐ alg₀`. +* `hasLaw_hist_withDensity`: the law of the history at time `n` under `alg` is the law of the + history at time `n` under `alg₀` with density `alg.density alg₀ n` when they are interacting + with the same environment and `alg ≪ₐ alg₀`. + +-/ + @[expose] public section open MeasureTheory ProbabilityTheory Finset @@ -17,78 +46,57 @@ open scoped ENNReal namespace Learning -variable {α R : Type*} [MeasurableSpace α] [MeasurableSpace R] +variable {𝓐 𝓨 : Type*} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] namespace Algorithm +/-- For every time and history, the distribution over actions according to `alg` is absolutely +continuous with respect to the distribution over actions according to `alg₀`. -/ +structure AbsolutelyContinuous (alg alg₀ : Algorithm 𝓐 𝓨) : Prop where + p0 : alg.p0 ≪ alg₀.p0 + policy n h : alg.policy n h ≪ alg₀.policy n h + +@[inherit_doc AbsolutelyContinuous] +scoped notation:50 alg " ≪ₐ " alg₀ => AbsolutelyContinuous alg alg₀ + /-- If the algorithm `alg` is absolutely continuous with respect to the algorithm `alg₀` and they are both interacting with the same environment, then the law of the history at time `n` under `alg` is the law of the history at time `n` under `alg₀` with density `alg.density alg₀ n`. -/ noncomputable -def density [MeasurableSpace.CountablyGenerated α] (alg alg₀ : Algorithm α R) : - (n : ℕ) → (Iic n → α × R) → ℝ≥0∞ +def density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) : + (n : ℕ) → (Iic n → 𝓐 × 𝓨) → ℝ≥0∞ | 0, h => (alg.p0.rnDeriv alg₀.p0 (h ⟨0, by simp⟩).1) | n + 1, h => - let p := MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n h + let p := MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n h alg.density alg₀ n p.1 * (alg.policy n).rnDeriv (alg₀.policy n) p.1 p.2.1 @[fun_prop] -lemma measurable_density [MeasurableSpace.CountablyGenerated α] (alg alg₀ : Algorithm α R) (n : ℕ) : +lemma measurable_density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ : Algorithm 𝓐 𝓨) (n : ℕ) : Measurable (alg.density alg₀ n) := by induction n with - | zero => - simp_rw [density] - fun_prop - | succ n ih => - simp_rw [density] - fun_prop + | zero => simp_rw [density]; fun_prop + | succ n ih => simp_rw [density]; fun_prop end Algorithm namespace IsAlgEnvSeq variable {Ω : Type*} [MeasurableSpace Ω] -variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] -variable {alg : Algorithm α R} {env : Environment α R} -variable {A : ℕ → Ω → α} {R' : ℕ → Ω → R} +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] +variable {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} +variable {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} variable {P : Measure Ω} [IsFiniteMeasure P] -lemma hasLaw_hist_zero (h : IsAlgEnvSeq A R' alg env P) : HasLaw (hist A R' 0) - ((P.map (step A R' 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ α × R)).symm) P where - aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback 0).aemeasurable - map_eq := by - have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ α × R)).symm ∘ step A R' 0 = - hist A R' 0 := by - funext _ ⟨0, _⟩ - rfl - rw [← he] - have hA := h.measurable_action - have hR := h.measurable_feedback - exact (Measure.map_map (by fun_prop) (by fun_prop)).symm - -lemma hasLaw_hist_succ (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) : HasLaw (hist A R' (n + 1)) - ((P.map (hist A R' n) ⊗ₘ condDistrib (step A R' (n + 1)) (hist A R' n) P).map - (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm) P where - aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback (n + 1)).aemeasurable - map_eq := by - have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm ∘ - (fun ω ↦ (hist A R' n ω, step A R' (n + 1) ω)) = hist A R' (n + 1) := by - funext ω - exact (MeasurableEquiv.IicSuccProd (fun _ ↦ α × R) n).symm_apply_apply (hist A R' (n + 1) ω) - have hA := h.measurable_action - have hR := h.measurable_feedback - rw [← he, ← Measure.map_map (by fun_prop) (by fun_prop)] - congr - exact (compProd_map_condDistrib (by fun_prop)).symm - variable {Ω₀ : Type*} [MeasurableSpace Ω₀] -variable {alg₀ : Algorithm α R} -variable {A₀ : ℕ → Ω₀ → α} {R₀ : ℕ → Ω₀ → R} +variable {alg₀ : Algorithm 𝓐 𝓨} +variable {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨} variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀] -lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A R' alg env P) - (h₀ : IsAlgEnvSeq A₀ R₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : - P.map (IsAlgEnvSeq.hist A R' n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ R₀ n) := by +open scoped Algorithm + +lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A Y alg env P) + (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : + P.map (IsAlgEnvSeq.hist A Y n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n) := by induction n with | zero => rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_zero.map_eq] @@ -103,9 +111,9 @@ lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A R' alg env P) apply Measure.AbsolutelyContinuous.compProd ih filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _ -lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A R' alg env P) (h₀ : IsAlgEnvSeq A₀ R₀ alg₀ env P₀) - (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (IsAlgEnvSeq.hist A R' n) - ((P₀.map (IsAlgEnvSeq.hist A₀ R₀ n)).withDensity (alg.density alg₀ n)) P where +lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) + (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (IsAlgEnvSeq.hist A Y n) + ((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where aemeasurable := (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable map_eq := by @@ -117,7 +125,7 @@ lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A R' alg env P) (h₀ : IsAlgEnvS Measure.compProd_withDensity_left (by fun_prop)] exact map_equiv_withDensity (by fun_prop) | succ n ih => - let ρ h' (ar : α × R) := Kernel.rnDeriv (alg.policy n) (alg₀.policy n) h' ar.1 + let ρ h' (ar : 𝓐 × 𝓨) := Kernel.rnDeriv (alg.policy n) (alg₀.policy n) h' ar.1 have hs : stepKernel alg env n = (stepKernel alg₀ env n).withDensity ρ := by rw [stepKernel, ← Kernel.withDensity_rnDeriv_eq' (hc.policy n)] exact Kernel.compProd_withDensity_left (Kernel.measurable_rnDeriv _ _)