From 471f463aa529a290df0622ccf621a7d22cba8e0c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 09:43:46 +0100 Subject: [PATCH 1/2] chore: bump Mathlib to 2ddf59c MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move Mathlib from 6135ffb to 2ddf59c, the commit Tau Ceti's main pins, so that LML can require Statlib and LMLExplore can sync to it. - `EventuallyEqSet` refactor (mathlib4#45712): a.e. equality of sets is now pointwise `↔`; adapt three proofs. - `enorm` renamed to `eNorm` (mathlib4#45735): fix the `ENorm EReal` instance and the deprecated lemma names; rename `bayesBinaryRisk_eq_lintegral_enorm` to `bayesBinaryRisk_eq_lintegral_eNorm` and two private lemmas to match. - Fix the linter warnings, so that the build is warning-free. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- Statlib/Divergence/Renyi/Basic.lean | 8 ++++---- Statlib/Divergence/StatInfo/Basic.lean | 4 ++-- Statlib/Divergence/TotalVariation.lean | 2 +- Statlib/EValues/NumeraireExistence.lean | 10 +++------- Statlib/ForMathlib/ENNReal.lean | 2 +- Statlib/ForMathlib/EReal.lean | 6 +++--- Statlib/Inference/QMD.lean | 18 +++++++++--------- Statlib/Testing/Binary.lean | 4 ++-- Statlib/Testing/Sequential/Wald.lean | 6 +++--- lake-manifest.json | 8 ++++---- lakefile.toml | 2 +- 11 files changed, 33 insertions(+), 37 deletions(-) diff --git a/Statlib/Divergence/Renyi/Basic.lean b/Statlib/Divergence/Renyi/Basic.lean index e28b9ef..43ab7fc 100644 --- a/Statlib/Divergence/Renyi/Basic.lean +++ b/Statlib/Divergence/Renyi/Basic.lean @@ -684,8 +684,8 @@ lemma renyiDiv_smul_left (ha_nonneg : 0 ≤ a) [IsFiniteMeasure μ] [IsFiniteMea have h_set : ν {x | 0 < (∂(c • μ)/∂ν) x} = ν {x | 0 < (∂μ/∂ν) x} := by refine measure_congr ?_ filter_upwards [Measure.rnDeriv_smul_left' μ ν c] with x hx - show (0 < (∂(c • μ)/∂ν) x) = (0 < (∂μ/∂ν) x) - rw [hx, Pi.smul_apply, ENNReal.smul_def, smul_eq_mul, eq_iff_iff, ENNReal.mul_pos_iff, + show 0 < (∂(c • μ)/∂ν) x ↔ 0 < (∂μ/∂ν) x + rw [hx, Pi.smul_apply, ENNReal.smul_def, smul_eq_mul, ENNReal.mul_pos_iff, ENNReal.coe_pos] exact ⟨fun h ↦ h.2, fun h ↦ ⟨pos_iff_ne_zero.mpr hc, h⟩⟩ rw [renyiDiv_zero, renyiDiv_zero, h_set] @@ -748,8 +748,8 @@ lemma renyiDiv_smul_right (ha_nonneg : 0 ≤ a) [IsFiniteMeasure μ] [IsFiniteMe congr 1 refine measure_congr ?_ filter_upwards [Measure.rnDeriv_smul_right' μ ν hc] with x hx - show (0 < (∂μ/∂(c • ν)) x) = (0 < (∂μ/∂ν) x) - rw [hx, Pi.smul_apply, ENNReal.smul_def, smul_eq_mul, eq_iff_iff, ENNReal.mul_pos_iff, + show 0 < (∂μ/∂(c • ν)) x ↔ 0 < (∂μ/∂ν) x + rw [hx, Pi.smul_apply, ENNReal.smul_def, smul_eq_mul, ENNReal.mul_pos_iff, ENNReal.coe_pos] exact ⟨fun h ↦ h.2, fun h ↦ ⟨pos_iff_ne_zero.mpr (inv_ne_zero hc), h⟩⟩ rw [renyiDiv_zero, renyiDiv_zero, h_set, Measure.coe_nnreal_smul_apply, diff --git a/Statlib/Divergence/StatInfo/Basic.lean b/Statlib/Divergence/StatInfo/Basic.lean index 09be312..afdb02a 100644 --- a/Statlib/Divergence/StatInfo/Basic.lean +++ b/Statlib/Divergence/StatInfo/Basic.lean @@ -276,7 +276,7 @@ lemma toReal_statInfo_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMeasure μ · rw [abs_of_nonpos] swap · refine sub_nonpos.mpr <| (ENNReal.toReal_le_toReal ?_ ?_).mpr h - <;> try simp only [ne_eq, measure_ne_top _ _, not_false_eq_true, ENNReal.mul_ne_top] + <;> simp only [ne_eq, measure_ne_top _ _, not_false_eq_true, ENNReal.mul_ne_top] simp_rw [toReal_statInfo_eq_integral_max_of_le h, sup_eq_half_smul_add_add_abs_sub' ℝ, smul_eq_mul, zero_add, sub_zero, integral_const_mul] calc @@ -300,7 +300,7 @@ lemma toReal_statInfo_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMeasure μ · rw [abs_of_nonneg] swap · refine sub_nonneg.mpr <| (ENNReal.toReal_le_toReal ?_ ?_).mpr h - <;> try simp only [ne_eq, measure_ne_top _ _, not_false_eq_true, ENNReal.mul_ne_top] + <;> simp only [ne_eq, measure_ne_top _ _, not_false_eq_true, ENNReal.mul_ne_top] simp_rw [toReal_statInfo_eq_integral_max_of_ge h, sup_eq_half_smul_add_add_abs_sub' ℝ, smul_eq_mul, zero_add, sub_zero, integral_const_mul] calc diff --git a/Statlib/Divergence/TotalVariation.lean b/Statlib/Divergence/TotalVariation.lean index f6f705e..b8e1d69 100644 --- a/Statlib/Divergence/TotalVariation.lean +++ b/Statlib/Divergence/TotalVariation.lean @@ -224,7 +224,7 @@ lemma tvDivFun_apply_top : tvDivFun ∞ = ∞ := by `x ↦ |1 - x|`. -/ lemma fDiv_tvDivFun (μ ν : Measure 𝒳) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : fDiv tvDivFun μ ν = etvDist μ ν := by - rw [fDiv, derivAtTop_tvDivFun, one_mul, etvDist_eq_lintegral_enorm_rnDeriv_add_singularPart] + rw [fDiv, derivAtTop_tvDivFun, one_mul, etvDist_eq_lintegral_eNorm_rnDeriv_add_singularPart] congr 1 refine lintegral_congr_ae ?_ filter_upwards [μ.rnDeriv_ne_top ν] with x hx diff --git a/Statlib/EValues/NumeraireExistence.lean b/Statlib/EValues/NumeraireExistence.lean index cf64364..09beff8 100644 --- a/Statlib/EValues/NumeraireExistence.lean +++ b/Statlib/EValues/NumeraireExistence.lean @@ -612,12 +612,11 @@ theorem IsEVarClass.exists_isLogNumeraireFor (h𝓔 : IsEVarClass 𝓔) (P : Mea -- all the sets `{Xo n ≠ ∞}` agree up to null sets set A : Set 𝓧 := {x | Xo 0 x ≠ ∞} with hA_def have hA (n : ℕ) : P {x | Xo n x ≠ ∞} = P A := by - refine measure_congr (Filter.EventuallyEq.symm ?_) + refine measure_congr (Filter.EventuallyEqSet.symm ?_) filter_upwards [lt_top_of_numeraireOfBounded_lt_top (boundedLogUtility_le (hN n)) P h𝓔 (hXo_evar 0), lt_top_of_numeraireOfBounded_lt_top (boundedLogUtility_le (hN 0)) P h𝓔 (hXo_evar n)] with x h1 h2 - exact propext - ⟨fun h ↦ (h2 (lt_top_iff_ne_top.mpr h)).ne, fun h ↦ (h1 (lt_top_iff_ne_top.mpr h)).ne⟩ + exact ⟨fun h ↦ (h2 (lt_top_iff_ne_top.mpr h)).ne, fun h ↦ (h1 (lt_top_iff_ne_top.mpr h)).ne⟩ have hPA : P A ≠ ∞ := measure_ne_top _ _ -- the first order condition, in `ℝ≥0∞` form have hfoc (n : ℕ) {Y : 𝓧 → ℝ≥0∞} (hY : Y ∈ 𝓔) : @@ -834,10 +833,7 @@ lemma lintegral_div_logNumeraire_le_measure_fsupport (P : Measure 𝓧) (h𝓔 : split_ifs with h · exact absurd h.2 hP · rfl - have h_fsupport : (1 : 𝓧 → ℝ≥0∞).fsupport = .univ := by - ext - simp [Function.fsupport] - simp [h_one, h_fsupport, h_univ] + simp [h_one, h_univ] lemma lintegral_div_logNumeraire_le (P : Measure 𝓧) (h𝓔 : IsEVarClass 𝓔) (hX : X ∈ 𝓔) : ∫⁻ x, X x / logNumeraire P 𝓔 x ∂P diff --git a/Statlib/ForMathlib/ENNReal.lean b/Statlib/ForMathlib/ENNReal.lean index cca3c06..60f0777 100644 --- a/Statlib/ForMathlib/ENNReal.lean +++ b/Statlib/ForMathlib/ENNReal.lean @@ -25,7 +25,7 @@ abbrev fsupport {α β : Type*} [Top β] [Zero β] (f : α → β) := {x | f x lemma fsupport_compl {α β : Type*} [Top β] [Zero β] (X : α → β) : X.fsupportᶜ = {ω | X ω = ⊤} ∪ {ω | X ω = 0} := by ext ω - simp [-not_and, not_and_or] + simp [-not_and] lemma fsupport_compl_disjoint {α β : Type*} [Top β] [Zero β] (X : α → β) (h : (0 : β) ≠ ⊤) : Disjoint {ω | X ω = ⊤} {ω | X ω = 0} := by diff --git a/Statlib/ForMathlib/EReal.lean b/Statlib/ForMathlib/EReal.lean index ca2c965..749b812 100644 --- a/Statlib/ForMathlib/EReal.lean +++ b/Statlib/ForMathlib/EReal.lean @@ -145,8 +145,8 @@ lemma EReal.add_sub_add (a b : EReal) {c d : EReal} (hc : c ≠ ⊥) (hd : d ≠ cases a <;> cases b <;> cases c <;> cases d -- 81 goals :) any_goals simp [hc, hd] - any_goals simp at hc - any_goals simp at hd + all_goals simp at hc + all_goals simp at hd · norm_cast ring · norm_cast @@ -249,7 +249,7 @@ lemma EReal.ne_top_exists_finite_iff {a : EReal} : a ≠ ⊤ ↔ ∃ b, b ≠ noncomputable instance : ENorm EReal where - enorm x := (max x 0).toENNReal + (- min x 0).toENNReal + eNorm x := (max x 0).toENNReal + (- min x 0).toENNReal noncomputable instance : SMul ℝ≥0 EReal where smul c x := c * x noncomputable instance : SMul ℝ≥0∞ EReal where smul c x := c * x diff --git a/Statlib/Inference/QMD.lean b/Statlib/Inference/QMD.lean index a4d4bdd..29562f2 100644 --- a/Statlib/Inference/QMD.lean +++ b/Statlib/Inference/QMD.lean @@ -108,7 +108,7 @@ theorem HasQuadraticMeanDerivWithinAt.tendsto_local_path_remainder {Ω E : Type* hbigO).tendsto_inv_smul_nhds_zero /-- The squared `ℝ≥0∞`-norm of `√((dm/dμ).toReal)` is `dm/dμ`, almost everywhere. -/ -private lemma enorm_sqrt_toReal_rnDeriv_rpow_two {Ω : Type*} {mΩ : MeasurableSpace Ω} +private lemma eNorm_sqrt_toReal_rnDeriv_rpow_two {Ω : Type*} {mΩ : MeasurableSpace Ω} (m μ : Measure Ω) [SigmaFinite m] : ∀ᵐ ω ∂μ, ‖√(m.rnDeriv μ ω).toReal‖ₑ ^ (2 : ℝ) = m.rnDeriv μ ω := by filter_upwards [Measure.rnDeriv_lt_top m μ] with ω hω @@ -118,18 +118,18 @@ private lemma enorm_sqrt_toReal_rnDeriv_rpow_two {Ω : Type*} {mΩ : MeasurableS exact hω.ne /-- The `L²` lintegral is unchanged after transporting `u` from `m` to `μ` by `√(dm/dμ)`. -/ -private lemma Lp.lintegral_enorm_mul_sqrt_rnDeriv_rpow_two {Ω : Type*} {mΩ : MeasurableSpace Ω} +private lemma Lp.lintegral_eNorm_mul_sqrt_rnDeriv_rpow_two {Ω : Type*} {mΩ : MeasurableSpace Ω} {m μ : Measure Ω} [SigmaFinite m] [m.HaveLebesgueDecomposition μ] (hm : m ≪ μ) (u : Ω →₂[m] ℝ) : ∫⁻ a, ‖u a * √(m.rnDeriv μ a).toReal‖ₑ ^ (2 : ℝ) ∂μ = ∫⁻ a, ‖u a‖ₑ ^ (2 : ℝ) ∂m := by calc ∫⁻ a, ‖u a * √(m.rnDeriv μ a).toReal‖ₑ ^ (2 : ℝ) ∂μ = ∫⁻ a, m.rnDeriv μ a * ‖u a‖ₑ ^ (2 : ℝ) ∂μ := by apply lintegral_congr_ae - filter_upwards [enorm_sqrt_toReal_rnDeriv_rpow_two m μ] with a hsqrt + filter_upwards [eNorm_sqrt_toReal_rnDeriv_rpow_two m μ] with a hsqrt calc ‖u a * √(m.rnDeriv μ a).toReal‖ₑ ^ (2 : ℝ) = ‖u a‖ₑ ^ (2 : ℝ) * ‖√(m.rnDeriv μ a).toReal‖ₑ ^ (2 : ℝ) := by - rw [enorm_mul, ENNReal.mul_rpow_of_nonneg _ _ (by norm_num : (0 : ℝ) ≤ 2)] + rw [eNorm_mul, ENNReal.mul_rpow_of_nonneg _ _ (by norm_num : (0 : ℝ) ≤ 2)] _ = ‖u a‖ₑ ^ (2 : ℝ) * m.rnDeriv μ a := by rw [hsqrt] _ = m.rnDeriv μ a * ‖u a‖ₑ ^ (2 : ℝ) := by rw [mul_comm] _ = ∫⁻ a, ‖u a‖ₑ ^ (2 : ℝ) ∂(μ.withDensity (m.rnDeriv μ)) := by @@ -142,21 +142,21 @@ private lemma Lp.lintegral_enorm_mul_sqrt_rnDeriv_rpow_two {Ω : Type*} {mΩ : M private lemma Lp.eLpNorm_mul_sqrt_rnDeriv {Ω : Type*} {mΩ : MeasurableSpace Ω} {m μ : Measure Ω} [SigmaFinite m] [m.HaveLebesgueDecomposition μ] (hm : m ≪ μ) (u : Ω →₂[m] ℝ) : eLpNorm (fun ω => u ω * √(m.rnDeriv μ ω).toReal) 2 μ = eLpNorm u 2 m := by - rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp) (by simp) (by fun_prop), - eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp) (by simp) (by fun_prop)] + rw [eLpNorm_eq_lintegral_rpow_eNorm_toReal (by simp) (by simp) (by fun_prop), + eLpNorm_eq_lintegral_rpow_eNorm_toReal (by simp) (by simp) (by fun_prop)] simpa using congrArg (fun x => x ^ (1 / ENNReal.toReal (2 : ℝ≥0∞))) - (Lp.lintegral_enorm_mul_sqrt_rnDeriv_rpow_two hm u) + (Lp.lintegral_eNorm_mul_sqrt_rnDeriv_rpow_two hm u) /-- The square root of a Radon-Nikodym derivative of a finite measure is in `L²`. -/ private lemma memLp_sqrt_rnDeriv {Ω : Type*} {mΩ : MeasurableSpace Ω} (m μ : Measure Ω) [IsFiniteMeasure m] : MemLp (fun ω => √(m.rnDeriv μ ω).toReal) 2 μ := by - rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top + rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_eNorm_lt_top (by simp) (by simp) ((Measure.measurable_rnDeriv _ _).aemeasurable.ennreal_toReal.sqrt).aestronglyMeasurable] calc ∫⁻ a, ‖√(m.rnDeriv μ a).toReal‖ₑ ^ (2 : ℝ) ∂μ = ∫⁻ a, m.rnDeriv μ a ∂μ := - lintegral_congr_ae (enorm_sqrt_toReal_rnDeriv_rpow_two m μ) + lintegral_congr_ae (eNorm_sqrt_toReal_rnDeriv_rpow_two m μ) _ < ∞ := Measure.lintegral_rnDeriv_lt_top m μ /-- If `u ∈ L²(m)` and `m ≪ μ`, then `u * √(dm/dμ)` belongs to `L²(μ)`. -/ diff --git a/Statlib/Testing/Binary.lean b/Statlib/Testing/Binary.lean index a0bd427..a2181e0 100644 --- a/Statlib/Testing/Binary.lean +++ b/Statlib/Testing/Binary.lean @@ -449,7 +449,7 @@ lemma toReal_bayesBinaryRisk_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMea (measure_ne_top _ _)) (ENNReal.mul_ne_top (measure_ne_top _ _) (measure_ne_top _ _)), ENNReal.toReal_mul] -lemma bayesBinaryRisk_eq_lintegral_enorm (μ ν : Measure 𝒳) [IsFiniteMeasure μ] +lemma bayesBinaryRisk_eq_lintegral_eNorm (μ ν : Measure 𝒳) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (π : Measure Bool) [IsFiniteMeasure π] : bayesBinaryRisk μ ν π = 2⁻¹ * (((Kernel.boolKernel μ ν ∘ₘ π) .univ) - ∫⁻ x, ‖(π {false} * (∂μ/∂(Kernel.boolKernel μ ν ∘ₘ π)) x).toReal @@ -464,6 +464,6 @@ lemma bayesBinaryRisk_eq_lintegral_enorm (μ ν : Measure 𝒳) [IsFiniteMeasure · simp_rw [ENNReal.toReal_mul] exact ((Measure.integrable_toReal_rnDeriv.const_mul _).sub (Measure.integrable_toReal_rnDeriv.const_mul _)).abs - simp_rw [Real.enorm_eq_ofReal_abs] + simp_rw [Real.eNorm_eq_ofReal_abs] end ProbabilityTheory diff --git a/Statlib/Testing/Sequential/Wald.lean b/Statlib/Testing/Sequential/Wald.lean index e1b773e..e6eb40c 100644 --- a/Statlib/Testing/Sequential/Wald.lean +++ b/Statlib/Testing/Sequential/Wald.lean @@ -87,12 +87,12 @@ lemma integrable_sum_Iic_of_summable (hX : ∀ n, IntegrableOn (X n) {ω | n ≤ rw [Set.indicator_of_notMem] simpa using hn · calc ∫⁻ ω, ‖∑' n, F n ω‖ₑ ∂P - _ ≤ ∫⁻ ω, ∑' n, ‖F n ω‖ₑ ∂P := lintegral_mono fun ω ↦ enorm_tsum_le_tsum_enorm + _ ≤ ∫⁻ ω, ∑' n, ‖F n ω‖ₑ ∂P := lintegral_mono fun ω ↦ eNorm_tsum_le_tsum_eNorm _ = ∑' n, ∫⁻ ω, ‖F n ω‖ₑ ∂P := - lintegral_tsum fun n ↦ (hF_int n).1.enorm + lintegral_tsum fun n ↦ (hF_int n).1.eNorm _ = ∑' n, ENNReal.ofReal (∫ ω, ‖F n ω‖ ∂P) := by congr with n - rw [ofReal_integral_norm_eq_lintegral_enorm (hF_int n)] + rw [ofReal_integral_norm_eq_lintegral_eNorm (hF_int n)] _ = ENNReal.ofReal (∑' n, ∫ ω, ‖F n ω‖ ∂P) := (ENNReal.ofReal_tsum_of_nonneg (fun n ↦ integral_nonneg fun _ ↦ norm_nonneg _) hF_sum).symm _ < ∞ := ENNReal.ofReal_lt_top diff --git a/lake-manifest.json b/lake-manifest.json index d6e2aa4..f14198b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b", + "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b", + "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60", + "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "08a1d53cd0bbb78442973b751c8e6f98e75b12be", + "rev": "4af7237d146261353907b06a01b6f3fc06cfa067", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 6ed32ac..90f55f6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,7 +13,7 @@ weak.linter.mathlibStandardSet = true [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b" +rev = "2ddf59c8f14245864e6c0ed227a2dab76b9efea2" [[require]] name = "subverso" From 9e5c133797540ce2599576dbd16c1da03f9f1995 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 09:51:44 +0100 Subject: [PATCH 2/2] chore: rename `AbsolutelyContinuous.pi` to `AbsolutelyContinuous.pi'` Tau Ceti has a `MeasureTheory.Measure.AbsolutelyContinuous.pi` with the same statement, so the two cannot be imported together. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- .../MeasureTheory/Measure/Decomposition/RNDerivProd.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RNDerivProd.lean b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RNDerivProd.lean index 45bf427..d62226a 100644 --- a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RNDerivProd.lean +++ b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RNDerivProd.lean @@ -24,7 +24,7 @@ and similarly for binary products. * `MeasureTheory.Measure.pi_eq_withDensity_prod_rnDeriv`: if `μ i ≪ ν i` for all `i`, then `Measure.pi μ = (Measure.pi ν).withDensity (fun x ↦ ∏ i, ∂(μ i)/∂(ν i) (x i))`. * `MeasureTheory.Measure.rnDeriv_pi`: `∂(Measure.pi μ)/∂(Measure.pi ν) =ᵐ ∏ i, ∂(μ i)/∂(ν i) (x i)`. -* `MeasureTheory.Measure.AbsolutelyContinuous.pi`: if `μ i ≪ ν i` for all `i`, then +* `MeasureTheory.Measure.AbsolutelyContinuous.pi'`: if `μ i ≪ ν i` for all `i`, then `Measure.pi μ ≪ Measure.pi ν`. * `MeasureTheory.Measure.not_mutuallySingular_pi`: products of σ-finite measures which are not mutually singular are not mutually singular. @@ -149,7 +149,7 @@ lemma rnDeriv_pi [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)] : ENNReal.prod_div_distrib_of_ne_top fun i _ ↦ h5 i] /-- If `μ i ≪ ν i` for all `i`, then `Measure.pi μ ≪ Measure.pi ν`. -/ -lemma AbsolutelyContinuous.pi [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)] +lemma AbsolutelyContinuous.pi' [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)] (h : ∀ i, μ i ≪ ν i) : Measure.pi μ ≪ Measure.pi ν := by rw [pi_eq_withDensity_prod_rnDeriv h] @@ -163,9 +163,9 @@ lemma not_mutuallySingular_pi [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite ( -- product of the `ρ i` is absolutely continuous with respect to both products set ρ : (i : ι) → Measure (X i) := fun i ↦ (ν i).withDensity ((μ i).rnDeriv (ν i)) have (i : ι) : NeZero (ρ i) := ⟨by simpa [ρ] using h i⟩ - have hρμ : Measure.pi ρ ≪ Measure.pi μ := AbsolutelyContinuous.pi fun i ↦ + have hρμ : Measure.pi ρ ≪ Measure.pi μ := AbsolutelyContinuous.pi' fun i ↦ absolutelyContinuous_of_le (withDensity_rnDeriv_le (μ i) (ν i)) - have hρν : Measure.pi ρ ≪ Measure.pi ν := AbsolutelyContinuous.pi fun i ↦ + have hρν : Measure.pi ρ ≪ Measure.pi ν := AbsolutelyContinuous.pi' fun i ↦ withDensity_absolutelyContinuous (ν i) ((μ i).rnDeriv (ν i)) intro h_ms exact NeZero.ne _ ((MutuallySingular.self_iff _).mp (h_ms.mono_ac hρμ hρν))