Bump mathlib

PFR.lean

@@ -29,22 +29,14 @@ import PFR.Kullback
 import PFR.Main
 import PFR.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
-import PFR.Mathlib.Data.Finsupp.Defs
-import PFR.Mathlib.Data.Set.Function
 import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Mathlib.Data.Set.Pointwise.SMul
-import PFR.Mathlib.GroupTheory.Torsion
 import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
 import PFR.Mathlib.MeasureTheory.Constructions.Pi
 import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
-import PFR.Mathlib.MeasureTheory.Group.Arithmetic
 import PFR.Mathlib.MeasureTheory.Integral.Bochner
 import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
-import PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic
-import PFR.Mathlib.MeasureTheory.MeasurableSpace.Defs
-import PFR.Mathlib.MeasureTheory.MeasurableSpace.Embedding
-import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
 import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
 import PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import PFR.Mathlib.MeasureTheory.Measure.Typeclasses

PFR/Endgame.lean

@@ -118,7 +118,7 @@ lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ :=
   have hU : Measurable U := Measurable.add hX₁ hX₂
   have hV : Measurable V := Measurable.add hX₁' hX₂
   have hW : Measurable W := Measurable.add hX₁' hX₁
-  have hS : Measurable S := by measurability
+  have hS : Measurable S := by fun_prop
   rw [condMutualInfo_eq hV hW hS, condMutualInfo_eq hU hW hS, chain_rule'' ℙ hU hS,
     chain_rule'' ℙ hV hS, chain_rule'' ℙ hW hS, chain_rule'' ℙ _ hS, chain_rule'' ℙ _ hS,
     IdentDistrib.entropy_eq hUVS, IdentDistrib.entropy_eq hUVWS]
@@ -133,10 +133,7 @@ include h_indep hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_min in
 lemma sum_condMutual_le [ElementaryAddCommGroup G 2] [IsProbabilityMeasure (ℙ : Measure Ω)] :
     I[U : V | S] + I[V : W | S] + I[W : U | S]
       ≤ 6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁) := by
-  have : I[W:U|S] = I₂ := by
-    rw [condMutualInfo_comm]
-    · exact Measurable.add' hX₁' hX₁
-    · exact Measurable.add' hX₁ hX₂
+  have : I[W : U | S] = I₂ := condMutualInfo_comm (by fun_prop) (by fun_prop) ..
   rw [I₃_eq, this]
   have h₂ := second_estimate p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min
   have h := add_le_add (add_le_add_left h₂ I₁) h₂
@@ -338,9 +335,9 @@ omit [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ
 lemma cond_c_eq_integral [IsProbabilityMeasure (ℙ : Measure Ω')]
     {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable Z) : c[Y | Z # Y | Z] =
     (Measure.map Z ℙ)[fun z => c[Y ; ℙ[|Z ← z] # Y ; ℙ[|Z ← z]]] := by
-  simp only [integral_eq_sum, smul_sub, smul_add, smul_sub, Finset.sum_sub_distrib,
+  simp only [integral_fintype _ .of_finite, smul_sub, smul_add, smul_sub, Finset.sum_sub_distrib,
     Finset.sum_add_distrib]
-  simp_rw [← integral_eq_sum]
+  simp_rw [← integral_fintype _ .of_finite]
   rw [← condRuzsaDist'_eq_integral _ hY hZ, ← condRuzsaDist'_eq_integral _ hY hZ, integral_const,
     integral_const]
   have : IsProbabilityMeasure (Measure.map Z ℙ) := isProbabilityMeasure_map hZ.aemeasurable
@@ -393,32 +390,32 @@ lemma construct_good_prelim :
 
   have h2 : p.η * sum2 ≤ p.η * (d[p.X₀₁ # T₁] - d[p.X₀₁ # X₁] + I[T₁ : T₃] / 2) := by
     have : sum2 = d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁] := by
-      simp only [integral_sub (.of_finite _ _) (.of_finite _ _), integral_const, measure_univ,
+      simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
         ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum2]
       simp_rw [condRuzsaDist'_eq_sum hT₁ hT₃,
         integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum,
-        Measure.map_apply hT₃ (measurableSet_singleton _), smul_eq_mul]
+        Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
 
     gcongr
     linarith [condRuzsaDist_le' ℙ ℙ p.hmeas1 hT₁ hT₃]
 
   have h3 : p.η * sum3 ≤ p.η * (d[p.X₀₂ # T₂] - d[p.X₀₂ # X₂] + I[T₂ : T₃] / 2) := by
     have : sum3 = d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂] := by
-      simp only [integral_sub (.of_finite _ _) (.of_finite _ _), integral_const, measure_univ,
+      simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
         ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum3]
       simp_rw [condRuzsaDist'_eq_sum hT₂ hT₃,
         integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum,
-        Measure.map_apply hT₃ (measurableSet_singleton _), smul_eq_mul]
+        Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
     gcongr
     linarith [condRuzsaDist_le' ℙ ℙ p.hmeas2 hT₂ hT₃]
 
   have h4 : sum4 ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁ : T₃] + I[T₂ : T₃]) / 2 := by
     suffices sum4 = sum1 + p.η * (sum2 + sum3) by linarith
-    simp only [sum4, integral_add (.of_finite _ _) (.of_finite _ _), integral_mul_left]
+    simp only [sum4, integral_add .of_finite .of_finite, integral_mul_left]
 
   have hk : k ≤ sum4 := by
     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 ↦ ?_
+    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)
     dsimp only
@@ -469,10 +466,10 @@ lemma cond_construct_good [IsProbabilityMeasure (ℙ : Measure Ω)] :
     k ≤ δ' + (p.η/3) * (δ' + c[T₁ | R # T₁ | R] + c[T₂ | R # T₂ | R] + c[T₃ | R # T₃ | R]) := by
   rw [delta'_eq_integral, cond_c_eq_integral _ _ _ hT₁ hR, cond_c_eq_integral _ _ _ hT₂ hR,
     cond_c_eq_integral _ _ _ hT₃ hR]
-  simp_rw [integral_eq_sum, ← Finset.sum_add_distrib, ← smul_add, Finset.mul_sum, mul_smul_comm,
+  simp_rw [integral_fintype _ .of_finite, ← Finset.sum_add_distrib, ← smul_add, Finset.mul_sum, mul_smul_comm,
     ← Finset.sum_add_distrib, ← smul_add]
-  simp_rw [← integral_eq_sum]
-  have : IsProbabilityMeasure (Measure.map R ℙ) := isProbabilityMeasure_map (by measurability)
+  simp_rw [← integral_fintype _ .of_finite]
+  have : IsProbabilityMeasure (Measure.map R ℙ) := isProbabilityMeasure_map (by fun_prop)
   calc
     k = (Measure.map R ℙ)[fun _r => k] := by
       rw [integral_const]; simp
@@ -499,8 +496,8 @@ theorem tau_strictly_decreases_aux
     [IsProbabilityMeasure (ℙ : Measure Ω)] [ElementaryAddCommGroup G 2]
     (hpη : p.η = 1/9) : d[X₁ # X₂] = 0 := by
   have h0 := cond_construct_good p X₁ X₂ hX₁ hX₂ h_min (sum_uvw_eq_zero ..)
-    (show Measurable U by measurability) (show Measurable V by measurability)
-    (show Measurable W by measurability) (show Measurable S by measurability)
+    (show Measurable U by fun_prop) (show Measurable V by fun_prop)
+    (show Measurable W by fun_prop) (show Measurable S by fun_prop)
   have h1 := sum_condMutual_le p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min
   have h2 := sum_dist_diff_le p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min
   have h_indep' : iIndepFun (fun _i => hG) ![X₁, X₂, X₂', X₁'] := by

PFR/Fibring.lean

@@ -35,15 +35,15 @@ $$I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ).$$
 lemma rdist_of_indep_eq_sum_fibre {Z_1 Z_2 : Ω → H} (h : IndepFun Z_1 Z_2 μ)
     (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2]:
     d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ] + I[Z_1-Z_2 : ⟨π∘Z_1, π∘Z_2⟩ | π∘(Z_1 - Z_2); μ] := by
-  have hπ : Measurable π := measurable_of_countable _
+  have hπ : Measurable π := .of_discrete
   have step1 : d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] +
       H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] - H[Z_1 | π ∘ Z_1; μ] / 2 - H[Z_2 | π ∘ Z_2; μ] / 2 := by
-    have hsub : H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] = H[(Z_1 - Z_2); μ] - H[π ∘ (Z_1 - Z_2); μ] := condEntropy_comp_self (by measurability) hπ
-
+    have hsub : H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] = H[(Z_1 - Z_2); μ] - H[π ∘ (Z_1 - Z_2); μ] :=
+      condEntropy_comp_self (by fun_prop) hπ
     rw [h.rdist_eq h1 h2, (h.comp hπ hπ).rdist_eq (hπ.comp h1) (hπ.comp h2),
       condEntropy_comp_self h1 hπ, condEntropy_comp_self h2 hπ, hsub, map_comp_sub π]
     ring_nf
-  have m0 : Measurable (fun x ↦ (x, π x)) := measurable_of_countable _
+  have m0 : Measurable (fun x ↦ (x, π x)) := .of_discrete
   have h' : IndepFun (⟨Z_1, π ∘ Z_1⟩) (⟨Z_2, π ∘ Z_2⟩) μ := h.comp m0 m0
   have m1 : Measurable (Z_1 - Z_2) := h1.sub h2
   have m2 : Measurable (⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩) := (hπ.comp h1).prod_mk (hπ.comp h2)
@@ -63,23 +63,22 @@ lemma rdist_le_sum_fibre {Z_1 : Ω → H} {Z_2 : Ω' → H}
   (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
   d[π ∘ Z_1; μ # π ∘ Z_2; μ'] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ']:= by
   obtain ⟨ν, W_1, W_2, hν, m1, m2, hi, hi1, hi2, _, _⟩ := ProbabilityTheory.independent_copies_finiteRange h1 h2 μ μ'
-  have hπ : Measurable π := measurable_of_countable _
-  have hφ : Measurable (fun x ↦ (x, π x)) := measurable_of_countable _
+  have hπ : Measurable π := .of_discrete
+  have hφ : Measurable (fun x ↦ (x, π x)) := .of_discrete
   have hπ1 : IdentDistrib (⟨Z_1, π ∘ Z_1⟩) (⟨W_1, π ∘ W_1⟩) μ ν := hi1.symm.comp hφ
   have hπ2 : IdentDistrib (⟨Z_2, π ∘ Z_2⟩) (⟨W_2, π ∘ W_2⟩) μ' ν := hi2.symm.comp hφ
   rw [← hi1.rdist_eq hi2, ← (hi1.comp hπ).rdist_eq (hi2.comp hπ),
     rdist_of_indep_eq_sum_fibre π hi m1 m2,
     condRuzsaDist_of_copy h1 (hπ.comp h1) h2 (hπ.comp h2) m1 (hπ.comp m1) m2 (hπ.comp m2) hπ1 hπ2]
-  exact le_add_of_nonneg_right (condMutualInfo_nonneg (by measurability) ((hπ.comp m1).prod_mk (hπ.comp m2)) _ _)
+  exact le_add_of_nonneg_right (condMutualInfo_nonneg (by fun_prop) (by fun_prop))
 
 /-- \[d[X;Y]\geq d[\pi(X);\pi(Y)].\] -/
 lemma rdist_of_hom_le {Z_1 : Ω → H} {Z_2 : Ω' → H}
     (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
     d[π ∘ Z_1; μ # π ∘ Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ'] := by
   apply le_trans _ (rdist_le_sum_fibre π h1 h2 (μ := μ) (μ' := μ'))
   rw [le_add_iff_nonneg_right]
-  exact condRuzsaDist_nonneg h1 ((measurable_of_countable π).comp h1) h2
-    ((measurable_of_countable π).comp h2)
+  exact condRuzsaDist_nonneg h1 (by fun_prop) h2 (by fun_prop)
 
 end GeneralFibring
 
@@ -97,7 +96,7 @@ lemma sum_of_rdist_eq_step_condRuzsaDist {Y : Fin 4 → Ω → G} (h_indep : iIn
     | 2 => Y 0 - Y 2
     | 3 => Y 1 - Y 3
   let f : (G × G) → (G × G) := fun (g, h) ↦ (g, g - h)
-  have hf : Measurable f := measurable_of_countable _
+  have hf : Measurable f := .of_discrete
   have h_indep' : IndepFun (⟨Y' 0, Y' 2⟩) (⟨Y' 1, Y' 3⟩) μ :=
     (h_indep.indepFun_prod_mk_prod_mk h_meas 0 2 1 3
       (by decide) (by decide) (by decide) (by decide)).comp hf hf
@@ -121,10 +120,7 @@ lemma sum_of_rdist_eq_step_condMutualInfo {Y : Fin 4 → Ω → G}
     I[Y 0 - Y 1 : Y 1 - Y 3|Y 0 - Y 1 - (Y 2 - Y 3) ; μ] by convert this using 2; abel
   symm
   have hm (f : G → G → G × G) {a b i j k l : Fin 4} :
-    Measurable (uncurry f ∘ ⟨Y i - Y j - (Y k - Y l), Y a - Y b⟩) :=
-    (measurable_of_countable (uncurry f)).comp
-    ((((h_meas _).sub (h_meas _)).sub ((h_meas _).sub (h_meas _))).prod_mk
-    ((h_meas _).sub (h_meas _)))
+    Measurable (uncurry f ∘ ⟨Y i - Y j - (Y k - Y l), Y a - Y b⟩) := by fun_prop
   have hmf : Measurable fun ω ↦ ((Y 0 - Y 1) ω, (Y 0 - Y 1) ω - (Y 0 - Y 1 - (Y 2 - Y 3)) ω) :=
     hm (fun z x ↦ (x, x - z))
   have hmg : Measurable fun ω ↦ ((Y 1 - Y 3) ω + (Y 0 - Y 1 - (Y 2 - Y 3)) ω, (Y 1 - Y 3) ω) :=

PFR/FirstEstimate.lean

@@ -85,7 +85,7 @@ lemma condRuzsaDist_of_sums_ge :
     d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] ≥
       k - p.η * (d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁])
         - p.η * (d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂]) :=
-  condRuzsaDistance_ge_of_min _ h_min hX₁ hX₂ _ _ (by measurability) (by measurability)
+  condRuzsaDistance_ge_of_min _ h_min hX₁ hX₂ _ _ (by fun_prop) (by fun_prop)
 
 variable [ElementaryAddCommGroup G 2]
 
@@ -135,7 +135,7 @@ lemma first_estimate
     I₁ ≤ 2 * p.η * k := by
   have v1 := rdist_add_rdist_add_condMutual_eq X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_› ‹_› ‹_›
   have v2 := rdist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_› ‹_›
-  have v3 := condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› (by measurability) (by measurability)
+  have v3 := condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› (by fun_prop) (by aesop)
   have v4 := (mul_le_mul_left p.hη).2 (diff_rdist_le_1 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
   have v5 := (mul_le_mul_left p.hη).2 (diff_rdist_le_2 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
   have v6 := (mul_le_mul_left p.hη).2 (diff_rdist_le_3 p X₁ X₂ X₁' X₂' ‹_› ‹_› ‹_› ‹_›)
@@ -159,7 +159,7 @@ lemma ent_ofsum_le
   have lem68 : D + Dcc + I₁ = 2 * k :=
     rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep
   have lem610 : Dcc ≥ k - p.η * (Dc1 - D1) - p.η * (Dc2 - D2) :=
-    condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' hX₁ hX₂ (by measurability) (by measurability) h_min
+    condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' hX₁ hX₂ (by fun_prop) (by aesop) h_min
   have lem611c : Dc1 - D1 ≤ k / 2 + H[X₁] / 4 - H[X₂] / 4 :=
     diff_rdist_le_3 p X₁ X₂ X₁' X₂' hX₁ hX₂' h₂ h_indep
   have lem611d : Dc2 - D2 ≤ k / 2 + H[X₂] / 4 - H[X₁] / 4 :=
@@ -179,7 +179,7 @@ lemma ent_ofsum_le
     exact iIndepFun.indepFun_add_add h_indep (fun i ↦ by fin_cases i <;> assumption) 0 2 1 3
       (by decide) (by decide) (by decide) (by decide)
   have ind : D = H[X₁ + X₂' - (X₂ + X₁')] - H[X₁ + X₂'] / 2 - H[X₂ + X₁'] / 2 :=
-    ind_aux.rdist_eq (by measurability) (by measurability)
+    ind_aux.rdist_eq (by fun_prop) (by fun_prop)
   rw [ind, ent_sub_eq_ent_add, rw₁] at aux
   have obs : H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁ := by
     linarith