Bump mathlib

PFR.lean

@@ -32,20 +32,16 @@ import PFR.ImprovedPFR
 import PFR.Kullback
 import PFR.Main
 import PFR.Mathlib.Algebra.AddTorsor
-import PFR.Mathlib.Algebra.Module.ZMod
 import PFR.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
 import PFR.Mathlib.Data.Set.Pointwise.SMul
-import PFR.Mathlib.GroupTheory.PGroup
 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.NullMeasurable
-import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import PFR.Mathlib.MeasureTheory.Measure.Prod
 import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib

PFR/ForMathlib/ConditionalIndependence.lean

@@ -131,7 +131,7 @@ open Function Set Measure
 /-- For `X, Y` random variables, there exist conditionally independent trials `X_1, X_2, Y'`. -/
 lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y)
     [finY : FiniteRange Y] (μ : Measure Ω) [IsProbabilityMeasure μ] :
-    ∃ (Ω' : Type u) (mΩ' : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
+    ∃ (Ω' : Type u) (_ : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
       IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧
       CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧
       IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ := by
@@ -265,7 +265,7 @@ lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY :
 lemma condIndep_copies' (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y)
     [FiniteRange Y] (μ : Measure Ω) [IsProbabilityMeasure μ] (p : α → β → Prop)
     (hp : Measurable (uncurry p)) (hp' : ∀ᵐ ω ∂μ, p (X ω) (Y ω)) :
-    ∃ (Ω' : Type u) (mΩ' : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
+    ∃ (Ω' : Type u) (_ : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
       IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧
       CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧
        IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ ∧ (∀ ω, p (X₁ ω) (Y' ω)) ∧ (∀ ω, p (X₂ ω) (Y' ω)) := by

PFR/ForMathlib/Entropy/RuzsaDist.lean

@@ -32,8 +32,6 @@ variable {Ω Ω' Ω'' Ω''' G S T : Type*}
   [mΩ'' : MeasurableSpace Ω''] {μ'' : Measure Ω''}
   [mΩ''' : MeasurableSpace Ω'''] {μ''' : Measure Ω'''}
   [hG : MeasurableSpace G]
-  --[Countable S] [Nonempty S] [MeasurableSpace S]
-  --[Countable T] [Nonempty T] [MeasurableSpace T]
 
 /-- Entropy depends continuously on the measure. -/
 -- TODO: Use notation `Hm[μ]` here? (figure out how)

PFR/ForMathlib/Entropy/RuzsaSetDist.lean

@@ -98,7 +98,7 @@ lemma isUniform_iff_uniform_dist {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : M
         rfl
   intro this
   constructor
-  · intro x y hx hy
+  · intro x hx y hy
     replace hx : {x} ∩ H = {x} := by simp [hx]
     replace hy : {y} ∩ H = {y} := by simp [hy]
     simp [← map_apply hU (MeasurableSet.singleton _), this, discreteUniform_apply, hx, hy]

PFR/ForMathlib/FiniteMeasureComponent.lean

@@ -1,12 +1,12 @@
+import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import PFR.ForMathlib.MeasureReal
-import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 
 /-!
 # The measure of a connected component of a space depends continuously on a finite measure
 -/
 
 open MeasureTheory Topology Metric Filter Set ENNReal NNReal
-open scoped Topology ENNReal NNReal BoundedContinuousFunction
+open scoped Topology ENNReal NNReal
 
 section measure_of_component
 
@@ -15,11 +15,10 @@ 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_boundedContinuousFunction
+  convert FiniteMeasure.continuous_integral_boundedContinousFunction
     (BoundedContinuousFunction.indicator s s_clopen)
   have s_mble : MeasurableSet s := s_clopen.isOpen.measurableSet
-  rw [integral_indicatorBCF _ s_clopen s_mble]
-  rfl
+  simp [integral_indicator, s_mble, Measure.real]
 
 /-- The probability of any connected component depends continuously on the `ProbabilityMeasure`.-/
 lemma continuous_probabilityMeasure_apply_of_isClopen
@@ -29,7 +28,6 @@ lemma continuous_probabilityMeasure_apply_of_isClopen
   convert ProbabilityMeasure.continuous_integral_boundedContinuousFunction
     (BoundedContinuousFunction.indicator s s_clopen)
   have s_mble : MeasurableSet s := s_clopen.isOpen.measurableSet
-  rw [integral_indicatorBCF _ s_clopen s_mble]
-  rfl
+  simp [integral_indicator, s_mble, Measure.real]
 
 end measure_of_component -- section

PFR/ForMathlib/GroupQuot.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.EuclideanDomain.Int
+import Mathlib.Algebra.Module.ZMod
 import Mathlib.LinearAlgebra.Dimension.Free
-import PFR.Mathlib.Algebra.Module.ZMod
 
 /-!
 If `G` is a rank `d` free `ℤ`-module, then `G/nG` is a finite group of cardinality `n ^ d`.
@@ -13,7 +13,7 @@ variable {G : Type*} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ}
 variable (G n) in
 abbrev modN : Type _ := G ⧸ LinearMap.range (LinearMap.lsmul ℤ G n)
 
-instance : Module (ZMod n) (modN G n) := QuotientAddGroup.instZModModule (by simp)
+instance : Module (ZMod n) (modN G n) := QuotientAddGroup.zmodModule (by simp)
 
 variable [NeZero n]
 

PFR/ForMathlib/MeasureReal.lean

@@ -1,6 +1,5 @@
 import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.Tactic.Finiteness
-import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
 
 /-!
 # Measures as real valued-functions

PFR/ForMathlib/Uniform.lean

@@ -17,16 +17,15 @@ While in applications $H$ will be non-empty finite set, $X$ measurable, and and
 measure, it could be technically convenient to have a definition that works even without these
 hypotheses. (For instance, `isUniform` would be well-defined, but false, for infinite `H`).
 
-This should probably be refactored, requiring instead that `μ.map X = uniformOn H` -- but at the
-time of writing `uniformOn` did not exist in mathlib. -/
-structure IsUniform (H : Set S) (X : Ω → S) (μ : Measure Ω := by volume_tac) : Prop :=
-  eq_of_mem : ∀ x y, x ∈ H → y ∈ H → μ (X ⁻¹' {x}) = μ (X ⁻¹' {y})
+This should probably be refactored, requiring instead that `μ.map X = uniformOn H`. -/
+structure IsUniform (H : Set S) (X : Ω → S) (μ : Measure Ω := by volume_tac) : Prop where
+  eq_of_mem ⦃x⦄ (hx : x ∈ H) ⦃y⦄ (hy : y ∈ H) : μ (X ⁻¹' {x}) = μ (X ⁻¹' {y})
   measure_preimage_compl : μ (X ⁻¹' Hᶜ) = 0
 
 lemma isUniform_uniformOn [MeasurableSingletonClass Ω] {A : Set Ω} :
     IsUniform A id (uniformOn A) := by
   constructor
-  · intro x y hx hy
+  · intro x hx y hy
     have h'x : {x} ∩ A = {x} := by ext y; simp (config := {contextual := true}) [hx]
     have h'y : {y} ∩ A = {y} := by ext y; simp (config := {contextual := true}) [hy]
     simp [uniformOn, cond, h'x, h'y]
@@ -35,45 +34,43 @@ lemma isUniform_uniformOn [MeasurableSingletonClass Ω] {A : Set Ω} :
 /-- Uniform distributions exist. -/
 lemma exists_isUniform [MeasurableSpace S] [MeasurableSingletonClass S]
     (H : Finset S) (h : H.Nonempty) :
-    ∃ (Ω : Type uS) (mΩ : MeasurableSpace Ω) (X : Ω → S) (μ : Measure Ω),
-    IsProbabilityMeasure μ ∧ Measurable X ∧ IsUniform H X μ ∧ (∀ ω : Ω, X ω ∈ H)
-      ∧ FiniteRange X := by
-  refine ⟨H, Subtype.instMeasurableSpace, (fun x ↦ x),
-      (Finset.card H : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac i, ?_, measurable_subtype_coe, ?_, fun x ↦ x.2, ?_⟩
+    ∃ (Ω : Type uS) (_ : MeasurableSpace Ω) (X : Ω → S) (μ : Measure Ω),
+      IsProbabilityMeasure μ ∧ Measurable X ∧ IsUniform H X μ ∧ (∀ ω, X ω ∈ H) ∧ FiniteRange X := by
+  refine ⟨H, Subtype.instMeasurableSpace, fun x ↦ x, (Finset.card H : ℝ≥0∞)⁻¹ • ∑ i, .dirac i, ?_,
+    measurable_subtype_coe, ⟨?_, ?_⟩, fun x ↦ x.2, ?_⟩
   · constructor
     simp only [Finset.univ_eq_attach, Measure.smul_apply, Measure.coe_finset_sum, Finset.sum_apply,
       measure_univ, Finset.sum_const, Finset.card_attach, nsmul_eq_mul, mul_one, smul_eq_mul]
     rw [ENNReal.inv_mul_cancel]
     · simpa using h.ne_empty
     · simp
-  · constructor
-    · intro x y hx hy
-      simp only [Finset.univ_eq_attach, Measure.smul_apply, Measure.coe_finset_sum,
-        Finset.sum_apply, Measure.dirac_apply, smul_eq_mul]
-      rw [Finset.sum_eq_single ⟨x, hx⟩, Finset.sum_eq_single ⟨y, hy⟩]
-      · simp
-      · rintro ⟨b, bH⟩ _hb h'b
-        simp only [ne_eq, Subtype.mk.injEq] at h'b
-        simp [h'b]
-      · simp
-      · rintro ⟨b, bH⟩ _hb h'b
-        simp only [ne_eq, Subtype.mk.injEq] at h'b
-        simp [h'b]
-      · simp
+  · intro x hx y hy
+    simp only [Finset.univ_eq_attach, Measure.smul_apply, Measure.coe_finset_sum,
+      Finset.sum_apply, Measure.dirac_apply, smul_eq_mul]
+    rw [Finset.sum_eq_single ⟨x, hx⟩, Finset.sum_eq_single ⟨y, hy⟩]
+    · simp
+    · rintro ⟨b, bH⟩ _hb h'b
+      simp only [ne_eq, Subtype.mk.injEq] at h'b
+      simp [h'b]
     · simp
-  apply finiteRange_of_finset _ H _
-  simp
+    · rintro ⟨b, bH⟩ _hb h'b
+      simp only [ne_eq, Subtype.mk.injEq] at h'b
+      simp [h'b]
+    · simp
+  · simp
+  · apply finiteRange_of_finset _ H _
+    simp
 
 /-- The image of a uniform random variable under an injective map is uniform on the image. -/
 lemma IsUniform.comp [DecidableEq T] {H : Finset S} (h : IsUniform H X μ) {f : S → T} (hf : Injective f) :
     IsUniform (Finset.image f H) (f ∘ X) μ where
   eq_of_mem := by
-    intro x y hx hy
+    intro x hx y hy
     simp only [Finset.coe_image, mem_image, Finset.mem_coe] at hx hy
     rcases hx with ⟨x, hx, rfl⟩
     rcases hy with ⟨y, hy, rfl⟩
     have A z : f ⁻¹' {f z} = {z} := by ext; simp [hf.eq_iff]
-    simp [preimage_comp, A, h.eq_of_mem x y hx hy]
+    simp [preimage_comp, A, h.eq_of_mem hx hy]
   measure_preimage_compl := by simpa [preimage_comp, hf] using h.measure_preimage_compl
 
 /-- Uniform distributions exist, version giving a measure space -/
@@ -140,7 +137,7 @@ lemma IsUniform.measure_preimage_of_mem
       · intro y _hy
         exact hX .of_discrete
     _ = ∑ _x in H, μ (X ⁻¹' {s}) :=
-      Finset.sum_congr rfl (fun x hx ↦ h.eq_of_mem x s (by simpa using hx) hs)
+      Finset.sum_congr rfl fun x hx ↦ h.eq_of_mem (by simpa using hx) hs
     _ = H.card * μ (X ⁻¹' {s}) := by simp
     _ = (Nat.card H) * μ (X ⁻¹' {s}) := by
       congr; simp
@@ -206,10 +203,10 @@ lemma IsUniform.of_identDistrib {Ω' : Type*} [MeasurableSpace Ω'] (h : IsUnifo
     {X' : Ω' → S} {μ' : Measure Ω'} (h' : IdentDistrib X X' μ μ') (hH : MeasurableSet (H : Set S)) :
     IsUniform H X' μ' := by
   constructor
-  · intro x y hx hy
+  · intro x hx y hy
     rw [← h'.measure_mem_eq (MeasurableSet.singleton x),
       ← h'.measure_mem_eq (MeasurableSet.singleton y)]
-    apply h.eq_of_mem x y hx hy
+    apply h.eq_of_mem hx hy
   · rw [← h'.measure_mem_eq hH.compl]
     exact h.measure_preimage_compl
 
@@ -225,10 +222,10 @@ lemma IsUniform.measure_preimage_ne_zero {H : Finset S} [NeZero μ] (h : IsUnifo
 $H'$ on $H' \cap H$. -/
 lemma IsUniform.restrict {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (H' : Set S) :
     IsUniform (H' ∩ H) X (μ[|X ⁻¹' H']) where
-  eq_of_mem := fun x y hx hy ↦ by
+  eq_of_mem := fun x hx y hy ↦ by
     simp only [cond, Measure.smul_apply, smul_eq_mul]
     rw [μ.restrict_eq_self (preimage_mono (singleton_subset_iff.mpr hx.1)),
-      μ.restrict_eq_self (preimage_mono (singleton_subset_iff.mpr hy.1)), h.eq_of_mem x y hx.2 hy.2]
+      μ.restrict_eq_self (preimage_mono (singleton_subset_iff.mpr hy.1)), h.eq_of_mem hx.2 hy.2]
   measure_preimage_compl := le_zero_iff.mp <| by
     rewrite [Set.compl_inter, Set.preimage_union]
     calc

PFR/ForMathlib/ZModModule.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Module.ZMod
+import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.Sylow
-import PFR.Mathlib.GroupTheory.PGroup
 
 open Function Set ZMod
 

PFR/HundredPercent.lean

@@ -122,7 +122,7 @@ lemma isUniform_sub_const_of_rdist_eq_zero (hX : Measurable X) (hdist : d[X # X]
       have Z := (mem_symmGroup hX).1 (AddSubgroup.neg_mem (symmGroup X hX) hz)
       simp [← sub_eq_add_neg] at Z
       exact Z.symm.measure_mem_eq $ .of_discrete
-    intro x y hx hy
+    intro x hx y hy
     rw [A x hx, A y hy]
   measure_preimage_compl := by
     apply (measure_preimage_eq_zero_iff_of_countable (Set.to_countable _)).2

PFR/ImprovedPFR.lean

@@ -736,7 +736,7 @@ variable (p : refPackage Ω₀₁ Ω₀₂ G)
 all minimizers are fine, by `tau_strictly_decreases'`. For `p.η = 1/8`, we use a limit of
 minimizers for `η < 1/8`, which exists by compactness. -/
 lemma tau_minimizer_exists_rdist_eq_zero :
-    ∃ (Ω : Type uG) (mΩ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
+    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
       Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧ tau_minimizes p X₁ X₂
       ∧ d[X₁ # X₂] = 0 := by
   -- let `uₙ` be a sequence converging from below to `η`. In particular, `uₙ < 1/8`.