chore: bump Mathlib to 2ddf59c

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,

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

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

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

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

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

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ρν))

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²(μ)`. -/

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

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

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",

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"