bump mathlib (#238)

In leanprover-community/mathlib4#22644, I've removed useless explicit arguments in `iIndepFun`, motivated by PFR where this was just cluttering things. In this PR for PFR, I do the corresponding cleanup.

Author: sgouezel

PFR/BoundingMutual.lean

@@ -25,8 +25,12 @@ $$ {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m}
  $$
  Then ${\mathcal I} \leq 4 m^2 \eta k.$
 -/
-lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → G) (h_indep:
-  iIndepFun (fun _ ↦ by infer_instance) X)
-  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω'] (X': Fin p.m × Fin p.m → Ω' → G) (h_indep': iIndepFun (fun _ ↦ by infer_instance) X') (hperm:
-  ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω) ) (fun ω ↦ (fun i ↦ X (e i) ω))) :
-  I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) | fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 4 * p.m^2 * p.η * D[ X; (fun _ ↦ hΩ)] := sorry
+lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ]
+  (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → G)
+  (h_indep : iIndepFun X)
+  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω']
+  (X' : Fin p.m × Fin p.m → Ω' → G) (h_indep': iIndepFun X')
+  (hperm : ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω))
+    (fun ω ↦ (fun i ↦ X (e i) ω))) :
+  I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) |
+    fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 4 * p.m^2 * p.η * D[ X; (fun _ ↦ hΩ)] := sorry

PFR/Endgame.lean

@@ -45,7 +45,7 @@ variable (X₁ X₂ X₁' X₂' : Ω → G)
 
 variable (h₁ : IdentDistrib X₁ X₁') (h₂ : IdentDistrib X₂ X₂')
 
-variable (h_indep : iIndepFun (fun _i => hG) ![X₁, X₂, X₁', X₂'])
+variable (h_indep : iIndepFun ![X₁, X₂, X₁', X₂'])
 
 variable (h_min : tau_minimizes p X₁ X₂)
 
@@ -81,7 +81,7 @@ private lemma hmeas2 {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSp
 include h_indep hX₁ hX₂ hX₁' hX₂' h₁ in
 /-- The quantity `I_3 = I[V:W|S]` is equal to `I_2`. -/
 lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ := by
-  have h_indep2 : iIndepFun (fun _ ↦ hG) ![X₁', X₂, X₁, X₂'] := by
+  have h_indep2 : iIndepFun ![X₁', X₂, X₁, X₂'] := by
     exact h_indep.reindex_four_cbad
   have hident : IdentDistrib (fun a (i : Fin 4) => ![X₁, X₂, X₁', X₂'] i a)
     (fun a (j : Fin 4) => ![X₁', X₂, X₁, X₂'] j a) := by
@@ -160,7 +160,7 @@ lemma hU [IsProbabilityMeasure (ℙ : Measure Ω)] : H[U] = H[X₁' + X₂'] :=
 variable {X₁ X₂ X₁' X₂'} in
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 lemma independenceCondition1 :
-    iIndepFun (fun _ ↦ hG) ![X₁, X₂, X₁' + X₂'] :=
+    iIndepFun ![X₁, X₂, X₁' + X₂'] :=
   h_indep.apply_two_last hX₁ hX₂ hX₁' hX₂' measurable_add
 
 include h₁ h₂ h_indep in
@@ -172,31 +172,31 @@ lemma hV [IsProbabilityMeasure (ℙ : Measure Ω)] : H[V] = H[X₁ + X₂'] :=
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
 lemma independenceCondition2 :
-    iIndepFun (fun _ ↦ hG) ![X₂, X₁, X₁' + X₂'] :=
+    iIndepFun ![X₂, X₁, X₁' + X₂'] :=
   independenceCondition1 hX₂ hX₁ hX₁' hX₂' h_indep.reindex_four_bacd
 
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
 lemma independenceCondition3 :
-    iIndepFun (fun _ ↦ hG) ![X₁', X₂, X₁ + X₂'] :=
+    iIndepFun ![X₁', X₂, X₁ + X₂'] :=
   independenceCondition1 hX₁' hX₂ hX₁ hX₂' h_indep.reindex_four_cbad
 
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
 lemma independenceCondition4 :
-    iIndepFun (fun _ ↦ hG) ![X₂, X₁', X₁ + X₂'] :=
+    iIndepFun ![X₂, X₁', X₁ + X₂'] :=
   independenceCondition1 hX₂ hX₁' hX₁ hX₂' h_indep.reindex_four_bcad
 
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
 lemma independenceCondition5 :
-    iIndepFun (fun _ ↦ hG) ![X₁, X₁', X₂ + X₂'] :=
+    iIndepFun ![X₁, X₁', X₂ + X₂'] :=
   independenceCondition1 hX₁ hX₁' hX₂ hX₂' h_indep.reindex_four_acbd
 
 include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
 lemma independenceCondition6 :
-    iIndepFun (fun _ ↦ hG) ![X₂, X₂', X₁' + X₁] :=
+    iIndepFun ![X₂, X₂', X₁' + X₁] :=
   independenceCondition1 hX₂ hX₂' hX₁' hX₁ h_indep.reindex_four_bdca
 
 set_option maxHeartbeats 400000 in
@@ -303,7 +303,7 @@ lemma sum_dist_diff_le [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2
         add_le_add (add_le_add step₁ step₂) step₃
     _ = 3 * H[S ; ℙ] - 3/2 * H[X₁ ; ℙ] -3/2 * H[X₂ ; ℙ] := by ring
 
-  have h_indep' : iIndepFun (fun _i => hG) ![X₁, X₂, X₂', X₁'] := by
+  have h_indep' : iIndepFun ![X₁, X₂, X₂', X₁'] := by
     refine .of_precomp (Equiv.swap (2 : Fin 4) 3).surjective ?_
     convert h_indep using 1
     ext x
@@ -500,7 +500,7 @@ theorem tau_strictly_decreases_aux
     (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
+  have h_indep' : iIndepFun ![X₁, X₂, X₂', X₁'] := by
     let σ : Fin 4 ≃ Fin 4 :=
     { toFun := ![0, 1, 3, 2]
       invFun := ![0, 1, 3, 2]

PFR/Examples.lean

@@ -173,7 +173,7 @@ example (h1 : IdentDistrib X X') (h2 : IdentDistrib Y Y') : d[X # Y] = d[X' # Y'
 example : d[X # Z] ≤ d[X # Y] + d[Y # Z] := rdist_triangle hX hY hZ
 
 /-- The Kaimanovich-Vershik-Madiman inequality -/
-example (h : iIndepFun (fun _ ↦ hG) ![X, Y, Z]) : H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y] :=
+example (h : iIndepFun ![X, Y, Z]) : H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y] :=
   kaimanovich_vershik h hX hY hZ
 
 /-- The entropic Balog--Szemeredi--Gowers inequality -/

PFR/Fibring.lean

@@ -87,7 +87,7 @@ variable {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G]
 variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
 
 /-- The conditional Ruzsa Distance step of `sum_of_rdist_eq` -/
-lemma sum_of_rdist_eq_step_condRuzsaDist {Y : Fin 4 → Ω → G} (h_indep : iIndepFun (fun _ : Fin 4 ↦ hG) Y μ)
+lemma sum_of_rdist_eq_step_condRuzsaDist {Y : Fin 4 → Ω → G} (h_indep : iIndepFun Y μ)
   (h_meas : ∀ i, Measurable (Y i)) :
     d[⟨Y 0, Y 2⟩ | Y 0 - Y 2 ; μ # ⟨Y 1, Y 3⟩ | Y 1 - Y 3 ; μ] = d[Y 0 | Y 0 - Y 2 ; μ # Y 1 | Y 1 - Y 3 ; μ] := by
   let Y' : Fin 4 → Ω → G
@@ -149,7 +149,7 @@ lemma sum_of_rdist_eq_step_condMutualInfo {Y : Fin 4 → Ω → G}
 $$d[Y_1-Y_3; Y_2-Y_4] + d[Y_1|Y_1-Y_3; Y_2|Y_2-Y_4] $$
 $$ + I[Y_1-Y_2 : Y_2 - Y_4 | Y_1-Y_2-Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$
 -/
-lemma sum_of_rdist_eq (Y : Fin 4 → Ω → G) (h_indep : iIndepFun (fun _ : Fin 4 ↦ hG) Y μ)
+lemma sum_of_rdist_eq (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)
   (h_meas : ∀ i, Measurable (Y i)) :
     d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]
       = d[(Y 0) - (Y 2); μ # (Y 1) - (Y 3); μ]
@@ -187,7 +187,7 @@ $$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$
 $$ + I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$
 -/
 lemma sum_of_rdist_eq_char_2
-  [Module (ZMod 2) G] (Y : Fin 4 → Ω → G) (h_indep : iIndepFun (fun _ : Fin 4 ↦ hG) Y μ)
+  [Module (ZMod 2) G] (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)
   (h_meas : ∀ i, Measurable (Y i)) :
     d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]
       = d[(Y 0) + (Y 2); μ # (Y 1) + (Y 3); μ]
@@ -196,7 +196,7 @@ lemma sum_of_rdist_eq_char_2
   simpa [ZModModule.sub_eq_add] using sum_of_rdist_eq Y h_indep h_meas
 
 lemma sum_of_rdist_eq_char_2' [Module (ZMod 2) G] (X Y X' Y' : Ω → G)
-  (h_indep : iIndepFun (fun _ : Fin 4 ↦ hG) ![X, Y, X', Y'] μ)
+  (h_indep : iIndepFun ![X, Y, X', Y'] μ)
   (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hY' : Measurable Y') :
   d[X ; μ # Y ; μ] + d[X' ; μ # Y' ; μ]
     = d[X + X' ; μ # Y + Y' ; μ] + d[X | X + X' ; μ # Y | Y + Y' ; μ]

PFR/FirstEstimate.lean

@@ -34,7 +34,7 @@ variable (X₁ X₂ X₁' X₂' : Ω → G)
   (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂')
 
 variable (h₁ : IdentDistrib X₁ X₁') (h₂ : IdentDistrib X₂ X₂')
-variable (h_indep : iIndepFun (fun _i => hG) ![X₁, X₂, X₂', X₁'])
+variable (h_indep : iIndepFun ![X₁, X₂, X₂', X₁'])
 variable (h_min : tau_minimizes p X₁ X₂)
 
 /-- `k := d[X₁ # X₂]`, the Ruzsa distance `rdist` between X₁ and X₂. -/

PFR/ForMathlib/Entropy/Group.lean

@@ -243,7 +243,7 @@ lemma max_entropy_le_entropy_div (hX : Measurable X) (hY : Measurable Y) (h : In
 lemma max_entropy_le_entropy_prod {G : Type*} [Countable G] [hG : MeasurableSpace G]
     [MeasurableSingletonClass G] [CommGroup G] [MeasurableMul₂ G]
     {I : Type*} {s : Finset I} {i₀ : I} (hi₀ : i₀ ∈ s) {X : I → Ω → G} [∀ i, FiniteRange (X i)]
-    (hX : (i : I) → Measurable (X i)) (h_indep : iIndepFun (fun (_ : I) => hG) X μ) :
+    (hX : (i : I) → Measurable (X i)) (h_indep : iIndepFun X μ) :
     H[X i₀ ; μ] ≤ H[∏ i ∈ s, X i ; μ] := by
   have hs : s.Nonempty := ⟨i₀, hi₀⟩
   induction' hs using Finset.Nonempty.cons_induction with i j s Hnot _ Hind

PFR/ForMathlib/Entropy/RuzsaDist.lean

@@ -172,7 +172,7 @@ lemma ProbabilityTheory.IndepFun.rdist_eq [IsFiniteMeasure μ]
 /-- `d[X ; Y] ≤ H[X]/2 + H[Y]/2`. -/
 lemma rdist_le_avg_ent {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)
     (hY : Measurable Y) (μ : Measure Ω := by volume_tac) (μ' : Measure Ω' := by volume_tac)
-  [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
+    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
     d[X ; μ # Y ; μ'] ≤ (H[X ; μ] + H[Y ; μ'])/2 := by
   rcases ProbabilityTheory.independent_copies_finiteRange hX hY μ μ'
     with ⟨ν, X', Y', hprob, hX', hY', h_indep, hidentX, hidentY, hfinX, hfinY⟩
@@ -186,7 +186,7 @@ lemma rdist_le_avg_ent {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRan
 /-- Applying an injective homomorphism does not affect Ruzsa distance. -/
 lemma rdist_of_inj {H : Type*} [hH : MeasurableSpace H] [MeasurableSingletonClass H]
   [AddCommGroup H] [Countable H] (hX : Measurable X) (hY : Measurable Y)
-  (φ : G →+ H) (hφ : Injective φ) [IsProbabilityMeasure μ] [IsProbabilityMeasure μ' ]:
+  (φ : G →+ H) (hφ : Injective φ) [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
     d[φ ∘ X ; μ # φ ∘ Y ; μ'] = d[X ; μ # Y ; μ'] := by
     rw [rdist_def, rdist_def]
     congr 2
@@ -1109,7 +1109,7 @@ lemma condRuzsaDist'_of_inj_map' [Module (ZMod 2) G] [IsProbabilityMeasure μ]
   simp [μ']
 
 /-- The **Kaimanovich-Vershik inequality**. `H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y]`. -/
-lemma kaimanovich_vershik {X Y Z : Ω → G} (h : iIndepFun (fun _ ↦ hG) ![X, Y, Z] μ)
+lemma kaimanovich_vershik {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
     [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
     H[X + Y + Z ; μ] - H[X + Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by
@@ -1141,7 +1141,7 @@ lemma kaimanovich_vershik {X Y Z : Ω → G} (h : iIndepFun (fun _ ↦ hG) ![X,
     exact h.indepFun_add_right this 2 0 1 (by decide) (by decide)
 
 /-- A version of the **Kaimanovich-Vershik inequality** with some variables negated. -/
-lemma kaimanovich_vershik' {X Y Z : Ω → G} (h : iIndepFun (fun _ ↦ hG) ![X, Y, Z] μ)
+lemma kaimanovich_vershik' {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
     [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
     H[X - (Y + Z) ; μ] - H[X - Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by
@@ -1429,7 +1429,7 @@ variable (μ) in
 lemma condRuzsaDist_diff_ofsum_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
     {X : Ω → G} {Y Z Z' : Ω' → G}
     (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hZ' : Measurable Z')
-    (h : iIndepFun (fun _ ↦ hG) ![Y, Z, Z'] μ')
+    (h : iIndepFun ![Y, Z, Z'] μ')
     [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange Z'] :
     d[X ; μ # Y + Z | Y + Z + Z'; μ'] - d[X ; μ # Y; μ'] ≤
     (H[Y + Z + Z'; μ'] + H[Y + Z; μ'] - H[Y ; μ'] - H[Z' ; μ'])/2 := by

PFR/ForMathlib/FiniteRange/IdentDistrib.lean

@@ -84,7 +84,7 @@ lemma independent_copies3_nondep_finiteRange {α : Type u}
     ∃ (A : Type (max u_1 u_2 u_3)) (_ : MeasurableSpace A) (μA : Measure A)
       (X₁' X₂' X₃' : A → α),
     IsProbabilityMeasure μA ∧
-    iIndepFun (fun _ ↦ mS) ![X₁', X₂', X₃'] μA ∧
+    iIndepFun ![X₁', X₂', X₃'] μA ∧
       Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧
       IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ ∧
       FiniteRange X₁' ∧ FiniteRange X₂' ∧ FiniteRange X₃' := by
@@ -121,7 +121,7 @@ lemma independent_copies4_nondep_finiteRange {α : Type u}
     ∃ (A : Type (max u_1 u_2 u_3 u_4)) (_ : MeasurableSpace A) (μA : Measure A)
       (X₁' X₂' X₃' X₄' : A → α),
     IsProbabilityMeasure μA ∧
-    iIndepFun (fun _ ↦ mS) ![X₁', X₂', X₃', X₄'] μA ∧
+    iIndepFun ![X₁', X₂', X₃', X₄'] μA ∧
       Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧ Measurable X₄'
       ∧ IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃
       ∧ IdentDistrib X₄' X₄ μA μ₄ ∧ FiniteRange X₁' ∧ FiniteRange X₂'