Bump mathlib to latest master and fix compatibility

Statlib/Contiguity/Def.lean

@@ -46,15 +46,13 @@ trivially from `Filter.tendsto_bot`.
 -/
 def Contiguous2 (l : Filter α) (P Q : ∀ a, ProbabilityMeasure (Ω a)) : Prop :=
   ∀ (L : ProbabilityMeasure ℝ≥0∞) ⦃h : Filter α⦄, h ≤ l → h.NeBot →
-    Tendsto (fun a => (Q a).map
-      ((Measure.measurable_rnDeriv (P a) (Q a)).aemeasurable)) h (𝓝 L) →
+    Tendsto (fun a ↦ (Q a).map ((P a : Measure (Ω a)).rnDeriv (Q a))) h (𝓝 L) →
       L {0} = 0
 
 /-- Contiguity characterized by unit mean for weak limits of reciprocal likelihood-ratio laws. -/
 def Contiguous3 (l : Filter α) (P Q : ∀ a, ProbabilityMeasure (Ω a)) : Prop :=
   ∀ (V : ProbabilityMeasure ℝ≥0∞) ⦃h : Filter α⦄, h ≤ l → h.NeBot →
-    Tendsto (fun a => (P a).map
-      ((Measure.measurable_rnDeriv (Q a) (P a)).aemeasurable)) h (𝓝 V) →
+    Tendsto (fun a ↦ (P a).map ((Q a : Measure (Ω a)).rnDeriv (P a))) h (𝓝 V) →
       ∫⁻ ω, ω ∂V = 1
 
 /-- Convergence in measure for a family of probability measures on varying measurable spaces. -/

Statlib/ForMathlib/Algebra/Order/Group/PosPart.lean

@@ -9,8 +9,8 @@ public import Mathlib.Algebra.Order.Group.PosPart
 variable {α : Type*} [Lattice α] [DivInvMonoid α]
 
 -- even though it is almost a duplicate of `one_le_oneLePart`, it allows `simp` to work on its goal.
-@[to_additive (attr := simp) posPart_fun_nonneg]
+@[to_additive (attr := simp, nolint simpNF) posPart_fun_nonneg, nolint simpNF]
 lemma one_le_oneLePart_fun {β : Type*} (f : β → α) (x : β) : 1 ≤ f⁺ᵐ x := one_le_oneLePart f x
 
-@[to_additive (attr := simp) negPart_fun_nonneg]
+@[to_additive (attr := simp, nolint simpNF) negPart_fun_nonneg, nolint simpNF]
 lemma one_le_leOnePart_fun {β : Type*} (f : β → α) (x : β) : 1 ≤ f⁻ᵐ x := one_le_leOnePart f x

Statlib/ForMathlib/EReal.lean

@@ -151,7 +151,6 @@ lemma EReal.add_sub_add (a b : EReal) {c d : EReal} (hc : c ≠ ⊥) (hd : d ≠
     ring
   · norm_cast
   · norm_cast
-  · norm_cast
 
 lemma EReal.mul_sub_of_eq_zero {a b c : EReal} (h : b = 0 ∨ c = 0) :
     a * (b - c) = a * b - a * c := by

Statlib/ForMathlib/MeasureTheory/Integral/EReal/Bochner.lean

@@ -104,8 +104,10 @@ lemma integrable_ereal_toReal_iff (hf_meas : AEMeasurable f μ)
   rw [lintegral_enorm_ereal_toReal h_bot h_top] at h_lintegral
   rw [eintegral_eq_posPartFun_sub_negPartFun]
   have := lintegral_enorm_eq_posPartFun_add_negPartFun hf_meas
-  have h_pos_ne_bot : ∫ᵉ x, f⁺ x ∂μ ≠ ⊥ := by simp [eintegral_of_nonneg (posPart_fun_nonneg _)]
-  have h_neg_ne_bot : ∫ᵉ x, f⁻ x ∂μ ≠ ⊥ := by simp [eintegral_of_nonneg (negPart_fun_nonneg _)]
+  have h_pos_ne_bot : ∫ᵉ x, f⁺ x ∂μ ≠ ⊥ :=
+    ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (posPart_fun_nonneg _)
+  have h_neg_ne_bot : ∫ᵉ x, f⁻ x ∂μ ≠ ⊥ :=
+    ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (negPart_fun_nonneg _)
   have h_pos_ne_top : ∫ᵉ x, f⁺ x ∂μ ≠ ⊤ := by
     intro h_contra
     simp only [h_contra] at this

Statlib/ForMathlib/MeasureTheory/Integral/EReal/EIntegral.lean

@@ -690,23 +690,23 @@ lemma eintegral_add (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
         | inl h' => exact h'
         | inr h' =>
           intro h_false
-          simp [h_false, EReal.top_sub h'] at h
+          exact h (by rw [h_false, EReal.top_sub h'])
       | inr h =>
         refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_right _ _)) (Ne.lt_top ?_)
         intro h_false
-        simp [h_false] at h
+        exact h (by rw [h_false, EReal.sub_top])
     · cases h_ne_bot_1 with
       | inl h =>
         refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_left _ _)) (Ne.lt_top ?_)
         intro h_false
-        simp [h_false] at h
+        exact h (by rw [h_false, EReal.sub_top])
       | inr h =>
         refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_right _ _)) (Ne.lt_top ?_)
         cases hg_int.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top with
         | inl h' => exact h'
         | inr h' =>
           intro h_false
-          simp [h_false, EReal.top_sub h'] at h
+          exact h (by rw [h_false, EReal.top_sub h'])
   · exact fun _ ↦ add_nonneg (by simp) (by simp)
   · exact fun _ ↦ add_nonneg (by simp) (by simp)
 
@@ -728,10 +728,10 @@ lemma eintegral_add' (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
     simp only [eintegral_eq_posPartFun_sub_negPartFun f, sub_eq_add_neg, EReal.add_eq_bot_iff,
       EReal.neg_eq_bot_iff] at hf_int_eq_bot
     have : ∫ᵉ x, f⁺ x ∂μ ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp)
-    simpa [this] using hf_int_eq_bot
+    exact hf_int_eq_bot.resolve_left this
   have hg₂_int : ∫ᵉ x, g⁻ x ∂μ ≠ ⊤ := by
     intro h_false
-    simp [eintegral_eq_posPartFun_sub_negPartFun g, h_false] at hg_ne_bot
+    exact hg_ne_bot (by rw [eintegral_eq_posPartFun_sub_negPartFun g, h_false, EReal.sub_top])
   have hg₁_int : ∫ᵉ x, g⁺ x ∂μ ≠ ⊤ := by
     intro h_false
     rw [eintegral_eq_posPartFun_sub_negPartFun g, h_false, EReal.top_sub hg₂_int] at hg_ne_top
@@ -745,11 +745,13 @@ lemma eintegral_add' (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
   simp_rw [hf_add_g]
   rw [eintegral_sub_of_nonneg (fun _ ↦ add_nonneg (by simp) (by simp))
     (fun _ ↦ add_nonneg (by simp) (by simp)) (by fun_prop) (by fun_prop)]
-  · suffices ∫ᵉ x, f⁻ x + g⁻ x ∂μ = ⊤ by simp [this]
-    rw [← top_le_iff]
-    calc ⊤
-    _ = ∫ᵉ x, f⁻ x ∂μ := by rw [hf₂_int]
-    _ ≤ ∫ᵉ x, f⁻ x + g⁻ x ∂μ := eintegral_mono (fun _ ↦ le_add_of_nonneg_right (by simp))
+  · have hneg : ∫ᵉ x, f⁻ x + g⁻ x ∂μ = ⊤ := by
+      rw [← top_le_iff]
+      calc ⊤
+      _ = ∫ᵉ x, f⁻ x ∂μ := by rw [hf₂_int]
+      _ ≤ ∫ᵉ x, f⁻ x + g⁻ x ∂μ :=
+        eintegral_mono (fun _ ↦ le_add_of_nonneg_right (by simp))
+    rw [hneg, EReal.sub_top]
   · have h_le x : min (f⁺ x + g⁺ x) (f⁻ x + g⁻ x) ≤ min (f⁺ x) (g⁻ x) + min (f⁻ x) (g⁺ x) := by
       rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f x with hf | hf <;>
         rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero g x with hg | hg <;>

Statlib/QMD.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Asymptotics.TVS
 public import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
 public import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
+public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
 
 /-!
 # Quadratic mean differentiability
@@ -141,18 +142,18 @@ 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),
-    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp) (by simp)]
+  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)
 
 /-- 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
-  refine
-    ⟨((Measure.measurable_rnDeriv _ _).aemeasurable.ennreal_toReal.sqrt).aestronglyMeasurable, ?_⟩
-  rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by simp) (by simp)]
+  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 μ)
@@ -162,27 +163,21 @@ private lemma memLp_sqrt_rnDeriv {Ω : Type*} {mΩ : MeasurableSpace Ω} (m μ :
 private lemma Lp.memLp_mul_sqrt_rnDeriv {Ω : Type*} {mΩ : MeasurableSpace Ω} {m μ : Measure Ω}
     [SigmaFinite m] [m.HaveLebesgueDecomposition μ] (hm : m ≪ μ) (u : Ω →₂[m] ℝ) :
     MemLp (fun ω => u ω * √(m.rnDeriv μ ω).toReal) 2 μ := by
-  refine ⟨(Lp.stronglyMeasurable u).aestronglyMeasurable.mul
-    ((Measure.measurable_rnDeriv _ _).aemeasurable.ennreal_toReal.sqrt).aestronglyMeasurable, ?_⟩
+  change eLpNorm (fun ω => u ω * √(m.rnDeriv μ ω).toReal) 2 μ < ∞
   rw [Lp.eLpNorm_mul_sqrt_rnDeriv hm u]
-  exact (Lp.memLp u).2
+  exact Lp.memLp u
 
 /-- Multiplication by `√(dm/dμ)` transports the real `L²` seminorm. -/
 private lemma Lp.lpNorm_mul_sqrt_rnDeriv {Ω : Type*} {mΩ : MeasurableSpace Ω} {m μ : Measure Ω}
     [SigmaFinite m] [m.HaveLebesgueDecomposition μ] (hm : m ≪ μ) (u : Ω →₂[m] ℝ) :
     lpNorm (fun ω => u ω * √(m.rnDeriv μ ω).toReal) 2 μ = lpNorm u 2 m := by
-  rw [← toReal_eLpNorm (Lp.memLp_mul_sqrt_rnDeriv hm u).aestronglyMeasurable,
-    ← toReal_eLpNorm (Lp.memLp u).aestronglyMeasurable, Lp.eLpNorm_mul_sqrt_rnDeriv hm u]
+  rw [← toReal_eLpNorm, ← toReal_eLpNorm, Lp.eLpNorm_mul_sqrt_rnDeriv hm u]
 
 /-- The real `Lᵖ` seminorm is invariant under almost-everywhere equality. -/
 private lemma lpNorm_congr_ae {Ω F : Type*} {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F]
     {μ : Measure Ω} {p : ℝ≥0∞} {f g : Ω → F} (hfg : f =ᵐ[μ] g) :
     lpNorm f p μ = lpNorm g p μ := by
-  by_cases hf : AEStronglyMeasurable f μ
-  · have hg : AEStronglyMeasurable g μ := hf.congr hfg
-    rw [← toReal_eLpNorm hf, ← toReal_eLpNorm hg, eLpNorm_congr_ae hfg]
-  · have hg : ¬ AEStronglyMeasurable g μ := fun hg => hf (hg.congr hfg.symm)
-    simp [lpNorm, hf, hg]
+  rw [← toReal_eLpNorm, ← toReal_eLpNorm, eLpNorm_congr_ae hfg]
 
 /-- If two versions of a random variable agree almost everywhere under a measure with density
 `p` with respect to `μ`, then the density `p` vanishes `μ`-almost everywhere on the set where the
@@ -231,7 +226,7 @@ private lemma lpNorm_score_eq_norm {Ω E : Type*} {mΩ : MeasurableSpace Ω} [Se
     refine Lp.lpNorm_mul_sqrt_rnDeriv_of_ae_eq hsθ ((2⁻¹ : ℝ) • A v) ?_
     exact (Lp.coeFn_smul (2⁻¹ : ℝ) (A v)).symm
   _ = ‖(2⁻¹ : ℝ) • A v‖ := by
-    rw [← toReal_eLpNorm (Lp.memLp ((2⁻¹ : ℝ) • A v)).aestronglyMeasurable, ← Lp.norm_def]
+    rw [← toReal_eLpNorm, ← Lp.norm_def]
 
 /-- After dividing by the scalar used in a local path, the transported score term is bounded above
 by the unscaled score term. -/
@@ -502,7 +497,6 @@ private lemma score_tendsto_zero' {Ω E : Type*} {mΩ : MeasurableSpace Ω} [Add
   rw [Lp.norm_def, toReal_eLpNorm]
   · refine (Lp.lpNorm_mul_sqrt_rnDeriv_of_ae_eq (hs _ hθ) ((2⁻¹ : ℝ) • A (p.1 • h)) ?_).symm
     exact(Lp.coeFn_smul (2⁻¹ : ℝ) (A (p.1 • h))).symm
-  · fun_prop
 
 /-- The square-root density itself is continuous along an admissible Hadamard path in `L²(μ)`. -/
 private lemma tendsto_sqrt_density {Ω E : Type*} {mΩ : MeasurableSpace Ω} [AddCommMonoid E]

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/subverso",
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "rev": "17e9f587d815324cbb86deaa91761c9741696ac7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "inputRev": "17e9f587d815324cbb86deaa91761c9741696ac7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "afc2695efcb6855264d85a45632db1ddc56c8774",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "50cd21bc62f2c8357c4f269d1185921cbfcdfc90",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "87dfe779d5dfd03142ee4fe158911b8eb553ec98",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "36cb0105a76ff3de70add8ae91afb6cfc57fafe3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "d93a8a0622807953d1e424f0fe2a5f5b5520c12e",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "914928598160c128affd7a42640b4237b7e4d912",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.35.0-rc3",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Statlib",

lakefile.toml

@@ -13,7 +13,7 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "0df444a360eaa60ab8c11dca51a86af692955474"
+rev = "17e9f587d815324cbb86deaa91761c9741696ac7"
 
 [[require]]
 name = "subverso"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.35.0-rc3