Bump mathlib

Author: YaelDillies

PFR/ApproxHomPFR.lean

@@ -1,7 +1,7 @@
 import Mathlib.Data.FunLike.Fintype
 import Mathlib.Data.Int.Lemmas
 
-import LeanAPAP.Extras.BSG
+import APAP.Extras.BSG
 
 import PFR.HomPFR
 

PFR/ForMathlib/Uniform.lean

@@ -260,7 +260,7 @@ lemma IsUniform.map_eq_uniformOn [Countable S] [IsProbabilityMeasure μ]
     {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (hH : H.Finite) (h'H : H.Nonempty) :
     μ.map X = uniformOn H := by
   have : Finite H := hH
-  have : IsProbabilityMeasure (uniformOn H) := uniformOn_isProbabilityMeasure hH h'H
+  have : IsProbabilityMeasure (uniformOn H) := isProbabilityMeasure_uniformOn hH h'H
   have : IdentDistrib X id μ (uniformOn (H : Set S)) :=
     .of_isUniform (H := H) hX measurable_id h isUniform_uniformOn
   simpa using this.map_eq

PFR/Mathlib/Probability/UniformOn.lean

@@ -47,7 +47,7 @@ lemma uniformOn_real_singleton (hs : s.Finite) (ω : Ω) [Decidable (ω ∈ s)]
   simp [uniformOn_real hs, Set.ncard_inter_singleton]; split <;> simp
 
 instance uniformOn.instIsProbabilityMeasure [Nonempty s] [Finite s] :
-    IsProbabilityMeasure (uniformOn s) := uniformOn_isProbabilityMeasure ‹_› .of_subtype
+    IsProbabilityMeasure (uniformOn s) := isProbabilityMeasure_uniformOn ‹_› .of_subtype
 
 lemma map_uniformOn_apply {f : Ω → Ω'} (hmes : Measurable f) (hf : Injective f) {t : Set Ω'}
     (ht : MeasurableSet t) :

PFR/RhoFunctional.lean

@@ -39,7 +39,7 @@ lemma map_prod_uniformOn_ne_zero {y : G} (hA : A.Nonempty)
   obtain ⟨a, ha⟩ : ∃ x, x ∈ A := by exact hA
   let ν := uniformOn (A : Set G)
   have : IsProbabilityMeasure ν :=
-    uniformOn_isProbabilityMeasure A.finite_toSet hA
+    isProbabilityMeasure_uniformOn A.finite_toSet hA
   have h_indep : IndepFun Prod.fst Prod.snd (μ.prod ν) := ProbabilityTheory.indepFun_fst_snd
   rw [h_indep.map_add_singleton_eq_sum measurable_fst measurable_snd,
     Finset.sum_eq_zero_iff_of_nonneg (fun i _ ↦ by simp)] at h
@@ -53,10 +53,10 @@ lemma map_prod_uniformOn_ne_zero {y : G} (hA : A.Nonempty)
 lemma nonempty_rhoMinusSet [IsZeroOrProbabilityMeasure μ] (hA : A.Nonempty) :
     Set.Nonempty (rhoMinusSet X A μ) := by
   rcases eq_zero_or_isProbabilityMeasure μ with hμ | hμ
-  · refine ⟨0, ⟨uniformOn (A : Set G), uniformOn_isProbabilityMeasure A.finite_toSet hA,
+  · refine ⟨0, ⟨uniformOn (A : Set G), isProbabilityMeasure_uniformOn A.finite_toSet hA,
       by simp [hμ], by simp [hμ, KLDiv]⟩⟩
   set μ' := uniformOn (univ : Set G) with hμ'
-  have : IsProbabilityMeasure μ' := uniformOn_isProbabilityMeasure finite_univ univ_nonempty
+  have : IsProbabilityMeasure μ' := isProbabilityMeasure_uniformOn finite_univ univ_nonempty
   refine ⟨_, ⟨μ', this, fun y hy ↦ (map_prod_uniformOn_ne_zero hA ?_ hy).elim, rfl⟩⟩
   intro x
   simp [hμ', uniformOn_apply_singleton_of_mem (mem_univ _) finite_univ]
@@ -110,7 +110,7 @@ lemma rhoMinus_le [IsZeroOrProbabilityMeasure μ]
   cases nonempty_fintype G
   have : IsProbabilityMeasure (μ'.map T) := isProbabilityMeasure_map hT.aemeasurable
   have : IsProbabilityMeasure (uniformOn (A : Set G)) :=
-    uniformOn_isProbabilityMeasure A.finite_toSet hA
+    isProbabilityMeasure_uniformOn A.finite_toSet hA
   have E : μ'.map U = uniformOn (A : Set G) := hunif.map_eq_uniformOn hU A.finite_toSet hA
   have M : (Measure.map (Prod.fst + Prod.snd) ((μ'.map T).prod (uniformOn ↑A))) =
       (Measure.map (T + U) μ') := by
@@ -133,7 +133,7 @@ lemma rhoMinus_nonneg [IsZeroOrProbabilityMeasure μ]
 lemma rhoMinus_zero_measure (hP : μ = 0)
     {X : Ω → G} {A : Finset G} : ρ⁻[X ; μ # A] = 0 := by
   have : ∃ (μ' : Measure G), IsProbabilityMeasure μ' :=
-    ⟨uniformOn Set.univ, uniformOn_isProbabilityMeasure finite_univ univ_nonempty⟩
+    ⟨uniformOn Set.univ, isProbabilityMeasure_uniformOn finite_univ univ_nonempty⟩
   simp [rhoMinus, rhoMinusSet, hP, this, KLDiv]
 
 private lemma rhoMinus_continuous_aux1 (hX : Measurable X) (hA : A.Nonempty)
@@ -147,7 +147,7 @@ private lemma rhoMinus_continuous_aux1 (hX : Measurable X) (hA : A.Nonempty)
   obtain ⟨u, -, u_mem, hu⟩ := exists_seq_strictAnti_tendsto' (x := (0 : ℝ≥0∞)) zero_lt_one
   let ν : ℕ → Measure G := fun n ↦ (1 - u n) • μ₀ + u n • uniformOn univ
   have : IsProbabilityMeasure (uniformOn (univ : Set G)) :=
-    uniformOn_isProbabilityMeasure finite_univ univ_nonempty
+    isProbabilityMeasure_uniformOn finite_univ univ_nonempty
   have P n : IsProbabilityMeasure (ν n) := by
     simp only [isProbabilityMeasure_iff, coe_add, coe_smul, Pi.add_apply, Pi.smul_apply,
       measure_univ, smul_eq_mul, mul_one, ν]
@@ -167,7 +167,7 @@ private lemma rhoMinus_continuous_aux1 (hX : Measurable X) (hA : A.Nonempty)
     · apply ENNReal.Tendsto.mul_const _ (by simp)
       exact ENNReal.Tendsto.sub tendsto_const_nhds hu (by simp)
     · exact ENNReal.Tendsto.mul_const hu (by simp)
-  let PA : ProbabilityMeasure G := ⟨uniformOn A, uniformOn_isProbabilityMeasure (A.finite_toSet) hA⟩
+  let PA : ProbabilityMeasure G := ⟨uniformOn A, isProbabilityMeasure_uniformOn (A.finite_toSet) hA⟩
   have : Tendsto (fun n ↦ (νP n).prod PA) atTop (𝓝 (μ₀P.prod PA)) :=
     (ProbabilityMeasure.continuous_prod.tendsto (μ₀P, PA)).comp (f := fun n ↦ (νP n, PA)) <|
       L.prodMk_nhds tendsto_const_nhds
@@ -461,7 +461,7 @@ private lemma le_rhoMinus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup
   let _ : MeasureSpace (G × G) := ⟨μ'.prod (uniformOn (A : Set G))⟩
   have hprod : (ℙ : Measure (G × G)) = μ'.prod (uniformOn (A : Set G)) := rfl
   have : IsProbabilityMeasure (uniformOn (A : Set G)) :=
-    uniformOn_isProbabilityMeasure A.finite_toSet hA
+    isProbabilityMeasure_uniformOn A.finite_toSet hA
   have : IsProbabilityMeasure (Measure.map T ℙ) := by rw [hprod, Measure.map_fst_prod]; simp [hμ']
   have h_indep : IndepFun T UA := ProbabilityTheory.indepFun_fst_snd
   have hUA_unif : IsUniform A UA := by
@@ -560,7 +560,7 @@ private lemma rhoMinus_le_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup
     rw [measureReal_def, μ'_sing]
     rfl
   have : IsProbabilityMeasure (uniformOn (A : Set G)) :=
-    uniformOn_isProbabilityMeasure A.finite_toSet hA
+    isProbabilityMeasure_uniformOn A.finite_toSet hA
   have : IsProbabilityMeasure μ' :=
     isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop))
   have h_indep : IndepFun Prod.fst Prod.snd (μ'.prod (uniformOn (A : Set G))) := indepFun_fst_snd
@@ -763,7 +763,7 @@ lemma rhoMinus_of_sum [IsZeroOrProbabilityMeasure μ]
   · simp [rhoMinus_zero_measure hμ]
   apply le_csInf (nonempty_rhoMinusSet hA)
   have : IsProbabilityMeasure (uniformOn (A : Set G)) :=
-    uniformOn_isProbabilityMeasure A.finite_toSet hA
+    isProbabilityMeasure_uniformOn A.finite_toSet hA
   rintro - ⟨μ', μ'_prob, habs, rfl⟩
   obtain ⟨Ω', hΩ', m, X', Y', T, U, hm, h_indep', hX', hY', hT, hU, hXX', hYY', hTμ, hU_unif⟩ :=
     independent_copies4_nondep (X₁ := X) (X₂ := Y) (X₃ := id) (X₄ := id) hX hY measurable_id
@@ -931,7 +931,7 @@ lemma condRhoMinus_le [IsZeroOrProbabilityMeasure μ] {S : Type*} [MeasurableSpa
     ρ⁻[X | Z ; μ # A] ≤ ρ⁻[X ; μ # A] + H[X ; μ] - H[X | Z ; μ] := by
   cases nonempty_fintype S
   have : IsProbabilityMeasure (uniformOn (A : Set G)) := by
-    apply uniformOn_isProbabilityMeasure A.finite_toSet hA
+    apply isProbabilityMeasure_uniformOn A.finite_toSet hA
   suffices ρ⁻[X | Z ; μ # A] - H[X ; μ] + H[X | Z ; μ] ≤ ρ⁻[X ; μ # A] by linarith
   apply le_csInf (nonempty_rhoMinusSet hA)
   rintro - ⟨μ', hμ', habs, rfl⟩

lake-manifest.json

@@ -11,31 +11,31 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/YaelDillies/LeanAPAP.git",
+  {"url": "https://github.com/YaelDillies/apap.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "96167d24d9724269561f5f1ed7d29d779157e4da",
-   "name": "LeanAPAP",
+   "rev": "13fd6dd3a47445b6dd10826f0ffc1116f4e13144",
+   "name": "APAP",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "507f18fc9044549fc730d8d0270521e3b090360a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": null,
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "0100f1a3222df01286db33fcb6a1f98564f5439d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "PFR",

lakefile.toml

@@ -14,9 +14,8 @@ weak.linter.mathlibStandardSet = true
 warn.sorry = false
 
 [[require]]
-name = "LeanAPAP"
-git = "https://github.com/YaelDillies/LeanAPAP.git"
-rev = "v4.27.0"
+name = "APAP"
+git = "https://github.com/YaelDillies/apap.git"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1