Bump mathlib

PFR.lean

@@ -32,36 +32,29 @@ import PFR.ImprovedPFR
 import PFR.Kullback
 import PFR.Main
 import PFR.Mathlib.Algebra.Group.Pointwise.Set.Basic
-import PFR.Mathlib.Algebra.Module.Submodule.Ker
-import PFR.Mathlib.Algebra.Module.Submodule.Map
-import PFR.Mathlib.Algebra.Module.Submodule.Range
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
 import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Mathlib.Data.Set.Pointwise.SMul
-import PFR.Mathlib.Data.ZMod.Basic
 import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
 import PFR.Mathlib.MeasureTheory.Constructions.Pi
-import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
 import PFR.Mathlib.MeasureTheory.Integral.Bochner
 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
 import PFR.Mathlib.Probability.Independence.Basic
 import PFR.Mathlib.Probability.Independence.FourVariables
 import PFR.Mathlib.Probability.Independence.Kernel
 import PFR.Mathlib.Probability.Kernel.Composition
 import PFR.Mathlib.Probability.Kernel.Disintegration
-import PFR.Mathlib.Probability.Kernel.MeasureCompProd
 import PFR.Mathlib.SetTheory.Cardinal.Finite
 import PFR.MoreRuzsaDist
 import PFR.MultiTauFunctional
 import PFR.RhoFunctional
 import PFR.SecondEstimate
-import PFR.Tactic.Finiteness
-import PFR.Tactic.Finiteness.Attr
 import PFR.Tactic.RPowSimp
 import PFR.TauFunctional
 import PFR.TorsionEndgame

PFR/ApproxHomPFR.lean

@@ -88,7 +88,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
         refine ⟨c + (h, φ h), ⟨⟨c, hc.1, (h, φ h), ?_⟩, by rwa [← hc.2] at hch⟩⟩
         exact ⟨(hH₀H₁ ⟨h, φ h⟩).mpr ⟨hh, by rw [sub_self]; apply zero_mem⟩, rfl⟩
     rewrite [← h_proj_A'', h_proj_c] at h_le
-    apply (h_le.trans Set.card_add_le).trans
+    apply (h_le.trans Set.natCard_add_le).trans
     gcongr
     exact Nat.card_image_le c.toFinite
 

PFR/Endgame.lean

@@ -325,7 +325,8 @@ lemma sum_dist_diff_le [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2
 omit [Fintype G] hG [MeasurableSingletonClass G] mΩ in
 /-- `U + V + W = 0`. -/
 lemma sum_uvw_eq_zero [Module (ZMod 2) G] : U + V + W = 0 := by
-  simp [add_assoc, add_left_comm (a := X₁), add_left_comm (a := X₂)]
+  simp [add_assoc, add_left_comm (a := X₁), add_left_comm (a := X₂), ← ZModModule.sub_eq_add X₁',
+    ZModModule.add_self]
 
 section construct_good
 variable {Ω' : Type*} [MeasureSpace Ω']
@@ -373,10 +374,10 @@ lemma construct_good_prelim :
   have hp.η : 0 ≤ p.η := by linarith [p.hη]
   have hP : IsProbabilityMeasure (Measure.map T₃ ℙ) := isProbabilityMeasure_map hT₃.aemeasurable
   have h2T₃ : T₃ = T₁ + T₂ :=
-    calc T₃ = T₁ + T₂ + T₃ - T₃ := by rw [hT, zero_sub]; simp
+    calc T₃ = T₁ + T₂ + T₃ - T₃ := by rw [hT, zero_sub]; simp [ZModModule.neg_eq_self]
       _ = T₁ + T₂ := by rw [add_sub_cancel_right]
-  have h2T₁ : T₁ = T₂ + T₃ := by simp [h2T₃, add_left_comm]
-  have h2T₂ : T₂ = T₃ + T₁ := by simp [h2T₁, add_left_comm]
+  have h2T₁ : T₁ = T₂ + T₃ := by simp [h2T₃, add_left_comm, ZModModule.add_self]
+  have h2T₂ : T₂ = T₃ + T₁ := by simp [h2T₁, add_left_comm, ZModModule.add_self]
 
   have h1 : sum1 ≤ δ := by
     have h1 : sum1 ≤ 3 * I[T₁ : T₂] + 2 * H[T₃] - H[T₁] - H[T₂] := by
@@ -416,7 +417,7 @@ lemma construct_good_prelim :
     suffices (Measure.map T₃ ℙ)[fun _ ↦ k] ≤ sum4 by simpa using this
     refine integral_mono_ae .of_finite .of_finite $ ae_iff_of_countable.2 fun t ht ↦ ?_
     have : IsProbabilityMeasure (ℙ[|T₃ ⁻¹' {t}]) :=
-      cond_isProbabilityMeasure ℙ (by simpa [hT₃] using ht)
+      cond_isProbabilityMeasure (by simpa [hT₃] using ht)
     dsimp only
     linarith only [distance_ge_of_min' (μ := ℙ[|T₃ ⁻¹' {t}]) (μ' := ℙ[|T₃ ⁻¹' {t}]) p h_min hT₁ hT₂]
   exact hk.trans h4
@@ -483,7 +484,7 @@ lemma cond_construct_good [IsProbabilityMeasure (ℙ : Measure Ω)] :
   gcongr (?_ * ?_)
   · apply rdist_nonneg hX₁ hX₂
   · rfl
-  have : IsProbabilityMeasure (ℙ[|R ⁻¹' {r}]) := cond_isProbabilityMeasure ℙ hr
+  have : IsProbabilityMeasure (ℙ[|R ⁻¹' {r}]) := cond_isProbabilityMeasure hr
   apply construct_good' p X₁ X₂ h_min hT hT₁ hT₂ hT₃
 
 end construct_good

PFR/Fibring.lean

@@ -193,4 +193,4 @@ lemma sum_of_rdist_eq_char_2
       = d[(Y 0) + (Y 2); μ # (Y 1) + (Y 3); μ]
         + d[Y 0 | (Y 0) + (Y 2); μ # Y 1 | (Y 1) + (Y 3); μ]
         + I[(Y 0) + (Y 1) : (Y 1) + (Y 3) | (Y 0) + (Y 1) + (Y 2) + (Y 3); μ] := by
-  simpa using sum_of_rdist_eq Y h_indep h_meas
+  simpa [ZModModule.sub_eq_add] using sum_of_rdist_eq Y h_indep h_meas

PFR/FirstEstimate.lean

@@ -173,7 +173,8 @@ lemma ent_ofsum_le
     · refine add_le_add (add_le_add (le_refl _) ?_) ?_
       · apply (mul_le_mul_left p.hη).mpr lem611c
       · apply (mul_le_mul_left p.hη).mpr lem611d
-  have ent_sub_eq_ent_add : H[X₁ + X₂' - (X₂ + X₁')] = H[X₁ + X₂' + (X₂ + X₁')] := by simp
+  have ent_sub_eq_ent_add : H[X₁ + X₂' - (X₂ + X₁')] = H[X₁ + X₂' + (X₂ + X₁')] := by
+    simp [ZModModule.sub_eq_add]
   have rw₁ : X₁ + X₂' + (X₂ + X₁') = X₁ + X₂ + X₁' + X₂' := by abel
   have ind_aux : IndepFun (X₁ + X₂') (X₂ + X₁') := by
     exact iIndepFun.indepFun_add_add h_indep (fun i ↦ by fin_cases i <;> assumption) 0 2 1 3
@@ -190,7 +191,7 @@ lemma ent_ofsum_le
       have k_eq_aux : k = d[X₁ # X₂'] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂
       rw [k_eq_aux]
       exact (h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)).rdist_eq hX₁ hX₂'
-    rw [k_eq, ← Module.sub_eq_add, ← HX₂_eq]
+    rw [k_eq, ← ZModModule.sub_eq_add, ← HX₂_eq]
     ring
   have rw₃ : H[X₂ + X₁'] = k + H[X₁]/2 + H[X₂]/2 := by
     have HX₁_eq : H[X₁] = H[X₁'] :=
@@ -200,7 +201,7 @@ lemma ent_ofsum_le
         IdentDistrib.rdist_eq h₁ (IdentDistrib.refl hX₂.aemeasurable)
       rw [k_eq_aux]
       exact IndepFun.rdist_eq (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)) hX₁' hX₂
-    rw [add_comm X₂ X₁', k_eq', ← Module.sub_eq_add, ← HX₁_eq]
+    rw [add_comm X₂ X₁', k_eq', ← ZModModule.sub_eq_add, ← HX₁_eq]
     ring
   calc H[X₁ + X₂ + X₁' + X₂']
       ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁  := obs

PFR/ForMathlib/ConditionalIndependence.lean

@@ -1,8 +1,8 @@
+import Mathlib.Tactic.Finiteness
 import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib
 import PFR.ForMathlib.FiniteRange.ConditionalProbability
 import PFR.ForMathlib.Pair
-import PFR.Tactic.Finiteness
 
 open MeasureTheory Measure Set
 open scoped ENNReal
@@ -23,7 +23,7 @@ theorem IndepFun.identDistrib_cond [IsProbabilityMeasure μ]
     IdentDistrib A A μ (μ[|B ⁻¹' s]) := by
   refine ⟨hA.aemeasurable, hA.aemeasurable, ?_⟩
   ext t ht
-  rw [Measure.map_apply hA ht, Measure.map_apply hA ht, cond_apply _ (hB hs), Set.inter_comm,
+  rw [Measure.map_apply hA ht, Measure.map_apply hA ht, cond_apply (hB hs), Set.inter_comm,
     hi.measure_inter_preimage_eq_mul _ _ ht hs, mul_comm, mul_assoc,
     ENNReal.mul_inv_cancel h (by finiteness), mul_one]
 
@@ -34,7 +34,7 @@ lemma IndepFun.cond_left (hi : IndepFun A B μ) {s : Set α}
     IndepFun A B (μ[| A⁻¹' s]) := by
   apply indepFun_iff_measure_inter_preimage_eq_mul.2 (fun u v hu hv ↦ ?_)
   have : A ⁻¹' s ∩ (A ⁻¹' u ∩ B ⁻¹' v) = A ⁻¹' (s ∩ u) ∩ B ⁻¹' v := by aesop
-  simp only [cond_apply _ (hA hs), this]
+  simp only [cond_apply (hA hs), this]
   rcases eq_or_ne (μ (A ⁻¹' s)) ∞ with h|h
   · simp [h]
   rcases eq_or_ne (μ (A ⁻¹' s)) 0 with h'|h'
@@ -64,7 +64,7 @@ lemma IndepFun.cond (hi : IndepFun A B μ) {s : Set α} {t : Set β}
   have I1 : A ⁻¹' s ∩ B ⁻¹' t ∩ (A ⁻¹' u ∩ B ⁻¹' v) = A ⁻¹' (s ∩ u) ∩ B ⁻¹' (t ∩ v) := by aesop
   have I2 : A ⁻¹' s ∩ B ⁻¹' t ∩ A ⁻¹' u = A ⁻¹' (s ∩ u) ∩ B ⁻¹' t := by aesop
   have I3 : A ⁻¹' s ∩ B ⁻¹' t ∩ B ⁻¹' v = A ⁻¹' s ∩ B ⁻¹' (t ∩ v) := by aesop
-  simp only [cond_apply _ ((hA hs).inter (hB ht)), I1, I2, I3]
+  simp only [cond_apply ((hA hs).inter (hB ht)), I1, I2, I3]
   rcases eq_or_ne (μ (A ⁻¹' s ∩ B⁻¹' t)) ∞ with h|h
   · simp [h]
   rcases eq_or_ne (μ (A ⁻¹' s ∩ B⁻¹' t)) 0 with h'|h'
@@ -114,7 +114,7 @@ lemma CondIndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi'
   rw [condIndepFun_iff] at hfg ⊢
   rw [← Measure.map_map hh hi.measurable, hi.map_comap, restrict_eq_self_of_ae_mem hi']
   refine hfg.mono $ fun c hc ↦ ?_
-  rw [preimage_comp, ← comap_cond _ hi hi' $ hh $ .singleton _]
+  rw [preimage_comp, ← comap_cond hi hi' $ hh $ .singleton _]
   exact IndepFun.comp_right hi (cond_absolutelyContinuous.ae_le hi') hf hg hc
 
 end defs
@@ -156,7 +156,7 @@ lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY :
     rw [this, ← Measure.map_apply measurable_snd (MeasurableSet.singleton y).compl]
     simp [m]
   have h5 {y : β} (hy : μ (Y ⁻¹' {y}) ≠ 0) : IsProbabilityMeasure (m' y) := by
-    have : IsProbabilityMeasure (μ[|Y ← y]) := cond_isProbabilityMeasure μ hy
+    have : IsProbabilityMeasure (μ[|Y ← y]) := cond_isProbabilityMeasure hy
     exact isProbabilityMeasure_map hX.aemeasurable
   have h1 : ν.map Prod.snd = μ.map Y := by
     rw [← sum_meas_smul_cond_fiber' hY μ, ← Measure.mapₗ_apply_of_measurable measurable_snd,
@@ -166,7 +166,7 @@ lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY :
     rcases eq_or_ne (μ (Y ⁻¹' {y})) 0 with hy | hy
     · simp [hy]
     have h6 : IsProbabilityMeasure (m' y) := h5 hy
-    have h7 : IsProbabilityMeasure (μ[|Y ← y]) := cond_isProbabilityMeasure μ hy
+    have h7 : IsProbabilityMeasure (μ[|Y ← y]) := cond_isProbabilityMeasure hy
     congr 3
     rw [Measure.mapₗ_apply_of_measurable measurable_snd, Measure.mapₗ_apply_of_measurable hY]
     simp only [map_snd_prod, measure_univ, one_smul, m]
@@ -203,7 +203,7 @@ lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY :
     have h2 : ν[| Prod.snd⁻¹' {y}] = m y := by
       rw [Measure.ext_iff]
       intro E _
-      rw [cond_apply ν (measurable_snd (by simp)) E, hy']
+      rw [cond_apply (measurable_snd (by simp)), hy']
       have h3 : (m y) ((Prod.snd⁻¹' {y}) ∩ E) = (m y) E := by
         apply measure_congr
         apply inter_ae_eq_right_of_ae_eq_univ

PFR/ForMathlib/Entropy/Basic.lean

@@ -136,15 +136,15 @@ lemma entropy_eq_sum_finiteRange' [MeasurableSingletonClass S] (hX : Measurable
 lemma entropy_cond_eq_sum (μ : Measure Ω) (y : T) :
     H[X | Y ← y ; μ] = ∑' x, negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
   by_cases hy : μ (Y ⁻¹' {y}) = 0
-  · rw [entropy_def, cond_eq_zero_of_meas_eq_zero _ hy]
+  · rw [entropy_def, cond_eq_zero_of_meas_eq_zero hy]
     simp
   · rw [entropy_eq_sum]
 
 lemma entropy_cond_eq_sum_finiteRange [MeasurableSingletonClass S]
     (hX : Measurable X) (μ : Measure Ω) (y : T) [FiniteRange X]:
     H[X | Y ← y ; μ] = ∑ x in FiniteRange.toFinset X, negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
   by_cases hy : μ (Y ⁻¹' {y}) = 0
-  · rw [entropy_def, cond_eq_zero_of_meas_eq_zero _ hy]
+  · rw [entropy_def, cond_eq_zero_of_meas_eq_zero hy]
     simp
   · rw [entropy_eq_sum_finiteRange hX]
 
@@ -403,7 +403,7 @@ lemma condEntropy_eq_kernel_entropy [Nonempty S] [Countable S] [MeasurableSingle
   congr
   ext s hs
   rw [condDistrib_apply' hX hY _ _ ht hs, Measure.map_apply hX hs,
-      cond_apply _ (hY (.singleton _))]
+      cond_apply (hY (.singleton _))]
 
 variable [Countable T] [Nonempty T] [Nonempty S] [MeasurableSingletonClass S] [Countable S]
   [Countable U] [MeasurableSingletonClass U]
@@ -472,13 +472,13 @@ lemma condEntropy_prod_eq_sum {X : Ω → S} {Y : Ω → T} {Z : Ω → T'} [Mea
   have A : (fun a ↦ (Y a, Z a)) ⁻¹' {(x, y)} = Z ⁻¹' {y} ∩ Y ⁻¹' {x} := by
     ext p; simp [and_comm]
   congr 2
-  · rw [cond_apply _ (hZ (.singleton y)), ← mul_assoc, A]
+  · rw [cond_apply (hZ (.singleton y)), ← mul_assoc, A]
     rcases eq_or_ne (μ (Z ⁻¹' {y})) 0 with hy|hy
     · have : μ (Z ⁻¹' {y} ∩ Y ⁻¹' {x}) = 0 :=
         le_antisymm ((measure_mono Set.inter_subset_left).trans hy.le) bot_le
       simp [this, hy]
     · rw [ENNReal.mul_inv_cancel hy (by finiteness), one_mul]
-  · rw [A, cond_cond_eq_cond_inter _ (hZ (.singleton y)) (hY (.singleton x))]
+  · rw [A, cond_cond_eq_cond_inter (hZ (.singleton y)) (hY (.singleton x))]
 
 variable [MeasurableSingletonClass S]
 
@@ -513,7 +513,7 @@ lemma condEntropy_of_injective
     intro y
     refine entropy_congr ?_
     have : ∀ᵐ ω ∂μ[|Y ← y], Y ω = y := by
-      rw [ae_iff, cond_apply _ (hY (.singleton _))]
+      rw [ae_iff, cond_apply (hY (.singleton _))]
       have : {a | ¬Y a = y} = (Y ⁻¹' {y})ᶜ := by ext; simp
       rw [this, Set.inter_compl_self, measure_empty, mul_zero]
     filter_upwards [this] with ω hω
@@ -958,7 +958,7 @@ lemma condEntropy_prod_eq_of_indepFun [Fintype T] [Fintype U] [IsZeroOrProbabili
   rcases eq_or_ne (μ (Z ⁻¹' {w})) 0 with hw|hw
   · simp [hw]
   congr 1
-  have : IsProbabilityMeasure (μ[|Z ⁻¹' {w}]) := cond_isProbabilityMeasure μ hw
+  have : IsProbabilityMeasure (μ[|Z ⁻¹' {w}]) := cond_isProbabilityMeasure hw
   apply IdentDistrib.condEntropy_eq hX hY hX hY
   exact (h.identDistrib_cond (MeasurableSet.singleton w) (hX.prod_mk hY) hZ hw).symm
 
@@ -986,7 +986,7 @@ lemma condMutualInfo_eq_zero (hX : Measurable X) (hY : Measurable Y)
     rw [Pi.le_def]
     intro z; simp
     by_cases hz : μ (Z ⁻¹' {z}) = 0
-    · have : μ[| Z ⁻¹' {z}] = 0 := cond_eq_zero_of_meas_eq_zero _ hz
+    · have : μ[| Z ⁻¹' {z}] = 0 := cond_eq_zero_of_meas_eq_zero hz
       simp [this]
       rw [mutualInfo_def]
       simp

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -1,4 +1,4 @@
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import PFR.ForMathlib.Entropy.Measure
 import PFR.Mathlib.MeasureTheory.Integral.Bochner
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
@@ -266,8 +266,8 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
   rw [this, Finset.mul_sum, ← Finset.sum_add_distrib]
   congr with u
   have : ((κ ⊗ₖ η) t).real {(s, u)} = ((κ t).real {s}) * ((η (t, s)).real {u}) := by
-    rw [measureReal_def, compProd_apply κ η _ (.singleton _),
-      lintegral_eq_setLIntegral (hB t ht), setLIntegral_eq_sum, Finset.sum_eq_single_of_mem s hs]
+    rw [measureReal_def, compProd_apply (.singleton _), lintegral_eq_setLIntegral (hB t ht),
+      setLIntegral_eq_sum, Finset.sum_eq_single_of_mem s hs]
     · simp [measureReal_def]
     intro b _ hbs
     simp [hbs]

PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean

@@ -67,8 +67,8 @@ lemma compProd_assoc (ξ : Kernel T S) [IsSFiniteKernel ξ]
       = ξ ⊗ₖ (κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable)) := by
   ext x s hs
   rw [map_apply' _ (by fun_prop) _ hs,
-    compProd_apply _ _ _ (MeasurableEquiv.prodAssoc.measurable hs),
-    compProd_apply _ _ _ hs, lintegral_compProd]
+    compProd_apply (MeasurableEquiv.prodAssoc.measurable hs),
+    compProd_apply hs, lintegral_compProd]
   swap; · exact measurable_kernel_prod_mk_left' (MeasurableEquiv.prodAssoc.measurable hs) _
   congr with a
   rw [compProd_apply]
@@ -86,7 +86,7 @@ lemma Measure.compProd_compProd (μ : Measure T)
     Measure.lintegral_compProd]
   swap; · exact measurable_kernel_prod_mk_left (MeasurableEquiv.prodAssoc.measurable hs)
   congr with a
-  rw [compProd_apply _ _ _ (measurable_prod_mk_left hs)]
+  rw [compProd_apply (measurable_prod_mk_left hs)]
   congr
 
 lemma Measure.compProd_compProd' (μ : Measure T)

PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean

@@ -1,4 +1,3 @@
-import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
 import PFR.ForMathlib.Entropy.Kernel.Group
 
 /-!

PFR/ForMathlib/Entropy/Measure.lean

@@ -1,10 +1,10 @@
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.Tactic.Finiteness
 import Mathlib.Tactic.Positivity.Finset
+import PFR.Mathlib.MeasureTheory.Measure.Prod
 import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.MeasureReal
-import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
-import PFR.Tactic.Finiteness
 
 /-!
 # Entropy of a measure