From 059af951a746d938d3c78a8d2babfcf9620ce359 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 15:53:15 +0200 Subject: [PATCH 1/6] use upstreamed HasCondDistrib definition --- .../Probability/HasCondDistrib.lean | 207 +++++------------- .../Online/Bandit/Algorithms/TS.lean | 15 +- .../Online/Bandit/ArrayProbSpace.lean | 61 +++--- .../Online/Bandit/RewardByCountMeasure.lean | 7 +- .../SequentialLearning/Algorithm.lean | 3 +- .../AlgorithmDensityBayes.lean | 14 +- .../Algorithms/RandomSampling.lean | 18 +- .../Algorithms/RoundRobin.lean | 3 +- .../BayesStationaryEnv.lean | 21 +- .../SequentialLearning/Deterministic.lean | 36 ++- .../SequentialLearning/EvaluationEnv.lean | 18 +- .../IonescuTulceaSpace.lean | 77 ++++--- .../SequentialLearning/StationaryEnv.lean | 14 +- 13 files changed, 207 insertions(+), 287 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index 0ab08b0c..033b8dae 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -6,7 +6,7 @@ Authors: Rémy Degenne, Paulo Rauber module public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib -public import Mathlib.Probability.HasLaw +public import Mathlib.Probability.HasCondDistrib /-! # A predicate for having a specified conditional distribution @@ -20,98 +20,34 @@ namespace ProbabilityTheory variable {α β γ Ω Ω' : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} - {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] - {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace Ω'] [Nonempty Ω'] + {mΩ : MeasurableSpace Ω} + {mΩ' : MeasurableSpace Ω'} {μ : Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω} -/-- Predicate stating that the conditional distribution of `Y` given `X` under the measure `μ` -is equal to the kernel `κ`. -/ -structure HasCondDistrib (Y : α → Ω) (X : α → β) (κ : Kernel β Ω) - (μ : Measure α) [IsFiniteMeasure μ] : Prop where - aemeasurable_fst : AEMeasurable Y μ := by fun_prop - aemeasurable_snd : AEMeasurable X μ := by fun_prop - condDistrib_eq : condDistrib Y X μ =ᵐ[μ.map X] κ - -attribute [fun_prop] HasCondDistrib.aemeasurable_fst HasCondDistrib.aemeasurable_snd - -lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} - {κ : Kernel β Ω} +lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} {κ : Kernel β Ω} {μ : Measure α} [IsFiniteMeasure μ] {ν : Measure γ} [IsProbabilityMeasure ν] (h : HasCondDistrib Y X κ μ) : HasCondDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) κ (μ.prod ν) where - aemeasurable_fst := by have := h.aemeasurable_fst; fun_prop - aemeasurable_snd := by have := h.aemeasurable_snd; fun_prop - condDistrib_eq := by - have : ((μ.prod ν).map (fun ω ↦ X ω.1)) = μ.map X := by + aemeasurable := by fun_prop + map_eq := by + have h_rhs : Measure.map (fun ω ↦ X ω.1) (μ.prod ν) ⊗ₘ κ = (μ.map X) ⊗ₘ κ := by conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst] rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)] · rfl - · have := h.aemeasurable_snd + · have := h.aemeasurable_fst simpa - rw [this] - exact (condDistrib_fst_prod X h.aemeasurable_fst ν).trans h.condDistrib_eq - -lemma HasCondDistrib.comp [IsFiniteMeasure μ] - (h : HasCondDistrib Y X κ μ) {f : Ω → Ω'} (hf : Measurable f) : - HasCondDistrib (fun ω ↦ f (Y ω)) X (κ.map f) μ where - aemeasurable_fst := by have := h.aemeasurable_fst; fun_prop - aemeasurable_snd := by have := h.aemeasurable_snd; fun_prop - condDistrib_eq := by - have h_comp := condDistrib_comp X (Y := Y) (f := f) (mβ := mβ) h.aemeasurable_fst hf - refine h_comp.trans ?_ - have h' := h.condDistrib_eq - filter_upwards [h'] with ω hω - rw [Kernel.map_apply _ hf, hω, Kernel.map_apply _ hf] - -lemma HasCondDistrib.fst {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [IsFiniteMeasure μ] - (h : HasCondDistrib Y X κ μ) : - HasCondDistrib (fun ω ↦ (Y ω).1) X κ.fst μ := by - rw [Kernel.fst_eq] - exact HasCondDistrib.comp h measurable_fst - -lemma HasCondDistrib.snd {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [IsFiniteMeasure μ] - (h : HasCondDistrib Y X κ μ) : - HasCondDistrib (fun ω ↦ (Y ω).2) X κ.snd μ := by - rw [Kernel.snd_eq] - exact HasCondDistrib.comp h measurable_snd - --- TODO: Rename to `HasCondDistrib.comp_right`? -lemma HasCondDistrib.comp_right' [IsFiniteMeasure μ] [IsFiniteKernel κ] {f : γ → β} - (hf : Measurable f) {Z : α → γ} (h : HasCondDistrib Y Z (κ.comap f hf) μ) : - HasCondDistrib Y (f ∘ Z) κ μ := by - have hY : AEMeasurable Y μ := h.aemeasurable_fst - have hZ : AEMeasurable Z μ := h.aemeasurable_snd - have hfZ : AEMeasurable (f ∘ Z) μ := hf.comp_aemeasurable hZ - refine ⟨hY, hfZ, ?_⟩ - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ hY] - calc μ.map (fun a ↦ ((f ∘ Z) a, Y a)) - _ = (μ.map (fun a ↦ (Z a, Y a))).map (Prod.map f id) := by - rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (hZ.prodMk hY)] - rfl - _ = (μ.map Z ⊗ₘ κ.comap f hf).map (Prod.map f id) := by - rw [(condDistrib_ae_eq_iff_measure_eq_compProd Z hY _).mp h.condDistrib_eq] - _ = (μ.map Z).map f ⊗ₘ κ := by - ext s hs - rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply (by measurability), - Measure.compProd_apply hs, lintegral_map (Kernel.measurable_kernel_prodMk_left hs) hf] - rfl - _ = μ.map (f ∘ Z) ⊗ₘ κ := by - rw [AEMeasurable.map_map_of_aemeasurable hf.aemeasurable hZ] - -lemma HasCondDistrib.comp_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ) - (f : β ≃ᵐ γ) : - HasCondDistrib Y (f ∘ X) (κ.comap f.symm (by fun_prop) : Kernel γ Ω) μ := by - apply HasCondDistrib.comp_right' f.measurable - simpa [← Kernel.comap_comp_right] + rw [h_rhs, ← h.map_eq] + conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst] + rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)] + · rfl + · have := h.aemeasurable + simpa lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ) {f : β → γ} (hf : Measurable f) : HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ := by - have hY := h.aemeasurable_fst - have hX := h.aemeasurable_snd - refine ⟨h.aemeasurable_fst, by fun_prop, ?_⟩ - have h_eq := h.condDistrib_eq - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢ + refine ⟨by fun_prop, ?_⟩ + have h_eq := h.map_eq calc μ.map (fun x ↦ ((X x, f (X x)), Y x)) _ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ ((p.1, f p.1), p.2)) := by rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] @@ -145,10 +81,8 @@ lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X have h_eq : X = (fun p ↦ p.1) ∘ (fun a ↦ (X a, f (X a))) := by ext; simp rw [h_eq] exact Measurable.comp_aemeasurable (by fun_prop) (by fun_prop) - have hY := h.aemeasurable_fst - refine ⟨by fun_prop, by fun_prop, ?_⟩ - have h_eq := h.condDistrib_eq - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢ + refine ⟨by fun_prop, ?_⟩ + have h_eq := h.map_eq calc μ.map (fun x ↦ (X x, Y x)) _ = (μ.map (fun ω ↦ ((X ω, f (X ω)), Y ω))).map (fun p ↦ (p.1.1, p.2)) := by rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] @@ -172,101 +106,70 @@ lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id, Measure.map_dirac' (by fun_prop)] -lemma HasCondDistrib.hasLaw_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q] - (h : HasCondDistrib Y X (Kernel.const β Q) μ) : HasLaw Y Q μ := by - obtain ⟨hY, hX, h⟩ := h - refine ⟨hY, ?_⟩ - have h_snd : (μ.map (fun ω => (X ω, Y ω))).snd = Q := by - have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (Kernel.const _ Q) := - have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (condDistrib Y X μ) := - (compProd_map_condDistrib hY).symm - h_map.trans (Measure.compProd_congr h) - rw [h_map, MeasureTheory.Measure.snd_compProd] - simp [MeasureTheory.Measure.map_apply_of_aemeasurable hX] - rwa [Measure.snd_map_prodMk₀ hX] at h_snd - lemma HasCondDistrib.indepFun_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q] - (h : HasCondDistrib Y X (Kernel.const β Q) μ) : IndepFun X Y μ := by - rw [indepFun_iff_condDistrib_eq_const h.aemeasurable_snd h.aemeasurable_fst, - h.hasLaw_of_const.map_eq] - exact h.condDistrib_eq + (h : HasCondDistrib Y X (Kernel.const β Q) μ) : + IndepFun X Y μ := by + rw [indepFun_iff_map_prod_eq_prod_map_map h.aemeasurable_fst h.aemeasurable_snd, h.map_eq, + h.hasLaw_of_const.map_eq, Measure.compProd_const] lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q] (h : HasCondDistrib Y X (Kernel.const β Q) μ) [StandardBorelSpace β] [Nonempty β] : HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where - aemeasurable_fst := h.aemeasurable_snd - aemeasurable_snd := h.aemeasurable_fst - condDistrib_eq := - condDistrib_of_indepFun h.indepFun_of_const.symm h.aemeasurable_fst h.aemeasurable_snd + aemeasurable := by fun_prop + map_eq := by + calc μ.map (fun ω ↦ (Y ω, X ω)) + _ = (μ.map (fun ω ↦ (X ω, Y ω))).map Prod.swap := by + rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] + rfl + _ = (μ.map X ⊗ₘ Kernel.const β Q).map Prod.swap := by rw [h.map_eq] + _ = μ.map Y ⊗ₘ Kernel.const Ω (μ.map X) := by simp [h.hasLaw_of_const.map_eq, Measure.prod_swap] lemma HasLaw.prod_of_hasCondDistrib {P : Measure β} [IsFiniteMeasure μ] [IsSFiniteKernel κ] (h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) : - HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ := by - have hX := h1.aemeasurable - have hY := h2.aemeasurable_fst - refine ⟨by fun_prop, ?_⟩ - rw [← compProd_map_condDistrib (by fun_prop), h1.map_eq] - refine Measure.compProd_congr ?_ - rw [← h1.map_eq] - exact h2.condDistrib_eq - -lemma HasCondDistrib.of_compProd [IsFiniteMeasure μ] [IsFiniteKernel κ] {Z : α → Ω'} - {η : Kernel (β × Ω) Ω'} [IsMarkovKernel η] - (h : HasCondDistrib (fun a ↦ (Y a, Z a)) X (κ ⊗ₖ η) μ) : - HasCondDistrib Z (fun a ↦ (X a, Y a)) η μ := by - have hZ : AEMeasurable Z μ := h.aemeasurable_fst.snd - have hX : AEMeasurable X μ := h.aemeasurable_snd - have hY : AEMeasurable Y μ := h.aemeasurable_fst.fst - refine ⟨hZ, (hX.prodMk hY), ?_⟩ - have hc := h.condDistrib_eq - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at hc ⊢ - calc μ.map (fun a ↦ ((X a, Y a), Z a)) - _ = (μ.map X ⊗ₘ (κ ⊗ₖ η)).map MeasurableEquiv.prodAssoc.symm := by - rw [← hc, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] - rfl - _ = μ.map X ⊗ₘ κ ⊗ₘ η := - Measure.compProd_assoc - _ = μ.map (fun a ↦ (X a, Y a)) ⊗ₘ η := by - rw [← (condDistrib_ae_eq_iff_measure_eq_compProd X hY κ).1] - simpa using h.fst.condDistrib_eq + HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ := + ⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩ lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ] {Z : α → Ω'} {η : Kernel (β × Ω) Ω'} [IsFiniteKernel η] (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) : HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ := by - have hX := h1.aemeasurable_snd - have hY := h1.aemeasurable_fst - have hZ := h2.aemeasurable_fst - refine ⟨by fun_prop, by fun_prop, ?_⟩ - have h_condDistrib_Y := h1.condDistrib_eq - have h_condDistrib_Z := h2.condDistrib_eq - have h_prod := condDistrib_prod_left hY hZ hX - have h_prod' : 𝓛[fun ω ↦ (Y ω, Z ω) | X; μ] =ᵐ[μ.map X] (κ ⊗ₖ 𝓛[Z | fun ω ↦ (X ω, Y ω); μ]) := by - filter_upwards [h_condDistrib_Y, h_prod] with ω hω₁ hω₂ - rw [hω₂] - ext s hs - rw [Kernel.compProd_apply hs, Kernel.compProd_apply hs] - simp [hω₁] - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] - at h_condDistrib_Z h_condDistrib_Y ⊢ - rw [← Measure.compProd_assoc', ← h_condDistrib_Y, ← h_condDistrib_Z, + refine ⟨by fun_prop, ?_⟩ + rw [← Measure.compProd_assoc', ← h1.map_eq, ← h2.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] rfl +variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempty Ω'] + +lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ] + (h : HasCondDistrib Y X κ μ) : + condDistrib Y X μ =ᵐ[μ.map X] κ := by + rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq] + +lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ] + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) + (h : condDistrib Y X μ =ᵐ[μ.map X] κ) : + HasCondDistrib Y X κ μ where + aemeasurable := by fun_prop + map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h] + lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β] - {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω} {η : Kernel (γ × β) Ω} (hf : Measurable f) + {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω} + {η : Kernel (γ × β) Ω} [IsFiniteKernel η] (hf : Measurable f) (hg : Measurable g) (hW : AEMeasurable W μ) (hcd : HasCondDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) η μ) : ∀ᵐ z ∂(μ.map Z), HasCondDistrib g f (η.sectR z) (condDistrib W Z μ z) := by + suffices ∀ᵐ z ∂μ.map Z, condDistrib g f (condDistrib W Z μ z) =ᵐ[(condDistrib W Z μ z).map f] + (η.sectR z) by + filter_upwards [this] with z hz + exact hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) hz have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ =ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by rw [← Measure.compProd_congr (condDistrib_comp Z hW hf), compProd_map_condDistrib (hf.comp_aemeasurable hW)] exact hcd.condDistrib_eq filter_upwards [ - condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_snd.fst, + condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_fst.fst, Measure.ae_ae_of_ae_compProd h_eq] with z hc ha - refine ⟨hg.aemeasurable, hf.aemeasurable, ?_⟩ rw [Kernel.map_apply _ hf] at ha filter_upwards [hc, ha] with b hcb hab using hcb.trans hab diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean index 1310275b..586502cd 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean @@ -92,17 +92,18 @@ variable {P : Measure Ω} [IsProbabilityMeasure P] of the next action given the history so far is equal to the conditional distribution of the best action given the history so far. -/ lemma TS.hasCondDistrib_action (hK : 0 < K) (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm hK Q κ) E A R P) - (n : ℕ) : HasCondDistrib (A (n + 1)) (history A R n) + (n : ℕ) : + HasCondDistrib (A (n + 1)) (history A R n) (condDistrib (bestAction κ E) (history A R n) P) P where - aemeasurable_fst := (h.measurable_action (n + 1)).aemeasurable - aemeasurable_snd := - (measurable_history h.measurable_action h.measurable_feedback n).aemeasurable - condDistrib_eq := by + aemeasurable := ((measurable_history h.measurable_action h.measurable_feedback n).prodMk + (h.measurable_action (n + 1))).aemeasurable + map_eq := by have hm : Measurable (bestAction κ id) := by fun_prop + rw [(h.hasCondDistrib_action' n).map_eq] + refine Measure.compProd_congr ?_ calc _ =ᵐ[P.map (history A R n)] - (IT.bayesTrajMeasurePosterior Q κ uniformAlgorithm n).map (bestAction κ id) := - (h.hasCondDistrib_action' n).condDistrib_eq + (IT.bayesTrajMeasurePosterior Q κ uniformAlgorithm n).map (bestAction κ id) := by rfl _ =ᵐ[P.map (history A R n)] (condDistrib E (history A R n) P).map (bestAction κ id) := by filter_upwards [(h.hasCondDistrib_env_history diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 392c1453..16e55bcf 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -954,37 +954,36 @@ lemma hasLaw_action_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkov variable [StandardBorelSpace R] [Nonempty R] lemma hasCondDistrib_reward_zero (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] : - HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) where - condDistrib_eq := by - refine (condDistrib_ae_eq_cond (by fun_prop) (by fun_prop)).trans ?_ - rw [Filter.EventuallyEq, ae_iff_of_countable] - intro a ha - simp only [reward_zero] - calc ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 (action alg 0 ω)) - _ = ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 a) := by - refine Measure.map_congr - (ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_) - intro x hx - simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx - simp [hx] - _ = ν a := by - rw [cond_of_indepFun] - · exact map_snd_apply_arrayMeasure 0 a - · have : (fun ω ↦ ω.1 0) ⟂ᵢ[arrayMeasure ν] fun ω ↦ ω.2 0 a := - indepFun_fst_zero_snd_zero_action ν a - rw [action_zero] - exact this.comp (φ := initAlgFunction alg) (by fun_prop) measurable_id - · fun_prop - · fun_prop - · simp - · rwa [Measure.map_apply (by fun_prop) (by simp)] at ha + HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) := by + refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ + refine (condDistrib_ae_eq_cond (by fun_prop) (by fun_prop)).trans ?_ + rw [Filter.EventuallyEq, ae_iff_of_countable] + intro a ha + simp only [reward_zero] + calc ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 (action alg 0 ω)) + _ = ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 a) := by + refine Measure.map_congr + (ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_) + intro x hx + simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx + simp [hx] + _ = ν a := by + rw [cond_of_indepFun] + · exact map_snd_apply_arrayMeasure 0 a + · have : (fun ω ↦ ω.1 0) ⟂ᵢ[arrayMeasure ν] fun ω ↦ ω.2 0 a := + indepFun_fst_zero_snd_zero_action ν a + rw [action_zero] + exact this.comp (φ := initAlgFunction alg) (by fun_prop) measurable_id + · fun_prop + · fun_prop + · simp + · rwa [Measure.map_apply (by fun_prop) (by simp)] at ha lemma hasCondDistrib_action' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) : HasCondDistrib (action alg (n + 1)) (hist alg · n) (alg.policy n) (arrayMeasure ν) := by rw [action_add_one_eq] have h_fun ω := algFunction_map alg n (hist alg ω n) - refine ⟨by fun_prop, by fun_prop, ?_⟩ - refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_ + refine ⟨by fun_prop, ?_⟩ have h_indep : (arrayMeasure ν).map (fun ω ↦ (ω.1 (n + 1), hist alg ω n)) = (ℙ).prod ((arrayMeasure ν).map (hist alg · n)) := by have h_indep' := indepFun_fst_add_one_hist alg ν n @@ -1046,7 +1045,7 @@ lemma hasCondDistrib_reward_pullCount_action change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) - refine ⟨by fun_prop, by fun_prop, ?_⟩ + refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine (condDistrib_ae_eq_cond (Measurable.prodMk (by fun_prop) (by fun_prop)) (by fun_prop)).trans ?_ rw [Filter.EventuallyEq, ae_iff_of_countable] @@ -1121,7 +1120,7 @@ lemma hasCondDistrib_reward_hist_action_pullCount change Measurable ((fun p : (probSpace 𝓐 R) × 𝓐 ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘ (fun ω : probSpace 𝓐 R ↦ (ω, action alg (n + 1) ω))) exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop) - refine ⟨by fun_prop, by fun_prop, ?_⟩ + refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine condDistrib_prod_of_forall_condDistrib_cond (by fun_prop) (by fun_prop) (by fun_prop) _ ?_ intro (a, m) ham have h_eq : ((ν.prodMkRight _).prodMkLeft _).comap (fun ω : (Iic n → 𝓐 × R) ↦ (ω, a, m)) @@ -1181,7 +1180,7 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa suffices HasCondDistrib R' (fun ω ↦ (A ω, H ω)) (ν.prodMkRight _) (arrayMeasure ν) by have h_eq : (fun ω ↦ (H ω, A ω)) = MeasurableEquiv.prodComm ∘ (fun ω ↦ (A ω, H ω)) := rfl rw [h_eq] - exact this.comp_right (κ := ν.prodMkRight _) _ + exact this.measurableEquiv_comp_right (κ := ν.prodMkRight _) _ suffices HasCondDistrib R' (fun ω ↦ ((A ω, H ω), P ω)) ((ν.prodMkRight _).prodMkRight _) (arrayMeasure ν) by -- use that `P` is measurable wrt `(A, H)` to drop it from the conditioning @@ -1198,14 +1197,14 @@ lemma hasCondDistrib_reward' (alg : Algorithm 𝓐 R) (ν : Kernel 𝓐 R) [IsMa invFun := fun x ↦ ((x.1.1, x.2), x.1.2) measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop } - exact this.comp_right e + exact this.measurableEquiv_comp_right e suffices HasCondDistrib R' (fun ω ↦ (A ω, P ω)) (ν.prodMkRight _) (arrayMeasure ν) by have h_indep : H ⟂ᵢ[(fun ω ↦ (A ω, P ω)), (by fun_prop); arrayMeasure ν] R' := (condIndepFun_reward_hist alg ν n).symm have h_condDistrib := this.condDistrib_eq rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) (by fun_prop) (by fun_prop)] at h_indep - refine ⟨by fun_prop, by fun_prop, ?_⟩ + refine hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) ?_ refine h_indep.trans ?_ rw [Filter.EventuallyEq, ae_map_iff] at h_condDistrib ⊢ · simpa only [Kernel.prodMkRight_apply] diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean index 0ac59b3e..5284ca37 100644 --- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean +++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean @@ -18,14 +18,13 @@ open scoped ENNReal NNReal namespace Bandits variable {𝓐 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] - [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : Measure Ω} [IsProbabilityMeasure P] {alg : Algorithm 𝓐 ℝ} {ν : Kernel 𝓐 ℝ} [IsMarkovKernel ν] {h_inter : IsAlgEnvSeq A R alg (stationaryEnv ν) P} local notation "𝔓" => P.prod (streamMeasure ν) -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in +omit [DecidableEq 𝓐] in lemma hasLaw_Z (a : 𝓐) (m : ℕ) : HasLaw (fun ω ↦ ω.2 m a) (ν a) 𝔓 where map_eq := by @@ -64,6 +63,8 @@ lemma condDistrib_reward'' [Countable 𝓐] filter_upwards [h_ra', h_prod] with ω h_eq h_prod rw [h_prod, h_eq] +variable [StandardBorelSpace 𝓐] + omit [DecidableEq 𝓐] in lemma reward_cond_action [Countable 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : 𝓐) (n : ℕ) @@ -81,6 +82,8 @@ lemma reward_cond_action [Countable 𝓐] rw [h_ra] at h_eq exact h_eq.symm +variable [Nonempty 𝓐] + lemma condIndepFun_reward_stepsUntil_action' [StandardBorelSpace Ω] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : 𝓐) (m n : ℕ) : R n ⟂ᵢ[A n, h.measurable_action n; P] {ω | stepsUntil A a m ω = ↑n}.indicator (fun _ ↦ 1) := by diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index ff4f58db..df979782 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -137,7 +137,6 @@ lemma snd_eval_comp_history (n : ℕ) : section IsAlgEnvSeq -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] /-- An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment. -/ @@ -246,6 +245,8 @@ lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw ( have hY := h.measurable_feedback exact (Measure.map_map (by fun_prop) (by fun_prop)).symm +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] + lemma IsAlgEnvSeq.hasLaw_history_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : HasLaw (history A Y (n + 1)) ((P.map (history A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (history A Y n) P).map diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean index 8acca0dd..ad4b00c4 100644 --- a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean @@ -89,24 +89,20 @@ variable [IsProbabilityMeasure Q] lemma hasCondDistrib_env_history (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : HasCondDistrib E (history A Y n) (condDistrib E₀ (history A₀ Y₀ n) P₀) P where - aemeasurable_fst := h.measurable_param.aemeasurable - aemeasurable_snd := - (measurable_history h.measurable_action h.measurable_feedback n).aemeasurable - condDistrib_eq := by + aemeasurable := ((measurable_history h.measurable_action + h.measurable_feedback n).prodMk h.measurable_param).aemeasurable + map_eq := by have hA := h.measurable_action have hY := h.measurable_feedback have hA₀ := h₀.measurable_action have hY₀ := h₀.measurable_feedback - have hE := h.measurable_param have hE₀ := h₀.measurable_param - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ h.measurable_param.aemeasurable, - ← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq, + rw [← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq, Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop) (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n), map_swap_withDensity_comp_snd (by fun_prop), ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop), - ← compProd_map_condDistrib (by fun_prop), - ← Measure.compProd_withDensity_left (by fun_prop), + ← compProd_map_condDistrib (by fun_prop), ← Measure.compProd_withDensity_left (by fun_prop), ← (hasLaw_history_withDensity h h₀ hc n).map_eq] end IsBayesAlgEnvSeq diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index 8f25f41e..f19bf9cc 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -33,8 +33,8 @@ open scoped Topology namespace Learning -variable {𝓐 𝓨 Ω : Type*} [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [StandardBorelSpace 𝓐] [Nonempty 𝓐] - [StandardBorelSpace 𝓨] [Nonempty 𝓨] {μ : Measure 𝓐} [IsProbabilityMeasure μ] [MeasurableSpace Ω] +variable {𝓐 𝓨 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} + {μ : Measure 𝓐} [IsProbabilityMeasure μ] {P : Measure Ω} [IsProbabilityMeasure P] open Set in @@ -65,14 +65,14 @@ lemma iIndep_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) : have hA := h.measurable_action rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)] intro n - have condDistrib_eq := (h.hasCondDistrib_action n).condDistrib_eq - simp only [randomSampling_policy] at condDistrib_eq - have law_eq := (hasLaw_action h (n + 1)).map_eq - rw [← law_eq, ← indepFun_iff_condDistrib_eq_const ?_ (by fun_prop)] at condDistrib_eq - · have meas_fst : Measurable (fun (f : Iic n → 𝓐 × 𝓨) ↦ (fun i ↦ (f i).1)) := by - fun_prop - exact (condDistrib_eq.comp meas_fst measurable_id).symm + have map_eq := (h.hasCondDistrib_action n).map_eq + simp only [randomSampling_policy, Measure.compProd_const] at map_eq + have law_eq : P.map (A (n + 1)) = μ := (hasLaw_action h (n + 1)).map_eq + rw [← law_eq, ← indepFun_iff_map_prod_eq_prod_map_map] at map_eq + · change A (n + 1) ⟂ᵢ[P] (fun (f : Iic n → 𝓐 × 𝓨) ↦ (fun i ↦ (f i).1))∘ (history A Y n) + refine map_eq.symm.comp measurable_id (by fun_prop) · exact (h.measurable_history n).aemeasurable + · exact (h.measurable_action (n + 1)).aemeasurable end randomSampling diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean index 4bebce42..2476ad31 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean @@ -86,8 +86,7 @@ end AlgorithmDefinition namespace RoundRobin -variable [StandardBorelSpace 𝓨] [Nonempty 𝓨] - {hK : 0 < K} {ν : Kernel (Fin K) 𝓨} [IsMarkovKernel ν] +variable {hK : 0 < K} {ν : Kernel (Fin K) 𝓨} [IsMarkovKernel ν] {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → Fin K} {Y : ℕ → Ω → 𝓨} diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean index c5b8b039..3a93e553 100644 --- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean @@ -56,7 +56,6 @@ variable [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [M and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting with an underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`). -/ structure IsBayesAlgEnvSeq - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (Q : Measure 𝓔) (κ : Kernel (𝓔 × 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (P : Measure Ω) [IsFiniteMeasure P] : Prop where @@ -75,7 +74,6 @@ structure IsBayesAlgEnvSeq namespace IsBayesAlgEnvSeq -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] variable {Q : Measure 𝓔} {κ : Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨} variable {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} variable {P : Measure Ω} [IsFiniteMeasure P] @@ -85,11 +83,13 @@ lemma hasLaw_action_zero [IsProbabilityMeasure P] (h : IsBayesAlgEnvSeq Q κ alg lemma hasCondDistrib_action' (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P := - (h.hasCondDistrib_action n).comp_right' (by fun_prop) + (h.hasCondDistrib_action n).comp_right lemma hasCondDistrib_feedback' [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : HasCondDistrib (Y (n + 1)) (fun ω ↦ (E ω, A (n + 1) ω)) κ P := - (h.hasCondDistrib_feedback n).comp_right' (by fun_prop) + (h.hasCondDistrib_feedback n).comp_right + +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] lemma hasLaw_IT_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ∀ᵐ e ∂Q, HasLaw (IT.action 0) alg.p0 (condDistrib (trajectory A Y) E P e) := by @@ -102,7 +102,7 @@ lemma hasLaw_IT_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : rw [← Kernel.map_apply _ (IT.measurable_action 0), ← hc, show IT.action 0 ∘ trajectory A Y = A 0 from rfl, hcd, Kernel.const_apply]⟩ -lemma hasCondDistrib_IT_feedback_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : +lemma hasCondDistrib_IT_feedback_zero [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ∀ᵐ e ∂Q, HasCondDistrib (IT.feedback 0) (IT.action 0) (κ.sectR e) (condDistrib (trajectory A Y) E P e) := by rw [← h.hasLaw_env.map_eq] @@ -127,7 +127,7 @@ lemma hasCondDistrib_IT_feedback [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ have hc : HasCondDistrib (Y (n + 1)) (fun ω ↦ (E ω, history A Y n ω, A (n + 1) ω)) (κ.comap (fun (e, _, a) ↦ (e, a)) (by fun_prop)) P := - (h.hasCondDistrib_feedback n).comp_right (MeasurableEquiv.prodAssoc.symm.trans + (h.hasCondDistrib_feedback n).measurableEquiv_comp_right (MeasurableEquiv.prodAssoc.symm.trans ((MeasurableEquiv.prodCongr .prodComm (.refl _)).trans .prodAssoc)) exact hc.hasCondDistrib_sectR ((IT.measurable_hist n).prodMk (IT.measurable_action (n + 1))) (IT.measurable_feedback (n + 1)) @@ -166,8 +166,7 @@ def bayesStationaryEnv (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (Kernel.deterministic (Prod.fst ∘ g) (by fun_prop)) ×ₖ (κ.comap g (by fun_prop)) ν0 := (Kernel.const _ Q) ⊗ₖ κ.swapLeft -variable [Nonempty 𝓐] [Nonempty 𝓔] [Nonempty 𝓨] -variable [StandardBorelSpace 𝓐] [StandardBorelSpace 𝓔] [StandardBorelSpace 𝓨] +variable [Nonempty 𝓐] [StandardBorelSpace 𝓐] variable {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × 𝓐) 𝓨} [IsMarkovKernel κ] variable {alg : Algorithm 𝓐 𝓨} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓔 × 𝓨} variable {P : Measure Ω} [IsProbabilityMeasure P] @@ -186,14 +185,14 @@ lemma IsAlgEnvSeq.isBayesAlgEnvSeq simpa [bayesStationaryEnv] using h.hasCondDistrib_feedback_zero.fst simpa [h.hasLaw_action_zero.map_eq, Algorithm.prodLeft] using hc.const_map_of_const hasCondDistrib_feedback_zero := - h.hasCondDistrib_feedback_zero.of_compProd.comp_right MeasurableEquiv.prodComm + h.hasCondDistrib_feedback_zero.of_compProd.measurableEquiv_comp_right MeasurableEquiv.prodComm hasCondDistrib_action n := by let f : (Iic n → 𝓐 × 𝓔 × 𝓨) → 𝓔 × (Iic n → 𝓐 × 𝓨) := fun h ↦ ((h ⟨0, by simp⟩).2.1, fun i ↦ ((h i).1, (h i).2.2)) have hc : HasCondDistrib (A (n + 1)) (history A Y n) (((alg.policy n).comap Prod.snd (by fun_prop)).comap f (by fun_prop)) P := h.hasCondDistrib_action n - exact hc.comp_right' (f := f) + exact hc.comp_right (f := f) hasCondDistrib_feedback n := by let f : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → (Iic n → 𝓐 × 𝓨) × 𝓔 × 𝓐 := fun p ↦ ((fun i ↦ ((p.1 i).1, (p.1 i).2.2)), (p.1 ⟨0, by simp⟩).2.1, p.2) @@ -202,7 +201,7 @@ lemma IsAlgEnvSeq.isBayesAlgEnvSeq ((Kernel.prodMkLeft ((Iic n) → 𝓐 × 𝓨) κ).comap f (by fun_prop)) P := by simpa [bayesStationaryEnv, Kernel.prodMkLeft, ← Kernel.comap_comp_right, Function.comp_def] using (h.hasCondDistrib_feedback n).snd - exact hc.comp_right' (by fun_prop) + exact hc.comp_right end IsAlgEnvSeq diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 70e0346e..0cfec6c0 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean @@ -83,7 +83,6 @@ lemma policy_eq_deterministic (alg : Algorithm 𝓐 𝓨) [h_det : IsDeterminist namespace IsDeterministicAlg variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ} @@ -93,7 +92,7 @@ lemma hasLaw_action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg] aemeasurable := have hA := h.measurable_action; by fun_prop map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg) -lemma action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg] +lemma action_zero_of_IsAlgEnvSeqUntil [StandardBorelSpace 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil A Y alg env P N) : A 0 =ᵐ[P] fun _ ↦ actionZero alg := by have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = actionZero alg := by @@ -101,8 +100,8 @@ lemma action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg] have hA := h.measurable_action exact ae_of_ae_map (by fun_prop) h_eq -lemma action_ae_eq_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg] - (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) : +lemma action_ae_eq_of_IsAlgEnvSeqUntil [StandardBorelSpace 𝓐] [Nonempty 𝓐] + [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) : A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) := by have hA := h.measurable_action have hY := h.measurable_feedback @@ -116,17 +115,19 @@ lemma hasLaw_action_zero [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y a aemeasurable := have hA := h.measurable_action; by fun_prop map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg) -lemma action_zero_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) : +lemma action_zero_ae_eq [StandardBorelSpace 𝓐] [h_det : IsDeterministicAlg alg] + (h : IsAlgEnvSeq A Y alg env P) : A 0 =ᵐ[P] fun _ ↦ actionZero alg := action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 0) -lemma action_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : +lemma action_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] [h_det : IsDeterministicAlg alg] + (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) := action_ae_eq_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil (n + 1)) (by simp) -lemma action_ae_all_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) : - ∀ᵐ ω ∂P, A 0 ω = actionZero alg ∧ - ∀ n, A (n + 1) ω = nextAction alg n (history A Y n ω) := by +lemma action_ae_all_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] [h_det : IsDeterministicAlg alg] + (h : IsAlgEnvSeq A Y alg env P) : + ∀ᵐ ω ∂P, A 0 ω = actionZero alg ∧ ∀ n, A (n + 1) ω = nextAction alg n (history A Y n ω) := by rw [eventually_and, ae_all_iff] exact ⟨action_zero_ae_eq h, action_ae_eq h⟩ @@ -171,7 +172,6 @@ lemma feedback_eq_deterministic (env : Environment 𝓐 𝓨) [IsDeterministicEn namespace IsDeterministicEnv variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {f : (n : ℕ) → ((Iic n → 𝓐 × 𝓨) × 𝓐) → 𝓨} {hf : ∀ n, Measurable (f n)} @@ -251,26 +251,25 @@ lemma feedbackFun_detEnvironment [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ namespace IsAlgEnvSeq variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν] {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} -lemma hasLaw_action_zero_detAlgorithm +lemma hasLaw_action_zero_detAlgorithm [StandardBorelSpace 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : HasLaw (A 0) (Measure.dirac action0) P := by simpa using IsDeterministicAlg.hasLaw_action_zero h -lemma action_zero_detAlgorithm +lemma action_zero_detAlgorithm [StandardBorelSpace 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : A 0 =ᵐ[P] fun _ ↦ action0 := (IsDeterministicAlg.action_zero_ae_eq h).trans (by simp) -lemma action_detAlgorithm_ae_eq +lemma action_detAlgorithm_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) (n : ℕ) : A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) := (IsDeterministicAlg.action_ae_eq h n).trans (by simp) -lemma action_detAlgorithm_ae_all_eq +lemma action_detAlgorithm_ae_all_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (history A Y n ω) := by filter_upwards [IsDeterministicAlg.action_ae_all_eq h] with ω hω using by simp [hω] @@ -280,21 +279,20 @@ end IsAlgEnvSeq namespace IsAlgEnvSeqUntil variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν] {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N n : ℕ} -lemma hasLaw_action_zero_detAlgorithm +lemma hasLaw_action_zero_detAlgorithm [StandardBorelSpace 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) : HasLaw (A 0) (Measure.dirac action0) P := by simpa using IsDeterministicAlg.hasLaw_action_zero_of_IsAlgEnvSeqUntil h -lemma action_zero_detAlgorithm +lemma action_zero_detAlgorithm [StandardBorelSpace 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) : A 0 =ᵐ[P] fun _ ↦ action0 := (IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil h).trans (by simp) -lemma action_detAlgorithm_ae_eq +lemma action_detAlgorithm_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) (hn : n < N) : A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) := (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp) diff --git a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean index bca3e668..3ab4a1f7 100644 --- a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean +++ b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean @@ -77,8 +77,7 @@ lemma feedbackFun_onlineEvalEnv [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) section OnlineEvalEnv -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] - {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {g : ℕ → 𝓐 → 𝓨} {hg : ∀ n, Measurable (g n)} {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} @@ -87,14 +86,14 @@ lemma hascondDistrib_feedback_onlineEvalEnv HasCondDistrib (Y n) (A n) (Kernel.deterministic (g n) (hg n)) P := by simpa using IsObliviousEnv.hasCondDistrib_feedback h n -lemma feedback_onlineEvalEnv_ae_eq_eval_action +lemma feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) (n : ℕ) : Y n =ᵐ[P] g n ∘ A n := ae_eq_of_condDistrib_eq_deterministic (hg n) (h.measurable_action n).aemeasurable (h.measurable_feedback n).aemeasurable (hascondDistrib_feedback_onlineEvalEnv h n).condDistrib_eq -lemma forall_feedback_onlineEvalEnv_ae_eq_eval_action +lemma forall_feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (onlineEvalEnv g hg) P) : ∀ᵐ ω ∂P, ∀ n, Y n ω = g n (A n ω) := by rw [ae_all_iff] @@ -125,22 +124,23 @@ lemma feedbackFun_evalEnv [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) : section EvalEnv -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] - {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {f : 𝓐 → 𝓨} {hf : Measurable f} {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} lemma hascondDistrib_feedback_evalEnv (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : ℕ) : HasCondDistrib (Y n) (A n) (Kernel.deterministic f hf) P := by simpa using IsObliviousEnv.hasCondDistrib_feedback h n -lemma feedback_evalEnv_ae_eq_eval_action (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : ℕ) : +lemma feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) (n : ℕ) : Y n =ᵐ[P] f ∘ A n := feedback_onlineEvalEnv_ae_eq_eval_action h n -lemma forall_feedback_evalEnv_ae_eq_eval_action (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) : +lemma forall_feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) : ∀ᵐ ω ∂P, ∀ n, Y n ω = f (A n ω) := forall_feedback_onlineEvalEnv_ae_eq_eval_action h open Finset in -lemma feedback_evalEnv_ae_eq_eval_action_comp {β : Type*} +lemma feedback_evalEnv_ae_eq_eval_action_comp {β : Type*} [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (evalEnv f hf) P) {n : ℕ} (g : (Iic n → 𝓨) → β) : ∀ᵐ ω ∂P, g (fun i ↦ Y i ω) = g (fun i ↦ f (A i ω)) := by filter_upwards [forall_feedback_evalEnv_ae_eq_eval_action h] with ω hω diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index d36d9ef8..1046fbb3 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean @@ -296,47 +296,66 @@ lemma hasLaw_action_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 rw [← fst_comp_step, ← Measure.map_map (by fun_prop) (by fun_prop), (hasLaw_step_zero alg env).map_eq, ← Measure.fst, Measure.fst_compProd] -variable [StandardBorelSpace 𝓨] [Nonempty 𝓨] - -lemma condDistrib_feedback_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : - condDistrib (feedback 0) (action 0) (trajMeasure alg env) - =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := by +lemma hasCondDistrib_feedback_zero (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : + HasCondDistrib (feedback 0) (action 0) env.ν0 (trajMeasure alg env) := by have h_step := (hasLaw_step_zero alg env).map_eq have h_action := (hasLaw_action_zero alg env).map_eq - rwa [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h_action] + exact ⟨by fun_prop, by rwa [h_action]⟩ + +lemma _root_.ProbabilityTheory.Kernel.hasCondDistrib_trajMeasure + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + HasCondDistrib (step (n + 1)) (hist n) (stepKernel alg env n) (trajMeasure alg env) := + ⟨by fun_prop, Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure.symm⟩ + +lemma hasCondDistrib_step (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + HasCondDistrib (step (n + 1)) (hist n) (stepKernel alg env n) (trajMeasure alg env) := + Kernel.hasCondDistrib_trajMeasure alg env n + +lemma hasCondDistrib_action (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + HasCondDistrib (action (n + 1)) (hist n) (alg.policy n) (trajMeasure alg env) := by + rw [← fst_comp_step, ← fst_stepKernel, Kernel.fst_eq] + exact HasCondDistrib.comp_left (hasCondDistrib_step alg env n) measurable_fst + +lemma hasCondDistrib_feedback (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + HasCondDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (env.feedback n) + (trajMeasure alg env) := by + have h_step := hasCondDistrib_step alg env n + have h_action := hasCondDistrib_action alg env n + refine ⟨by fun_prop, ?_⟩ + rw [h_action.map_eq, ← Measure.compProd_assoc, ← stepKernel, ← h_step.map_eq, + Measure.map_map (by fun_prop) (by fun_prop)] + rfl + +lemma condDistrib_feedback_zero [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : + condDistrib (feedback 0) (action 0) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := + (hasCondDistrib_feedback_zero alg env).condDistrib_eq -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] +lemma condDistrib_feedback [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + condDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := + (hasCondDistrib_feedback alg env n).condDistrib_eq -lemma condDistrib_step (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : +lemma condDistrib_step [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : condDistrib (step (n + 1)) (hist n) (trajMeasure alg env) =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n := - Kernel.condDistrib_trajMeasure + (hasCondDistrib_step alg env n).condDistrib_eq -lemma condDistrib_action (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : +lemma condDistrib_action [StandardBorelSpace 𝓐] [Nonempty 𝓐] + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : condDistrib (action (n + 1)) (hist n) (trajMeasure alg env) - =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by - rw [← fst_comp_step] - refine (condDistrib_comp _ (by fun_prop) (by fun_prop)).trans ?_ - filter_upwards [condDistrib_step alg env n] with h h_eq - rw [Kernel.map_apply _ (by fun_prop), h_eq, ← Kernel.map_apply _ (by fun_prop), ← Kernel.fst_eq, - fst_stepKernel] - -lemma condDistrib_feedback (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : - condDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) - =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by - have h_step := condDistrib_step alg env n - have h_action := condDistrib_action alg env n - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_step h_action ⊢ - rw [h_action, ← Measure.compProd_assoc, ← stepKernel, ← h_step, - Measure.map_map (by fun_prop) (by fun_prop)] - rfl + =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := + (hasCondDistrib_action alg env n).condDistrib_eq lemma isAlgEnvSeq_trajMeasure (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : IsAlgEnvSeq action feedback alg env (trajMeasure alg env) where hasLaw_action_zero := hasLaw_action_zero alg env - hasCondDistrib_feedback_zero := ⟨by fun_prop, by fun_prop, condDistrib_feedback_zero alg env⟩ - hasCondDistrib_action n := ⟨by fun_prop, by fun_prop, condDistrib_action alg env n⟩ - hasCondDistrib_feedback n := ⟨by fun_prop, by fun_prop, condDistrib_feedback alg env n⟩ + hasCondDistrib_feedback_zero := hasCondDistrib_feedback_zero alg env + hasCondDistrib_action n := hasCondDistrib_action alg env n + hasCondDistrib_feedback n := hasCondDistrib_feedback alg env n end Laws diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean index 1efdce54..39539bd7 100644 --- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean @@ -73,7 +73,6 @@ lemma feedback_eq_feedbackCondAction (env : Environment 𝓐 𝓨) [IsObliviousE namespace IsObliviousEnv variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ} {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)] @@ -85,9 +84,8 @@ lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env cases n with | zero => rw [← ν0_eq_feedbackCondAction]; exact h.hasCondDistrib_feedback_zero | succ n => - refine ⟨by fun_prop, by fun_prop, ?_⟩ - have h_eq := (h.hasCondDistrib_feedback n).condDistrib_eq - rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_eq ⊢ + refine ⟨by fun_prop, ?_⟩ + have h_eq := (h.hasCondDistrib_feedback n).map_eq have : P.map (A (n + 1)) = (P.map (fun x ↦ (history A Y n x, A (n + 1) x))).snd := by rw [Measure.snd_map_prodMk (by fun_prop)] @@ -96,6 +94,8 @@ lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env Measure.snd_map_prodMk (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)] congr +variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] + /-- The feedback at time `n + 1` is conditionally independent of the history up to time `n` given the action at time `n + 1`. -/ lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω] @@ -186,7 +186,6 @@ lemma feedbackCondAction_stationaryEnv (ν : Kernel 𝓐 𝓨) [hν : IsMarkovKe feedbackCondAction (stationaryEnv ν) n = ν := feedbackCondAction_obliviousEnv _ _ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν] {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} @@ -199,7 +198,7 @@ lemma hasCondDistrib_feedback_stationaryEnv simpa using IsObliviousEnv.hasCondDistrib_feedback h n /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/ -lemma condDistrib_feedback_stationaryEnv +lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) : condDistrib (Y n) (A n) P =ᵐ[P.map (A n)] ν := (hasCondDistrib_feedback_stationaryEnv h n).condDistrib_eq @@ -207,17 +206,20 @@ lemma condDistrib_feedback_stationaryEnv /-- The feedback at time `n + 1` is conditionally independent of the history up to time `n` given the action at time `n + 1`. -/ lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω] + [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) : Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action _ ; P] history A Y n := IsObliviousEnv.condIndepFun_feedback_history_action h n lemma condIndepFun_feedback_history_action_action [StandardBorelSpace Ω] + [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) : Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action (n + 1); P] (fun ω ↦ (history A Y n ω, A (n + 1) ω)) := IsObliviousEnv.condIndepFun_feedback_history_action_action h n lemma condIndepFun_feedback_history_action_action' [StandardBorelSpace Ω] + [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) (hn : n ≠ 0) : Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ (history A Y (n - 1) ω, A n ω)) := IsObliviousEnv.condIndepFun_feedback_history_action_action' h n hn From 1bfa4e2d88bde110ec90e0439001ee78c2a8e22c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 16:13:34 +0200 Subject: [PATCH 2/6] history_succ --- .../SequentialLearning/Algorithm.lean | 26 ++++++------------- .../SequentialLearning/AlgorithmDensity.lean | 24 ++++++++++------- 2 files changed, 23 insertions(+), 27 deletions(-) diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index df979782..e5eb2451 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -135,6 +135,14 @@ lemma fst_eval_comp_history (n : ℕ) : lemma snd_eval_comp_history (n : ℕ) : (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (history A Y n) = Y n := rfl +lemma history_succ (n : ℕ) : + history A Y (n + 1) = + (MeasurableEquiv.IicSuccProd (fun ℕ ↦ 𝓐 × 𝓨) n).symm ∘ + (fun ω ↦ (history A Y n ω, step A Y (n + 1) ω)) := by + funext ω + symm + exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (history A Y (n + 1) ω) + section IsAlgEnvSeq @@ -245,24 +253,6 @@ lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw ( have hY := h.measurable_feedback exact (Measure.map_map (by fun_prop) (by fun_prop)).symm -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] - -lemma IsAlgEnvSeq.hasLaw_history_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : - HasLaw (history A Y (n + 1)) - ((P.map (history A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (history A Y n) P).map - (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm) P where - aemeasurable := (h.measurable_history (n + 1)).aemeasurable - map_eq := by - have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm ∘ - (fun ω ↦ (history A Y n ω, step A Y (n + 1) ω)) = history A Y (n + 1) := by - funext ω - exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (history 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 120f0fd9..b54a6841 100644 --- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean @@ -84,7 +84,6 @@ open scoped Algorithm namespace IsAlgEnvSeq variable {Ω : Type*} [MeasurableSpace Ω] -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] variable {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} variable {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} variable {P : Measure Ω} [IsFiniteMeasure P] @@ -104,13 +103,18 @@ lemma absolutelyContinuous_map_history (h : IsAlgEnvSeq A Y alg env P) 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_history_succ n).map_eq, (h₀.hasLaw_history_succ n).map_eq] + simp_rw [history_succ] + rw [← Measure.map_map (by fun_prop), ← Measure.map_map (by fun_prop)] + rotate_left + · exact (h₀.measurable_history n).prodMk (h₀.measurable_step (n + 1)) + · exact (h.measurable_history n).prodMk (h.measurable_step (n + 1)) 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] + rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_eq] apply Measure.AbsolutelyContinuous.compProd ih filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _ +variable [MeasurableSpace.CountablyGenerated 𝓐] + lemma hasLaw_history_withDensity (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (history A Y n) ((P₀.map (history A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where @@ -131,12 +135,14 @@ lemma hasLaw_history_withDensity (h : IsAlgEnvSeq A Y alg env P) have : IsMarkovKernel ((stepKernel alg₀ env n).withDensity ρ) := by rw [← hs] infer_instance - rw [(h.hasLaw_history_succ n).map_eq, (h₀.hasLaw_history_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)] + simp_rw [history_succ] + rw [← Measure.map_map (by fun_prop), ← Measure.map_map (by fun_prop)] + rotate_left + · exact (h₀.measurable_history n).prodMk (h₀.measurable_step (n + 1)) + · exact (h.measurable_history n).prodMk (h.measurable_step (n + 1)) + rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_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 5740f95ef9375a3710467d76644e0d44f15ecc28 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 16:34:34 +0200 Subject: [PATCH 3/6] StandardBorelSpace -> MeasurableEq --- .../Probability/HasCondDistrib.lean | 9 ++++++ .../Probability/Independence/CondDistrib.lean | 16 +++++----- .../SequentialLearning/Deterministic.lean | 32 +++++++++---------- 3 files changed, 32 insertions(+), 25 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index 033b8dae..b60621ad 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -138,6 +138,15 @@ lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ] AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] rfl +lemma ae_eq_of_hasCondDistrib_deterministic [MeasurableEq Ω] [SFinite μ] {f : β → Ω} + (hf : Measurable f) (hX : AEMeasurable X μ) + (hY : AEMeasurable Y μ) (h : HasCondDistrib Y X (Kernel.deterministic f hf) μ) : + Y =ᵐ[μ] f ∘ X := by + refine ae_eq_of_map_prodMk_eq hf hX hY ?_ + rw [h.map_eq, Measure.compProd_deterministic, + AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] + rfl + variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempty Ω'] lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ] diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean index 90d24c0f..9925b4e2 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean @@ -400,14 +400,14 @@ lemma indepFun_snd_prod (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h_ind rfl -- cf. measurableSet_graph (Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean) -lemma measurableSet_graph' {β Ω : Type*} [MeasurableSpace β] [MeasurableSpace Ω] - [StandardBorelSpace Ω] {f : β → Ω} (hf : Measurable f) : - MeasurableSet {p : β × Ω | p.2 = f p.1} := by - letI := upgradeStandardBorel Ω - exact (measurable_snd.prodMk (by fun_prop)) isClosed_diagonal.measurableSet - -omit [Nonempty Ω] [IsFiniteMeasure μ] in -lemma ae_eq_of_map_prodMk_eq {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ) +lemma measurableSet_graph' {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω} + [MeasurableEq Ω] {f : β → Ω} (hf : Measurable f) : + MeasurableSet {p : β × Ω | p.2 = f p.1} := + measurableSet_eq_fun (by fun_prop) (by fun_prop) + +omit [IsFiniteMeasure μ] in +lemma ae_eq_of_map_prodMk_eq {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω} + [MeasurableEq Ω] {X : α → β} {Y : α → Ω} {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h : μ.map (fun ω ↦ (X ω, Y ω)) = μ.map (fun ω ↦ (X ω, f (X ω)))) : Y =ᵐ[μ] f ∘ X := by have hp : ∀ᵐ p ∂μ.map (fun ω ↦ (X ω, f (X ω))), p.2 = f p.1 := diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 0cfec6c0..abbcfffa 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean @@ -92,7 +92,7 @@ lemma hasLaw_action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg] aemeasurable := have hA := h.measurable_action; by fun_prop map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg) -lemma action_zero_of_IsAlgEnvSeqUntil [StandardBorelSpace 𝓐] [h_det : IsDeterministicAlg alg] +lemma action_zero_of_IsAlgEnvSeqUntil [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil A Y alg env P N) : A 0 =ᵐ[P] fun _ ↦ actionZero alg := by have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = actionZero alg := by @@ -100,32 +100,30 @@ lemma action_zero_of_IsAlgEnvSeqUntil [StandardBorelSpace 𝓐] [h_det : IsDeter have hA := h.measurable_action exact ae_of_ae_map (by fun_prop) h_eq -lemma action_ae_eq_of_IsAlgEnvSeqUntil [StandardBorelSpace 𝓐] [Nonempty 𝓐] +lemma action_ae_eq_of_IsAlgEnvSeqUntil [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) : A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) := by - have hA := h.measurable_action - have hY := h.measurable_feedback - have h_eq := (h.hasCondDistrib_action n hn).condDistrib_eq + have h_eq := (h.hasCondDistrib_action n hn) rw [policy_eq_deterministic alg n] at h_eq - refine ae_eq_of_condDistrib_eq_deterministic (by fun_prop : Measurable (nextAction alg n)) - (by fun_prop) (by fun_prop) h_eq + exact ae_eq_of_hasCondDistrib_deterministic (measurable_nextAction _ _) (by fun_prop) + (by fun_prop) h_eq lemma hasLaw_action_zero [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) : HasLaw (A 0) (Measure.dirac (actionZero alg)) P where aemeasurable := have hA := h.measurable_action; by fun_prop map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg) -lemma action_zero_ae_eq [StandardBorelSpace 𝓐] [h_det : IsDeterministicAlg alg] +lemma action_zero_ae_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) : A 0 =ᵐ[P] fun _ ↦ actionZero alg := action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 0) -lemma action_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] [h_det : IsDeterministicAlg alg] +lemma action_ae_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) : A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) := action_ae_eq_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil (n + 1)) (by simp) -lemma action_ae_all_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] [h_det : IsDeterministicAlg alg] +lemma action_ae_all_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) : ∀ᵐ ω ∂P, A 0 ω = actionZero alg ∧ ∀ n, A (n + 1) ω = nextAction alg n (history A Y n ω) := by rw [eventually_and, ae_all_iff] @@ -254,22 +252,22 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν] {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} -lemma hasLaw_action_zero_detAlgorithm [StandardBorelSpace 𝓐] +lemma hasLaw_action_zero_detAlgorithm [MeasurableEq 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : HasLaw (A 0) (Measure.dirac action0) P := by simpa using IsDeterministicAlg.hasLaw_action_zero h -lemma action_zero_detAlgorithm [StandardBorelSpace 𝓐] +lemma action_zero_detAlgorithm [MeasurableEq 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : A 0 =ᵐ[P] fun _ ↦ action0 := (IsDeterministicAlg.action_zero_ae_eq h).trans (by simp) -lemma action_detAlgorithm_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] +lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) (n : ℕ) : A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) := (IsDeterministicAlg.action_ae_eq h n).trans (by simp) -lemma action_detAlgorithm_ae_all_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] +lemma action_detAlgorithm_ae_all_eq [MeasurableEq 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) : ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (history A Y n ω) := by filter_upwards [IsDeterministicAlg.action_ae_all_eq h] with ω hω using by simp [hω] @@ -282,17 +280,17 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν] {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N n : ℕ} -lemma hasLaw_action_zero_detAlgorithm [StandardBorelSpace 𝓐] +lemma hasLaw_action_zero_detAlgorithm [MeasurableEq 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) : HasLaw (A 0) (Measure.dirac action0) P := by simpa using IsDeterministicAlg.hasLaw_action_zero_of_IsAlgEnvSeqUntil h -lemma action_zero_detAlgorithm [StandardBorelSpace 𝓐] +lemma action_zero_detAlgorithm [MeasurableEq 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) : A 0 =ᵐ[P] fun _ ↦ action0 := (IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil h).trans (by simp) -lemma action_detAlgorithm_ae_eq [StandardBorelSpace 𝓐] [Nonempty 𝓐] +lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐] [Nonempty 𝓐] (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) (hn : n < N) : A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) := (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp) From c4d7821b40e5884215586189c1f71cff699856f5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 16:54:03 +0200 Subject: [PATCH 4/6] empty line --- LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean index b54a6841..311fd885 100644 --- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean @@ -143,6 +143,7 @@ lemma hasLaw_history_withDensity (h : IsAlgEnvSeq A Y alg env P) rw [(h.hasCondDistrib_step n).map_eq, (h₀.hasCondDistrib_step n).map_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 af9f394b6f4789d9b0fad0ff9f13464823e64eb7 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 16:56:08 +0200 Subject: [PATCH 5/6] reduce diff --- .../SequentialLearning/IonescuTulceaSpace.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index 1046fbb3..de72c256 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean @@ -332,12 +332,6 @@ lemma condDistrib_feedback_zero [StandardBorelSpace 𝓨] [Nonempty 𝓨] =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := (hasCondDistrib_feedback_zero alg env).condDistrib_eq -lemma condDistrib_feedback [StandardBorelSpace 𝓨] [Nonempty 𝓨] - (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : - condDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) - =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := - (hasCondDistrib_feedback alg env n).condDistrib_eq - lemma condDistrib_step [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : condDistrib (step (n + 1)) (hist n) (trajMeasure alg env) @@ -350,6 +344,12 @@ lemma condDistrib_action [StandardBorelSpace 𝓐] [Nonempty 𝓐] =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := (hasCondDistrib_action alg env n).condDistrib_eq +lemma condDistrib_feedback [StandardBorelSpace 𝓨] [Nonempty 𝓨] + (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : + condDistrib (feedback (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env) + =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := + (hasCondDistrib_feedback alg env n).condDistrib_eq + lemma isAlgEnvSeq_trajMeasure (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : IsAlgEnvSeq action feedback alg env (trajMeasure alg env) where hasLaw_action_zero := hasLaw_action_zero alg env From 796116b5690b6bc0665fa116e478d67ad00f326e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 20 Jun 2026 17:32:06 +0200 Subject: [PATCH 6/6] remove StandardBorelSpace --- .../Kernel/IonescuTulcea/Traj.lean | 31 +++++----- .../Online/Bandit/SumRewards.lean | 56 +++++++++---------- .../IonescuTulceaSpace.lean | 5 +- 3 files changed, 44 insertions(+), 48 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean index 9cc32932..c620a2d6 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean @@ -67,7 +67,7 @@ lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} : (MeasurableEquiv.refl α : α → α) = id := rfl set_option backward.isDefEq.respectTransparency false in -lemma hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] +lemma hasLaw_Iic_of_forall_hasCondDistrib' {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ} (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) (hn : n ≤ N) : @@ -121,8 +121,7 @@ lemma hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [ congr simp [MeasurableEquiv.coe_refl] -lemma hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] - {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) +lemma hasLaw_Iic_of_forall_hasCondDistrib {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) (n : ℕ) : HasLaw (fun ω (i : Iic n) ↦ Y i ω) @@ -136,27 +135,25 @@ lemma trajMeasure_map_frestrictLe (n : ℕ) : rw [trajMeasure, ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, Kernel.deterministic_comp_eq_map, traj_map_frestrictLe] -lemma eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] - {Y : (n : ℕ) → Ω → X n} - (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ} +lemma eq_trajMeasure_map_frestrictLe {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ} (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) : P.map (fun ω (n : Iic N) ↦ Y n ω) = (trajMeasure μ₀ κ).map (frestrictLe N) := by rw [(hasLaw_Iic_of_forall_hasCondDistrib' h0 h_condDistrib le_rfl).map_eq, trajMeasure_map_frestrictLe] --- todo: switch to `HasLaw` /-- Uniqueness of `trajMeasure`. -/ -lemma eq_trajMeasure [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] - {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n)) +lemma hasLaw_trajMeasure {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n)) (h0 : HasLaw (Y 0) μ₀ P) (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) : - P.map (fun ω n ↦ Y n ω) = trajMeasure μ₀ κ := by - refine IsProjectiveLimit.unique (P := fun (J : Finset ℕ) ↦ P.map (fun ω (i : J) ↦ Y i ω)) ?_ ?_ - · exact isProjectiveLimit_map (by fun_prop) - rw [isProjectiveLimit_nat_iff] - swap; · exact isProjectiveMeasureFamily_map_restrict (by fun_prop) - intro n - rw [(hasLaw_Iic_of_forall_hasCondDistrib h0 h_condDistrib n).map_eq, - trajMeasure_map_frestrictLe] + HasLaw (fun ω n ↦ Y n ω) (trajMeasure μ₀ κ) P where + aemeasurable := by fun_prop + map_eq := by + refine IsProjectiveLimit.unique (P := fun (J : Finset ℕ) ↦ P.map (fun ω (i : J) ↦ Y i ω)) ?_ ?_ + · exact isProjectiveLimit_map (by fun_prop) + rw [isProjectiveLimit_nat_iff] + swap; · exact isProjectiveMeasureFamily_map_restrict (by fun_prop) + intro n + rw [(hasLaw_Iic_of_forall_hasCondDistrib h0 h_condDistrib n).map_eq, + trajMeasure_map_frestrictLe] end ProbabilityTheory.Kernel diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean index 7a455c64..77b73365 100644 --- a/LeanMachineLearning/Online/Bandit/SumRewards.lean +++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean @@ -150,10 +150,8 @@ lemma pullCount_eq_comp : ext simp [pullCount] -variable [StandardBorelSpace 𝓐] [Nonempty 𝓐] - -- todo: write those lemmas with IdentDistrib instead of equality of maps -lemma _root_.Learning.IsAlgEnvSeq.law_sumRewards_unique +lemma _root_.Learning.IsAlgEnvSeq.law_sumRewards_unique [MeasurableSingletonClass 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : P.map (sumRewards A R a n) = P'.map (sumRewards A₂ R₂ a n) := by @@ -166,14 +164,12 @@ lemma _root_.Learning.IsAlgEnvSeq.law_sumRewards_unique ← sumRewards_eq_comp] · refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop) exact (measurableSet_singleton _).preimage (by fun_prop) - · rw [measurable_pi_iff] - exact fun n ↦ Measurable.prodMk (hA2 n) (hR2 n) + · fun_prop · refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop) exact (measurableSet_singleton _).preimage (by fun_prop) - · rw [measurable_pi_iff] - exact fun n ↦ Measurable.prodMk (hA n) (hR n) + · fun_prop -lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' +lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' [MeasurableSingletonClass 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : IdentDistrib (fun ω a ↦ (pullCount A a n ω, sumRewards A R a n ω)) @@ -219,14 +215,14 @@ lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' · rw [measurable_pi_iff] exact fun n ↦ Measurable.prodMk (hA n) (hR n) -lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique +lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique [MeasurableSingletonClass 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : P.map (fun ω ↦ (pullCount A a n ω, sumRewards A R a n ω)) = P'.map (fun ω ↦ (pullCount A₂ a n ω, sumRewards A₂ R₂ a n ω)) := ((h1.law_pullCount_sumRewards_unique' h2 (n := n)).comp (u := fun f ↦ f a) (by fun_prop)).map_eq -lemma _root_.Learning.IsAlgEnvSeq.identDistrib_pullCount_sumRewards +lemma _root_.Learning.IsAlgEnvSeq.identDistrib_pullCount_sumRewards [MeasurableSingletonClass 𝓐] (h1 : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (h2 : IsAlgEnvSeq A₂ R₂ alg (stationaryEnv ν) P') : IdentDistrib (fun ω n a ↦ (pullCount A a n ω, sumRewards A R a n ω)) @@ -255,8 +251,10 @@ lemma _root_.Learning.IsAlgEnvSeq.identDistrib_pullCount_sumRewards rw [hc1, hc2] exact (h1.identDistrib_trajectory h2).comp hf +variable [Nonempty 𝓐] + -- this is what we will use for UCB -lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] +lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) : P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ @@ -278,7 +276,7 @@ lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := ArrayModel.prob_pullCount_prod_sumRewards_mem_le a n hs -lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] +lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : P {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ @@ -297,7 +295,8 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] exists_eq_right, mem_filter, mem_range] at hk simp [hk.2.1] -lemma prob_sumRewards_mem_le [Countable 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) +lemma prob_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {B : Set ℝ} (hB : MeasurableSet B) : P (sumRewards A R a n ⁻¹' B) ≤ ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by @@ -307,7 +306,7 @@ lemma prob_sumRewards_mem_le [Countable 𝓐] (h : IsAlgEnvSeq A R alg (stationa convert h_le rfl -lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] +lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {m : ℕ} (hm : m ≤ n) {B : Set ℝ} (hB : MeasurableSet B) : P {ω | pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤ @@ -316,7 +315,7 @@ lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] have hm' : m < n + 1 := by lia simpa [hm'] using h_le -lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] +lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : 𝓐) (m : ℕ) {B : Set ℝ} (hB : MeasurableSet B) : P {ω | ∃ n, pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤ @@ -333,7 +332,8 @@ lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] (ArrayModel.isAlgEnvSeq_arrayMeasure alg ν)).measure_mem_eq hs _ ≤ _ := ArrayModel.prob_exists_pullCount_eq_and_sumRewards_mem_le a m hB -lemma probReal_sumRewards_le_sumRewards_le [Fintype 𝓐] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) +lemma probReal_sumRewards_le_sumRewards_le [Fintype 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : 𝓐) (n m₁ m₂ : ℕ) : P.real {ω | pullCount A (bestArm ν) n ω = m₁ ∧ pullCount A a n ω = m₂ ∧ sumRewards A R (bestArm ν) n ω ≤ sumRewards A R a n ω} ≤ @@ -369,7 +369,7 @@ section Subgaussian namespace StreamMeasure -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] +omit [DecidableEq 𝓐] [Nonempty 𝓐] lemma prob_sum_range_sub_ge_le_of_HasSubgaussianMGF {σ2 : ℝ≥0} (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) : @@ -430,8 +430,8 @@ lemma prob_sum_range_sub_le_le_of_HasSubgaussianMGF' {σ2 : ℝ≥0} (hσ2 : 0 < end StreamMeasure -lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] {σ2 : ℝ≥0} (hσ2 : 0 < σ2) - (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) +lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤ sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} ≤ ENNReal.ofReal ((n - 1) * δ) := @@ -464,8 +464,8 @@ lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] {σ2 : ℝ≥0} ( Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hn)] ring_nf -lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] {σ2 : ℝ≥0} (hσ2 : 0 < σ2) - (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) +lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ sumRewards A R a t ω - pullCount A a t ω * (ν a)[id] ≤ @@ -499,8 +499,8 @@ lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] {σ2 : ℝ≥0} ( Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hn)] ring_nf -lemma prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype [Fintype 𝓐] {σ2 : ℝ≥0} (hσ2 : 0 < σ2) - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) +lemma prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype [Fintype 𝓐] [MeasurableSingletonClass 𝓐] + {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) : P {ω | ∃ a, ∃ t < n, pullCount A a t ω ≠ 0 ∧ √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤ @@ -518,7 +518,7 @@ lemma prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype [Fintype 𝓐] {σ2 : rw [sum_const, Finset.card_univ, ← ENNReal.ofReal_nsmul, nsmul_eq_mul] ring_nf -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] in +omit [DecidableEq 𝓐] in lemma probReal_sum_le_sum_streamMeasure [Fintype 𝓐] {c : ℝ≥0} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (a : 𝓐) (m : ℕ) : (streamMeasure ν).real @@ -549,7 +549,7 @@ lemma probReal_sum_le_sum_streamMeasure [Fintype 𝓐] {c : ℝ≥0} field_simp ring -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in +omit [DecidableEq 𝓐] [Nonempty 𝓐] in lemma prob_sum_le_sqrt_log {σ2 : ℝ≥0} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : @@ -577,7 +577,7 @@ lemma prob_sum_le_sqrt_log {σ2 : ℝ≥0} ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)] norm_cast -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in +omit [DecidableEq 𝓐] [Nonempty 𝓐] in lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : @@ -607,7 +607,7 @@ lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0} open Real -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in +omit [DecidableEq 𝓐] [Nonempty 𝓐] in lemma prob_avg_add_sqrt_log_le {σ2 : ℝ≥0} {c : ℝ} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : @@ -633,7 +633,7 @@ lemma prob_avg_add_sqrt_log_le {σ2 : ℝ≥0} {c : ℝ} sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm] _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk -omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in +omit [DecidableEq 𝓐] [Nonempty 𝓐] in lemma prob_avg_sub_sqrt_log_ge {σ2 : ℝ≥0} {c : ℝ} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean index de72c256..4112eb5f 100644 --- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean +++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean @@ -45,7 +45,6 @@ deriving IsProbabilityMeasure section ModelEquivalence variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} - [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} {N : ℕ} @@ -53,8 +52,8 @@ variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω' lemma eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) : P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by rw [trajMeasure] - have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P) - (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_) + have h := (Kernel.hasLaw_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P) + (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)).map_eq · exact h · have hA := h.measurable_action n have hR := h.measurable_feedback n