Bump mathlib

PFR.lean

@@ -39,7 +39,6 @@ import PFR.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
 import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
 import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
 import PFR.Mathlib.MeasureTheory.Constructions.Pi
-import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn
 import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Mathlib.MeasureTheory.Measure.Prod
@@ -48,6 +47,7 @@ import PFR.Mathlib.Probability.IdentDistrib
 import PFR.Mathlib.Probability.Independence.Basic
 import PFR.Mathlib.Probability.Independence.FourVariables
 import PFR.Mathlib.Probability.Independence.Kernel
+import PFR.Mathlib.Probability.Independence.ThreeVariables
 import PFR.Mathlib.Probability.Kernel.Composition
 import PFR.Mathlib.Probability.Kernel.Disintegration
 import PFR.Mathlib.Probability.UniformOn

PFR/ApproxHomPFR.lean

@@ -162,7 +162,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   obtain ⟨c', h, hch⟩ := this
   use φ, -φ c'.1 + c'.2 + h
   refine le_trans ?_ hch
-  unfold_let cH₁
+  unfold cH₁
   rewrite [hA, ← mul_inv, inv_mul_eq_div, div_div]
   apply div_le_div (Nat.cast_nonneg _) le_rfl
   · apply mul_pos

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -1,6 +1,5 @@
 import Mathlib.MeasureTheory.Integral.Prod
 import PFR.ForMathlib.Entropy.Measure
-import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Mathlib.Probability.Kernel.Disintegration
 

PFR/ForMathlib/FiniteMeasureComponent.lean

@@ -15,7 +15,7 @@ lemma continuous_finiteMeasure_apply_of_isClopen
     {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
     {s : Set α} (s_clopen : IsClopen s) :
     Continuous fun μ : FiniteMeasure α ↦ (μ : Measure α).real s := by
-  convert FiniteMeasure.continuous_integral_boundedContinousFunction
+  convert FiniteMeasure.continuous_integral_boundedContinuousFunction
     (BoundedContinuousFunction.indicator s s_clopen)
   have s_mble : MeasurableSet s := s_clopen.isOpen.measurableSet
   simp [integral_indicator, s_mble, Measure.real]

PFR/Mathlib/Probability/Kernel/Disintegration.lean

@@ -546,7 +546,7 @@ lemma _root_.MeasureTheory.Measure.ae_of_compProd_eq_zero {α β : Type*}
     ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s) = 0 := by
   let t := toMeasurable (μ ⊗ₘ κ) s
   have ht : (μ ⊗ₘ κ) t = 0 := by
-    unfold_let t
+    unfold t
     rwa [measure_toMeasurable]
   rw [Measure.compProd_apply (measurableSet_toMeasurable _ _), lintegral_eq_zero_iff] at ht
   swap; · exact measurable_kernel_prod_mk_left (measurableSet_toMeasurable _ _)

PFR/MoreRuzsaDist.lean

@@ -747,7 +747,7 @@ lemma multiDist_indep {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (X : Fin m
 
 lemma multiDist_nonneg_of_indep [Fintype G] {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)
     (hprob : IsProbabilityMeasure (ℙ : Measure Ω)) (X : Fin m → Ω → G) (hX : ∀ i, Measurable (X i))
-    (hindep : iIndepFun (fun i => inferInstance) X ℙ) :
+    (hindep : iIndepFun (fun _ => inferInstance) X ℙ) :
     D[X ; fun _ ↦ hΩ] ≥ 0 := by
   rw [multiDist_indep hΩ X hindep]
   by_cases hm : m = 0

PFR/Tactic/RPowSimp.lean

@@ -301,7 +301,7 @@ macro "rpow_simp" extras:(simpArgs)? loc:(location)? : tactic => `(tactic|
       [abs_one, abs_mul, abs_inv, abs_div, abs_abs, abs_zero, mul_rpow, ← rpow_mul, div_rpow,
        ← rpow_natCast, abs_rpow_of_nonneg, rpow_one, ← rpow_add, ← rpow_sub, zero_rpow, one_rpow,
        rpow_one, inv_rpow', rpow_inv] $(loc)? <;> try push_cast) <;>
-   try rpow_ring) <;> try field_simp only $(extras)? $(loc)?) <;> try ring_nf (config:={}) $(loc)?) <;>
+   try rpow_ring) <;> try field_simp only $(extras)? $(loc)?)) <;>
    try simp (discharger := positivity) only [abs_one, abs_zero, one_rpow, rpow_one, rpow_zero,
      mul_zero, zero_mul, mul_one, one_mul, fix_cast₁, fix_cast₂, fix_cast₃, Nat.cast_one, inv_rpow',
      rpow_inv] $(loc)?)

PFR/WeakPFR.lean

@@ -515,7 +515,7 @@ lemma single_fibres {G H Ω Ω': Type*}
   let M := H[φ.toFun ∘ UA] + H[φ.toFun ∘ UB]
   have hM : M = ∑ x in X, ∑ y in Y, Real.negMulLog (p x y) := by
     have h_compl {x y} (h_notin : (x, y) ∉ X ×ˢ Y) : Real.negMulLog (p x y) = 0 := by
-      unfold_let p; beta_reduce
+      unfold p
       rewrite [Finset.mem_product, not_and_or] at h_notin
       suffices A_ x = ∅ ∨ B_ y = ∅ by obtain h | h := this <;> rw [h] <;> simp
       refine h_notin.imp ?_ ?_
@@ -525,7 +525,7 @@ lemma single_fibres {G H Ω Ω': Type*}
       · rw [← not_nonempty_iff_eq_empty]
         rintro h ⟨a, ha, rfl⟩
         exact h (h_BY ⟨a, ha⟩)
-    unfold_let M
+    unfold M
     unfold entropy
     haveI := isProbabilityMeasure_map (μ := ℙ)
       ((Measurable.of_discrete (f := φ)).comp hUA').aemeasurable
@@ -555,7 +555,7 @@ lemma single_fibres {G H Ω Ω': Type*}
       rewrite [← left_distrib]
       apply mul_le_mul_of_nonneg_left
       · linarith
-      · unfold_let M
+      · unfold M
         linarith only [entropy_nonneg (φ.toFun ∘ UA) ℙ, entropy_nonneg (φ.toFun ∘ UB) ℙ]
   have : ∃ x : X, ∃ y : Y,
       M * dᵤ[A_ x.val # B_ y.val] + d[φ.toFun ∘ UA # φ.toFun ∘ UB] * -Real.log (p x.val y.val) ≤

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "af731107d531b39cd7278c73f91c573f40340612",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b",
+   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "88fac4fdcd3f426be4d972e0d3a7c78458e0bf01",
+   "rev": "62a2cc31bac6416736c17a57383a622c208f21cb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5c16c6a9a8bb45be40bdd773f0d2f09310c03773",
+   "rev": "cb34568b42bd7e241d86c011fd268c4180ebc0ae",
    "name": "LeanAPAP",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
+   "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.14.0-rc2