From dd7fbc5cc6934579c867779b85359cce37e56d78 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Nov 2026 20:26:59 +0100 Subject: [PATCH] Bump Mathlib to 1b1ccf4, the commit of Tau Ceti's v4.36.0-rc2 tag LMLExplore builds LML against this Mathlib, where LML's uses of `Measure.coe_add`, `Measure.coe_zero`, `Measure.smul_apply` and `Measure.finsetSum_apply` are deprecated. The warnings fail LMLExplore's strict PR builds. Use the generic `FunLike.coe_add`, `FunLike.coe_zero`, `smul_apply` and `sum_apply`. `Kernel.sum_apply` is now protected, so name it in full. `Kernel.compProd`'s body is no longer exposed, so prove `compProd_lift` from `compProd_apply` instead of unfolding the definition. Co-Authored-By: Claude Opus 5.5 --- .../KullbackLeibler/Convex.lean | 4 +-- .../Measure/Decomposition/Lebesgue.lean | 2 +- .../Probability/ConditionalProbability.lean | 2 +- .../Probability/HasCondDistrib.lean | 2 +- .../ForMathlib/Probability/HasLaw.lean | 2 +- .../Probability/Kernel/RadonNikodym.lean | 2 +- .../Tactic/EqLift/ForMathlib/Kernel.lean | 2 +- .../Tactic/EqLift/Kernel/Lift.lean | 34 ++++++++++--------- lake-manifest.json | 6 ++-- lakefile.toml | 2 +- 10 files changed, 30 insertions(+), 28 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean index 271e591b..44918b88 100644 --- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean +++ b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean @@ -86,9 +86,9 @@ lemma klDiv_finsetSum_smul_le [∀ i, IsFiniteMeasure (μ i)] have h_comp (ρ : Kernel s Ω) (ρ' : ι → Measure Ω) (hρ : ∀ i : s, ρ i = ρ' i) : ρ ∘ₘ β = ∑ i ∈ s, (c i : ℝ≥0∞) • ρ' i := by ext t ht - rw [Measure.bind_apply ht ρ.aemeasurable, hβ_lintegral, Measure.finsetSum_apply, + rw [Measure.bind_apply ht ρ.aemeasurable, hβ_lintegral, sum_apply, ← Finset.sum_coe_sort s] - exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, Measure.smul_apply, smul_eq_mul] + exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, smul_apply, smul_eq_mul] calc klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ s, (c i : ℝ≥0∞) • ν i) _ = klDiv (κ ∘ₘ β) (η ∘ₘ β) := by rw [h_comp κ μ hκ_apply, h_comp η ν hη_apply] -- data processing inequality for the second projection diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean index f302cc93..e93a8f66 100644 --- a/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean +++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean @@ -46,7 +46,7 @@ lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasur swap · simp only [withDensity_one] exact mutuallySingular_singularPart μ ν - simp only [coe_add, Pi.add_apply] + simp only [FunLike.coe_add, Pi.add_apply] have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance rw [add_comm, ← withDensity_sub (by fun_prop) (by fun_prop)] congr diff --git a/LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean b/LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean index 80d7c2f5..64cfa452 100644 --- a/LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean +++ b/LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean @@ -34,7 +34,7 @@ lemma sum_meas_smul_cond_fiber {X : Ω → α} (hX : Measurable X) (μ : Measure [IsFiniteMeasure μ] : Measure.sum (fun x ↦ μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) = μ := by ext s hs - simp_rw [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, mul_comm (μ _), + simp_rw [Measure.sum_apply _ hs, smul_apply, smul_eq_mul, mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))] rw [← measure_iUnion (fun i j hij ↦ ((Set.disjoint_singleton.2 hij).preimage X).mono Set.inter_subset_left Set.inter_subset_left) fun i ↦ (hX (.singleton i)).inter hs, diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index 4ef69b4c..11c39a78 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -280,7 +280,7 @@ lemma HasCondDistrib.hasLaw_cond (h : HasCondDistrib Y X κ μ) map_eq := by ext u hu rw [Measure.map_apply_of_aemeasurable (h.aemeasurable_snd.mono_ac cond_absolutelyContinuous) hu, - cond, Measure.smul_apply, smul_eq_mul, + cond, smul_apply, smul_eq_mul, Measure.restrict_apply₀ (h.aemeasurable_snd.restrict.nullMeasurableSet_preimage hu), Set.inter_comm, h.measure_inter_preimage_eq_mul_of_eqOn_const hs hκ hu, ← mul_assoc, ENNReal.inv_mul_cancel hμs (measure_ne_top _ _), one_mul] diff --git a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean index 2ef10159..e400d5fb 100644 --- a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean @@ -72,7 +72,7 @@ lemma hasLaw_of_forall_hasLaw_cond [IsProbabilityMeasure P] {g : Ω → ι} (hg rw [← Measure.sum_meas_smul_cond_fiber hg P] at hX ⊢ simp_rw [Measure.map_sum hX, h_eq] ext s hs - simp_rw [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, ENNReal.tsum_mul_right, + simp_rw [Measure.sum_apply _ hs, smul_apply, smul_eq_mul, ENNReal.tsum_mul_right, h_univ, one_mul] end Cond diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/RadonNikodym.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/RadonNikodym.lean index a04ff2bb..3c8ecd90 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Kernel/RadonNikodym.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/RadonNikodym.lean @@ -81,7 +81,7 @@ lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFinit ext s hs rw [sub_apply_eq_rnDeriv_add_singularPart, Kernel.withDensity_apply _ (by fun_prop), Kernel.singularPart_eq_singularPart_measure, Measure.sub_apply_eq_rnDeriv_add_singularPart _] - simp only [Measure.coe_add, Pi.add_apply] + simp only [FunLike.coe_add, Pi.add_apply] congr 2 refine MeasureTheory.withDensity_congr_ae ?_ filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb diff --git a/LeanMachineLearning/Tactic/EqLift/ForMathlib/Kernel.lean b/LeanMachineLearning/Tactic/EqLift/ForMathlib/Kernel.lean index 52c0b616..644fe394 100644 --- a/LeanMachineLearning/Tactic/EqLift/ForMathlib/Kernel.lean +++ b/LeanMachineLearning/Tactic/EqLift/ForMathlib/Kernel.lean @@ -63,7 +63,7 @@ instance (κ : Kernel α β) [IsDeterministic κ] : IsSFiniteKernel κ := by replace h := DFunLike.congr_fun h Set.univ rw [comp_apply'] at h · simp_rw [copy_apply, Measure.dirac_apply' _ MeasurableSet.univ, indicator_univ] at h - simp only [Measure.coe_zero, Pi.zero_apply, Pi.one_apply, MeasureTheory.lintegral_const, + simp only [FunLike.coe_zero, Pi.zero_apply, Pi.one_apply, MeasureTheory.lintegral_const, one_mul] at h exact ha.ne h exact MeasurableSet.univ diff --git a/LeanMachineLearning/Tactic/EqLift/Kernel/Lift.lean b/LeanMachineLearning/Tactic/EqLift/Kernel/Lift.lean index 5a6af29e..049b76bb 100644 --- a/LeanMachineLearning/Tactic/EqLift/Kernel/Lift.lean +++ b/LeanMachineLearning/Tactic/EqLift/Kernel/Lift.lean @@ -64,7 +64,7 @@ lemma isSFinite_lift (κ : Kernel X Y) : · simp only [κs'] ext a s hs replace h := DFunLike.congr (x := ey.symm '' s) (DFunLike.congr (x := ex.symm a) h rfl) rfl - rw [sum_apply, Measure.sum_apply] at h ⊢ + rw [Kernel.sum_apply, Measure.sum_apply] at h ⊢ · rw [lift_apply'] at h · convert h with x · simp @@ -72,7 +72,7 @@ lemma isSFinite_lift (κ : Kernel X Y) : simp · simp only [coe_comap, Function.comp_apply] rw [map_apply' _ ey.measurable _ hs, image_symm] - all_goals measurability + measurability all_goals measurability instance (κ : Kernel X Y) [IsSFiniteKernel κ] : IsSFiniteKernel (lift (ex := ex) (ey := ey) κ) := @@ -137,7 +137,7 @@ lemma id_lift : Kernel.id (α := X') = Kernel.id.lift (ex := ex) (ey := ex) := b simp only [id_apply] rw [Measure.dirac_apply' _ hs, Measure.dirac_apply'] · exact Set.indicator_eq_indicator (by simp) rfl - all_goals measurability + measurability lemma discard_lift : discard.{_, w} X' = (discard X).lift (ex := ex) (ey := punit) := by ext _ _ hs @@ -195,19 +195,21 @@ lemma compProd_lift (κ : Kernel X Y) (η : Kernel (X × Y) Z) : swap · simp [hη, (isSFinite_lift (ex.prodCongr ey) ez η).not.mpr hη] simp [lift] - · simp only [compProd] - rw [← comp_lift (ex := ex.prodCongr ex) (ey := ey.prodCongr ez), ← copy_lift, - ← comp_lift (ex := ex.prodCongr ey), ← parallelComp_lift, ← id_lift, - ← comp_lift (ex := ex.prodCongr (ey.prodCongr ey)), ← parallelComp_lift, ← id_lift, - ← copy_lift, - ← comp_lift (ex := (ex.prodCongr ey).prodCongr ey), - ← comp_lift (ex := ez.prodCongr ey), ← parallelComp_lift, ← id_lift, ← swap_lift] - congr - simp only [lift] - rw [deterministic_map (MeasurableEquiv.measurable _) (MeasurableEquiv.measurable _)] - ext _ : 1 - simp [comap_apply, deterministic_apply, MeasurableEquiv.prodCongr, prodAssoc] - + · have := (isSFinite_lift ex ey κ).mpr hκ + have := (isSFinite_lift (ex.prodCongr ey) ez η).mpr hη + ext a s hs + rw [compProd_apply hs, lift_apply' _ _ _ _ hs, + compProd_apply ((ey.prodCongr ez).measurableSet_image.mpr hs), lift_apply, + map_apply _ ey.symm.measurable, lintegral_map_equiv] + refine lintegral_congr fun y ↦ ?_ + rw [lift_apply' _ _ _ _ (measurable_prodMk_left hs)] + congr 1 + · simp [MeasurableEquiv.prodCongr] + · ext z + simp only [image_eq_preimage_symm, Set.mem_preimage, prodCongr, MeasurableEquiv.coe_mk, + Equiv.prodCongr_apply, coe_toEquiv, Set.mem_image, Prod.exists, Prod.map_apply, + Prod.mk.injEq] + exact ⟨fun h ↦ ⟨_, _, h, by simp, by simp⟩, by rintro ⟨_, _, h, rfl, rfl⟩; simpa using h⟩ instance {κ : Kernel X Y} [IsDeterministic κ] : IsDeterministic (κ.lift (ex := ex) (ey := ey)) where diff --git a/lake-manifest.json b/lake-manifest.json index be14d92e..c0a1ef54 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d581dfff2e41de989072ea63abf3daf69311520", + "rev": "1b1ccf4b088b32fa3f23f2de1127433254a81e1e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc2", + "inputRev": "1b1ccf4b088b32fa3f23f2de1127433254a81e1e", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3", + "rev": "6d971e7e6b3f7d0a501c5418815aa9022edd3499", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 366fbf69..88ee01ce 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -17,7 +17,7 @@ rev = "v4.36.0-rc2" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.36.0-rc2" +rev = "1b1ccf4b088b32fa3f23f2de1127433254a81e1e" [[lean_lib]] name = "LeanMachineLearning"