From 32ba3e52a1e2f882664b7f940975e4393866a673 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 17 Dec 2025 15:13:28 +0100 Subject: [PATCH 1/2] Update Mathlib --- LeanBandits/AlgorithmBuilding.lean | 3 +- LeanBandits/BanditAlgorithms/ETC.lean | 3 +- LeanBandits/ForMathlib/IndepFun.lean | 47 ++++++-- LeanBandits/ForMathlib/KernelSub.lean | 4 +- LeanBandits/ForMathlib/SubGaussian.lean | 113 +----------------- LeanBandits/ForMathlib/Traj.lean | 84 ++----------- LeanBandits/RewardByCountMeasure.lean | 2 +- LeanBandits/SequentialLearning/Algorithm.lean | 5 +- blueprint/lean_decls | 2 +- blueprint/src/chapters/algorithm.tex | 2 +- lake-manifest.json | 22 ++-- lean-toolchain | 2 +- 12 files changed, 69 insertions(+), 220 deletions(-) diff --git a/LeanBandits/AlgorithmBuilding.lean b/LeanBandits/AlgorithmBuilding.lean index 4cb518dd..1e1df9f5 100644 --- a/LeanBandits/AlgorithmBuilding.lean +++ b/LeanBandits/AlgorithmBuilding.lean @@ -5,7 +5,8 @@ Authors: Rémy Degenne -/ import Mathlib.Analysis.Normed.Ring.Basic import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic -import Mathlib.Topology.Compactness.PseudometrizableLindelof +import Mathlib.Topology.Compactness.Lindelof +import Mathlib.Topology.Metrizable.Basic /-! # Tools to build bandit algorithms diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanBandits/BanditAlgorithms/ETC.lean index 3e85e1ce..d3a70c67 100644 --- a/LeanBandits/BanditAlgorithms/ETC.lean +++ b/LeanBandits/BanditAlgorithms/ETC.lean @@ -375,8 +375,7 @@ lemma expectation_pullCount_le (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - ( rw [integrable_indicator_iff] · exact integrableOn_const · exact (measurableSet_singleton _).preimage (by fun_prop) - simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul, neg_mul, - add_le_add_iff_left, ge_iff_le] + simp only [integral_const, probReal_univ, smul_eq_mul, one_mul, neg_mul, add_le_add_iff_left] gcongr · norm_cast simp diff --git a/LeanBandits/ForMathlib/IndepFun.lean b/LeanBandits/ForMathlib/IndepFun.lean index f5e287b4..15901bd4 100644 --- a/LeanBandits/ForMathlib/IndepFun.lean +++ b/LeanBandits/ForMathlib/IndepFun.lean @@ -9,22 +9,45 @@ variable {α Ω Ω' E ι : Type*} [Countable ι] {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {mE : MeasurableSpace E} {μ ν : Measure Ω} -lemma iIndepFun_nat_iff_forall_indepFun {X : ℕ → Ω → E} (hX : ∀ n, AEMeasurable (X n) μ) : +lemma iIndepFun_nat_iff_forall_indepFun [IsProbabilityMeasure μ] {X : ℕ → Ω → E} + (hX : ∀ n, AEMeasurable (X n) μ) : iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by constructor · intro h n - have h' := h.indepFun_finset₀ {n + 1} (Iic n) (by simp) hX - let f : (({n + 1} : Finset ℕ) → E) → E := fun x ↦ x ⟨n + 1, by simp⟩ - have hf : Measurable f := by unfold f; fun_prop - have h_eq : X (n + 1) = f ∘ (fun ω (i : ({n + 1} : Finset ℕ)) ↦ X i ω) := rfl - exact h'.comp (ψ := id) hf measurable_id + exact (h.indepFun_finset₀ {n + 1} (Iic n) (by simp) hX).comp + (measurable_pi_apply ⟨n + 1, by simp⟩) measurable_id · intro h - suffices ∀ n, iIndepFun ((Iic n).restrict X) μ by - rw [iIndepFun_iff_finset] - intro s - sorry - intro n - sorry + rw [iIndepFun_iff_measure_inter_preimage_eq_mul] + intro s sets hsets + induction s using Finset.strongInductionOn with + | _ s ih => + obtain rfl | hs := s.eq_empty_or_nonempty + · simp + · obtain hn_zero | hn_pos := (s.max' hs).eq_zero_or_pos + · simp [eq_singleton_iff_unique_mem.mpr ⟨hn_zero ▸ max'_mem _ hs, + fun j hj => Nat.le_zero.mp (hn_zero ▸ le_max' _ j hj)⟩] + · have hs'_le : ∀ i ∈ s.erase (s.max' hs), i ∈ Iic (s.max' hs - 1) := fun i hi => + mem_Iic.mpr (Nat.lt_succ_iff.mp (Nat.succ_pred_eq_of_pos hn_pos ▸ + lt_max'_of_mem_erase_max' _ hs hi)) + let t : Set (Iic (s.max' hs - 1) → E) := + {f | ∀ i : s.erase (s.max' hs), f ⟨i.1, hs'_le i.1 i.2⟩ ∈ sets i.1} + have ht : MeasurableSet t := by + have : t = ⋂ i : s.erase (s.max' hs), (· ⟨i.1, hs'_le i.1 i.2⟩) ⁻¹' sets i.1 := by + ext + simp [t] + exact this ▸ .iInter fun ⟨i, hi⟩ => + (hsets i (erase_subset _ _ hi)).preimage (measurable_pi_apply _) + have heq : ⋂ i ∈ s.erase (s.max' hs), X i ⁻¹' sets i = + (fun ω (j : Iic (s.max' hs - 1)) => X j ω) ⁻¹' t := by + ext ω + simp only [Set.mem_iInter, Set.mem_preimage, t] + exact ⟨fun hω ⟨i, hi⟩ => hω i hi, fun hω i hi => hω ⟨i, hi⟩⟩ + have hind := h (s.max' hs - 1) + rw [Nat.sub_add_cancel hn_pos] at hind + rw [(insert_erase (max'_mem _ hs)).symm, set_biInter_insert, heq, + hind.measure_inter_preimage_eq_mul _ _ (hsets _ (max'_mem _ hs)) ht, ← heq, + ih _ (erase_ssubset (max'_mem _ hs)) fun i hi => hsets i (erase_subset _ _ hi), + prod_insert (notMem_erase _ _)] -- todo: kernel version? lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f : Ω → Ω'} diff --git a/LeanBandits/ForMathlib/KernelSub.lean b/LeanBandits/ForMathlib/KernelSub.lean index 16e5886d..cb0c3461 100644 --- a/LeanBandits/ForMathlib/KernelSub.lean +++ b/LeanBandits/ForMathlib/KernelSub.lean @@ -250,9 +250,9 @@ lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] : rw [h_sing] exact measurableSet_mutuallySingular κ κ -lemma measurableSet_eq [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] - (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : +lemma measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : MeasurableSet {a | κ a = η a} := by + classical have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by ext1 a simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le] diff --git a/LeanBandits/ForMathlib/SubGaussian.lean b/LeanBandits/ForMathlib/SubGaussian.lean index 9d63efca..34f628f3 100644 --- a/LeanBandits/ForMathlib/SubGaussian.lean +++ b/LeanBandits/ForMathlib/SubGaussian.lean @@ -10,119 +10,10 @@ open scoped ENNReal NNReal namespace ProbabilityTheory -theorem mgf_const_mul {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} - {t : ℝ} (α : ℝ) : mgf (fun ω ↦ α * X ω) μ t = mgf X μ (α * t) := by - rw [← mgf_smul_left] - rfl - -/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`, then `X` is integrable. -/ -lemma integrable_of_mem_interior_integrableExpSet - {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} - (h : 0 ∈ interior (integrableExpSet X μ)) : - Integrable X μ := by - simpa using integrable_pow_of_mem_interior_integrableExpSet h 1 - -namespace Kernel.HasSubgaussianMGF - -variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} - {ν : Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {c : ℝ≥0} - -lemma id_map_iff (hX : Measurable X) : - HasSubgaussianMGF X c κ ν ↔ HasSubgaussianMGF id c (κ.map X) ν := by - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - · constructor - · intro t - rw [← Kernel.deterministic_comp_eq_map hX, ← Measure.comp_assoc, - Measure.deterministic_comp_eq_map] - rw [integrable_map_measure (by fun_prop) hX.aemeasurable] - exact h.integrable_exp_mul t - · simp_rw [Kernel.map_apply _ hX, mgf_id_map hX.aemeasurable] - exact h.mgf_le - · have : X = id ∘ X := rfl - rw [this] - exact .of_map hX h - -protected lemma const_mul (h : HasSubgaussianMGF X c κ ν) (r : ℝ) : - HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, sq_nonneg r⟩ * c) κ ν where - integrable_exp_mul t := by - simp_rw [← mul_assoc] - exact h.integrable_exp_mul (t * r) - mgf_le := by - filter_upwards [h.mgf_le] with ω hω t - specialize hω (t * r) - rw [mgf_const_mul, mul_comm] - refine hω.trans_eq ?_ - congr 1 - simp only [NNReal.coe_mul, NNReal.coe_mk] - ring - -end Kernel.HasSubgaussianMGF - namespace HasSubgaussianMGF variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → ℝ} {c cX cY : ℝ≥0} -lemma id_map_iff (hX : AEMeasurable X μ) : - HasSubgaussianMGF X c μ ↔ HasSubgaussianMGF id c (μ.map X) := by - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - · constructor - · intro t - rw [integrable_map_measure (by fun_prop) hX] - exact h.integrable_exp_mul t - · intro t - rw [mgf_id_map hX] - exact h.mgf_le t - · have : X = id ∘ X := rfl - rw [this] - exact .of_map hX h - -lemma congr_identDistrib {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'} - {Y : Ω' → ℝ} (hX : HasSubgaussianMGF X c μ) (hXY : IdentDistrib X Y μ μ') : - HasSubgaussianMGF Y c μ' := by - rw [id_map_iff hXY.aemeasurable_fst] at hX - rwa [id_map_iff hXY.aemeasurable_snd, ← hXY.map_eq] - -protected lemma const_mul (h : HasSubgaussianMGF X c μ) (r : ℝ) : - HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, sq_nonneg r⟩ * c) μ := by - rw [HasSubgaussianMGF_iff_kernel] at h ⊢ - exact Kernel.HasSubgaussianMGF.const_mul h r - -lemma sub_of_indepFun (hX : HasSubgaussianMGF X cX μ) (hY : HasSubgaussianMGF Y cY μ) - (hindep : IndepFun X Y μ) : - HasSubgaussianMGF (fun ω ↦ X ω - Y ω) (cX + cY) μ := by - simp_rw [sub_eq_add_neg] - exact hX.add_of_indepFun hY.neg hindep.neg_right - --- todo: name -lemma measure_le_le (hX : HasSubgaussianMGF (fun ω ↦ X ω - μ[X]) cX μ) - (hY : HasSubgaussianMGF (fun ω ↦ Y ω - μ[Y]) cY μ) - (hindep : IndepFun X Y μ) (h_le : μ[Y] ≤ μ[X]) : - μ.real {ω | X ω ≤ Y ω} ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by - calc μ.real {ω | X ω ≤ Y ω} - _ = μ.real {ω | (μ[X] - μ[Y]) ≤ (Y ω - μ[Y]) - (X ω - μ[X])} := by - congr with ω - grind - _ ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by - refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq - ?_ - · rw [add_comm cX] - refine sub_of_indepFun hY hX ?_ - exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X]) - (by fun_prop) (by fun_prop) - · grind - · congr 2 - grind - -lemma integrableExpSet_eq_univ (hX : HasSubgaussianMGF X c μ) : - integrableExpSet X μ = Set.univ := by - ext t - simp only [Set.mem_univ, iff_true] - exact hX.integrable_exp_mul t - -lemma integrable (hX : HasSubgaussianMGF X c μ) : Integrable X μ := by - refine integrable_of_mem_interior_integrableExpSet ?_ - simp [integrableExpSet_eq_univ hX] - section Sum variable {ι ι' : Type*} {X : ι → Ω → ℝ} {cX : ι → ℝ≥0} {s : Finset ι} @@ -145,8 +36,8 @@ lemma measure_sum_le_sum_le [IsFiniteMeasure μ] have h_int := (hY_subG j his).integrable simp_rw [sub_eq_add_neg, integrable_add_const_iff] at h_int exact h_int - refine (measure_le_le (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq - ?_ + refine (measureReal_le_le_exp + (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq ?_ · suffices HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, (X i ω - μ[X i])) (∑ i ∈ s, cX i) μ by convert this rw [integral_finset_sum _ hX_int, Finset.sum_sub_distrib] diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index eb509fc3..8df53a22 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -10,87 +10,21 @@ variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀] section MeasurableEquiv -instance : Unique (Iic 0) := by simp only [mem_Iic, nonpos_iff_eq_zero]; exact Unique.subtypeEq 0 - -lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := by - calc _ = ((⟨0, by simp⟩ : Iic 0) : ℕ) := by congr; exact (Unique.eq_default _).symm - _ = _ := by simp - -/-- Measurable equivalence between `Iic 0 → X i` and `X 0`. -/ -def MeasurableEquiv.piIicZero (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] : - ((i : Iic 0) → X i) ≃ᵐ X 0 := - (MeasurableEquiv.piUnique _).trans (coe_default_Iic_zero.symm ▸ MeasurableEquiv.refl _) +lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0 := rfl end MeasurableEquiv namespace ProbabilityTheory.Kernel --- Probability/Kernel/IonescuTulcea/Traj.lean -/-- Distribution of the infinite trajectory given the distribution of `X 0`. -/ -noncomputable -def trajMeasure (μ₀ : Measure (X 0)) (κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))) - [∀ n, IsMarkovKernel (κ n)] : - Measure (Π n, X n) := - (traj κ 0) ∘ₘ (μ₀.map (MeasurableEquiv.piIicZero _).symm) - --- Probability/Kernel/IonescuTulcea/Traj.lean -instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by - rw [trajMeasure] - have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piIicZero _).symm) := - Measure.isProbabilityMeasure_map <| by fun_prop - infer_instance - --- Probability/Kernel/IonescuTulcea/Traj.lean -lemma traj_map_eq_kernel {a : ℕ} : (traj κ a).map (fun x ↦ x (a + 1)) = κ a := by - set f : (Π n, X n) → X (a + 1) := fun x ↦ x (a + 1) - set g : (Π n : Iic (a + 1), X n) → X (a + 1) := fun x ↦ x ⟨a + 1, by simp⟩ - have hf : f = g ∘ (frestrictLe (a + 1)) := by rfl - have hp : g ∘ IicProdIoc a (a + 1) = (piSingleton a).symm ∘ Prod.snd := by - ext - simp [g, _root_.IicProdIoc, piSingleton] - rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe, partialTraj_succ_self, - ← map_comp_right _ (by fun_prop) (by fun_prop), hp, - map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod, - ← map_comp_right _ (by fun_prop) (by fun_prop)] - simp - --- Probability/Kernel/IonescuTulcea/Traj.lean -lemma partialTraj_compProd_kernel_eq_traj_map {a : ℕ} {x₀ : Π n : Iic 0, X n} : - (partialTraj κ 0 a x₀) ⊗ₘ (κ a) = (traj κ 0 x₀).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by - set f := fun x ↦ (frestrictLe a x, x (a + 1)) - set g := fun x ↦ (frestrictLe a x, x) - have hf : f = (Prod.map id (fun x ↦ x (a + 1))) ∘ g := rfl - rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj zero_le', - ← MeasureTheory.Measure.compProd_map (by fun_prop), traj_map_eq_kernel] - --- (Extract kernel lemmas from rewrites?) Probability/Kernel/IonescuTulcea/Traj.lean -lemma trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map {a : ℕ} : - (trajMeasure μ₀ κ).map (frestrictLe a) ⊗ₘ κ a = - (trajMeasure μ₀ κ).map (fun x ↦ (frestrictLe a x, x (a + 1))) := by - rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop), - traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)] - congr with x₀ - rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop), - partialTraj_compProd_kernel_eq_traj_map] - --- Probability/Kernel/IonescuTulcea/Traj.lean -lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ} - [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] : - condDistrib (fun x ↦ x (a + 1)) (frestrictLe a) (trajMeasure μ₀ κ) - =ᵐ[(trajMeasure μ₀ κ).map (frestrictLe a)] κ a := by - apply condDistrib_ae_eq_of_measure_eq_compProd _ (by measurability) - exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm - lemma traj_zero_map_eval_zero : - (Kernel.traj κ 0).map (fun h ↦ h 0) - = Kernel.deterministic (MeasurableEquiv.piIicZero X) - (MeasurableEquiv.piIicZero X).measurable := by - suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map - (MeasurableEquiv.piIicZero X) by - rwa [Kernel.partialTraj_zero, - Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this + (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0)) + = Kernel.deterministic (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i)) + (MeasurableEquiv.piUnique _).measurable := by + suffices (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0)) + = (Kernel.partialTraj κ 0 0).map (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i)) by + rwa [Kernel.partialTraj_zero, Kernel.deterministic_map] at this + fun_prop rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)] - congr with h - sorry + rfl end ProbabilityTheory.Kernel diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean index cf073f5e..effb2b92 100644 --- a/LeanBandits/RewardByCountMeasure.lean +++ b/LeanBandits/RewardByCountMeasure.lean @@ -259,7 +259,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace α] [Countable α] [Nonempty α rw [cond_of_condIndepFun (by fun_prop)] · exact condIndepFun_reward_stepsUntil_arm a m n hm · refine measurable_one.indicator ?_ - exact measurableSet_eq_fun' (by fun_prop) (by fun_prop) + exact measurableSet_eq_fun (by fun_prop) (by fun_prop) · fun_prop · convert hμna using 2 rw [Set.inter_comm] diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanBandits/SequentialLearning/Algorithm.lean index a52ccf45..7fb28c02 100644 --- a/LeanBandits/SequentialLearning/Algorithm.lean +++ b/LeanBandits/SequentialLearning/Algorithm.lean @@ -186,7 +186,7 @@ lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : condDistrib (step (n + 1)) (hist n) (trajMeasure alg env) =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n := - Kernel.condDistrib_trajMeasure_ae_eq_kernel + Kernel.condDistrib_trajMeasure lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : @@ -214,11 +214,12 @@ lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) : aemeasurable := Measurable.aemeasurable (by fun_prop) map_eq := by unfold step + rw [← coe_default_Iic_zero] simp only [trajMeasure, Kernel.trajMeasure] rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero, Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)] - simp + exact Measure.map_id lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) : HasLaw (action 0) alg.p0 (trajMeasure alg env) where diff --git a/blueprint/lean_decls b/blueprint/lean_decls index d545e1de..c92a2d0a 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -2,7 +2,7 @@ Learning.Algorithm Learning.Environment ProbabilityTheory.Kernel.traj ProbabilityTheory.Kernel.trajMeasure -ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel +ProbabilityTheory.Kernel.condDistrib_trajMeasure Learning.condDistrib_action Learning.condDistrib_reward Learning.hasLaw_action_zero diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex index 000a5f16..92edafdc 100644 --- a/blueprint/src/chapters/algorithm.tex +++ b/blueprint/src/chapters/algorithm.tex @@ -90,7 +90,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_X_add_one} \uses{def:history, def:trajMeasure} \leanok - \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel} + \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. \end{lemma} diff --git a/lake-manifest.json b/lake-manifest.json index 49a20969..fd41da25 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "21083832f383e338d7dc4d708dd328018610454e", + "rev": "a06e2b664ad658aa0e96140ac942641ee8f5cd66", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8864a73bf79aad549e34eff972c606343935106d", + "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "451499ea6e97cee4c8979b507a9af5581a849161", + "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d", + "rev": "ef8377f31b5535430b6753a974d685b0019d0681", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.77", + "inputRev": "v0.0.84", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0", + "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7", + "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca", + "rev": "78129e1913fe4988ac238156ec5f223ec02d286c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672", + "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.25.0-rc2", + "inputRev": "v4.27.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "LeanBandits", diff --git a/lean-toolchain b/lean-toolchain index 137937a3..fb18a7f4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0-rc2 \ No newline at end of file +leanprover/lean4:v4.27.0-rc1 \ No newline at end of file From 4d7bdcb1851f7192ae6f5ac67b29e7dc7b8e164f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 17 Dec 2025 15:21:56 +0100 Subject: [PATCH 2/2] remove a sorry --- LeanBandits/ForMathlib/CondDistrib.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean index f937fd20..284eb3ce 100644 --- a/LeanBandits/ForMathlib/CondDistrib.lean +++ b/LeanBandits/ForMathlib/CondDistrib.lean @@ -202,7 +202,7 @@ theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = rfl instance : CanonicallyOrderedAdd (FiniteMeasure α) where - le_add_self := sorry -- was not needed before? + le_add_self μ ν := fun s ↦ by simp exists_add_of_le {μ ν} hμν := by refine ⟨ν - μ, ?_⟩ rw [FiniteMeasure.ext_iff_coe] @@ -264,6 +264,7 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) : Y ⟂ᵢ[Z, hZ; μ] X := by refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight hX hY hZ ?_ (η := η) + rw [← Kernel.compProd_eq_iff, compProd_map_condDistrib (by fun_prop)] at h ⊢ sorry /-- Law of `Y` conditioned on `X`. -/