Bump Lean to 4.11.0rc2

PFR.lean

@@ -27,7 +27,7 @@ import PFR.HomPFR
 import PFR.HundredPercent
 import PFR.ImprovedPFR
 import PFR.Main
-import PFR.Mathlib.Algebra.Group.Subgroup.Pointwise
+import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
 import PFR.Mathlib.Data.Fin.VecNotation
 import PFR.Mathlib.Data.Set.Pointwise.SMul
 import PFR.Mathlib.GroupTheory.Torsion

PFR/ApproxHomPFR.lean

@@ -1,5 +1,5 @@
 import Mathlib.Combinatorics.Additive.Energy
-import Mathlib.Analysis.NormedSpace.PiLp
+import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Extras.BSG
 import PFR.HomPFR
@@ -19,7 +19,7 @@ is true for a positive proportion of x,y.
 -/
 
 open Finset
-open scoped BigOperators Classical Pointwise Combinatorics.Additive
+open scoped Classical Pointwise Combinatorics.Additive
 
 variable {G G' : Type*} [AddCommGroup G] [Fintype G] [AddCommGroup G'] [Fintype G']
   [ElementaryAddCommGroup G 2] [ElementaryAddCommGroup G' 2] (A : Finset G)
@@ -57,9 +57,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   obtain ⟨A', hA', hA'1, hA'2⟩ :=
     BSG_self' (sq_nonneg K) hA_nonempty (by simpa only [inv_mul_eq_div] using this)
   clear h_cs hf this
-  have hA'₀ : A'.Nonempty := Finset.card_pos.1 $ Nat.cast_pos.1 $ hA'1.trans_lt' $ by
-    have := hA_nonempty.card_pos; positivity
-
+  have hA'₀ : A'.Nonempty := Finset.card_pos.1 $ Nat.cast_pos.1 $ hA'1.trans_lt' $ by positivity
   let A'' := A'.toSet
   have hA''_coe : Nat.card A'' = Finset.card A' := Nat.card_eq_finsetCard A'
   have hA''_pos : 0 < Nat.card A'' := by rw [hA''_coe]; exact hA'₀.card_pos
@@ -119,7 +117,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     show c.2 + h + x'.2 = φ (c.1 + 0 + x'.1) + (-φ c.1 + c.2 + h)
     replace : φ x'.1 = x'.2 := (Set.mem_graph x').mp hx
     rw [map_add, map_add, map_zero, add_zero, this, add_comm (φ c.1), add_assoc x'.2,
-      ← add_assoc (φ c.1), ← add_assoc (φ c.1), add_neg_self, zero_add, add_comm]
+      ← add_assoc (φ c.1), ← add_assoc (φ c.1), ← sub_eq_add_neg, sub_self, zero_add, add_comm]
   have h_translate_card c h : Nat.card (translate c h) = Nat.card (Prod.fst '' translate c h) :=
     Nat.card_congr (Equiv.Set.imageOfInjOn Prod.fst (translate c h) <|
       Set.InjOn.mono (fun _ hx ↦ Set.Finite.subset_toFinset.mp hA' hx.1) (Set.fst_injOn_graph f))
@@ -195,7 +193,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   conv => { lhs; rhs; rw [← mul_assoc, ← mul_div_assoc, mul_comm_div, mul_div_assoc] }
   rw [div_self <| Nat.cast_ne_zero.mpr (Nat.ne_of_lt Nat.card_pos).symm, mul_one]
   push_cast
-  rw [mul_inv_cancel <| Nat.cast_ne_zero.mpr (Nat.ne_of_lt Nat.card_pos).symm, one_mul, ← sq,
+  rw [mul_inv_cancel₀ <| Nat.cast_ne_zero.mpr (Nat.ne_of_lt Nat.card_pos).symm, one_mul, ← sq,
     ← Real.rpow_two, ← Real.rpow_mul (by positivity), Real.mul_rpow (by positivity) (by positivity)]
   have : K ^ (12 : ℕ) = K ^ (12 : ℝ) := (Real.rpow_natCast K 12).symm
   rw [this, ← Real.rpow_mul (by positivity)]

PFR/BoundingMutual.lean

@@ -13,7 +13,7 @@ import PFR.MultiTauFunctional
 -/
 
 universe u
-open MeasureTheory ProbabilityTheory BigOperators
+open MeasureTheory ProbabilityTheory
 
 -- Spelling here is *very* janky.  Feel free to respell
 /-- Suppose that $X_{i,j}$, $1 \leq i,j \leq m$, are jointly independent $G$-valued random variables, such that for each $j = 1,\dots,m$, the random variables $(X_{i,j})_{i = 1}^m$

PFR/Endgame.lean

@@ -30,18 +30,16 @@ Assumptions:
 -/
 
 open MeasureTheory ProbabilityTheory
-open scoped BigOperators
-
 
 variable {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G]
-  [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ G]
+  [MeasurableSingletonClass G]
 
 variable {Ω₀₁ Ω₀₂ : Type*} [MeasureSpace Ω₀₁] [MeasureSpace Ω₀₂]
   [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)]
 
 variable (p : refPackage Ω₀₁ Ω₀₂ G)
 
-variable {Ω : Type*} [mΩ : MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
+variable {Ω : Type*} [mΩ : MeasureSpace Ω]
 
 variable (X₁ X₂ X₁' X₂' : Ω → G)
   (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂')
@@ -76,20 +74,14 @@ given the quadruple sum `S = X₁ + X₂ + X₁' + X₂'`. -/
 local notation3 "I₂" => I[U : W | S]
 
 --(Mantas) this times out in the proof below
-private lemma hmeas2 :
+private lemma hmeas2 {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G]
+    [MeasurableSingletonClass G] :
     Measurable fun p : Fin 4 → G => ((p 0 + p 1, p 0 + p 2), p 0 + p 1 + p 2 + p 3) := by
-  apply Measurable.prod
-  · apply Measurable.prod
-    · exact (measurable_pi_apply _).add (measurable_pi_apply _)
-    · exact (measurable_pi_apply _).add (measurable_pi_apply _)
-  · apply Measurable.add
-    · apply Measurable.add
-      · exact (measurable_pi_apply _).add (measurable_pi_apply _)
-      · apply measurable_pi_apply
-    · apply measurable_pi_apply
+  fun_prop
 
+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 : I[V : W | S] = I₂ := by
+lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ := by
   have h_indep2 : iIndepFun (fun _ ↦ hG) ![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)
@@ -118,14 +110,7 @@ lemma I₃_eq : I[V : W | S] = I₂ := by
               fin_cases i
               all_goals simp [h₁.map_eq] }
   have hmeas1 : Measurable (fun p : Fin 4 → G => (p 0 + p 1, p 0 + p 1 + p 2 + p 3)) := by
-    simp_all only [Matrix.cons_val', Matrix.empty_val', Matrix.cons_val_fin_one]
-    apply Measurable.prod
-    · exact (measurable_pi_apply _).add (measurable_pi_apply _)
-    · apply Measurable.add
-      · apply Measurable.add
-        · exact (measurable_pi_apply _).add (measurable_pi_apply _)
-        · apply measurable_pi_apply
-      · apply measurable_pi_apply
+    fun_prop
   have hUVS : IdentDistrib (prod U S) (prod V S) := by
     convert (hident.comp hmeas1); simp; abel
   have hUVWS : IdentDistrib (prod (prod U W) S) (prod (prod V W) S) := by
@@ -137,15 +122,15 @@ lemma I₃_eq : I[V : W | S] = I₂ := by
   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]
-  · exact Measurable.prod (by exact hU) (by exact hW)
-  · exact Measurable.prod (by exact hV) (by exact hW)
-
+  · exact Measurable.prod hU hW
+  · exact Measurable.prod hV hW
 
+include h_indep hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_min in
 /--
 `I[U : V | S] + I[V : W | S] + I[W : U | S]` is less than or equal to
 `6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁)`.
 -/
-lemma sum_condMutual_le :
+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
@@ -169,48 +154,63 @@ local notation3:max "c[" A " # " B "]" =>
 
 local notation3:max "c[" A " | " B " # " C " | " D "]" => d[p.X₀₁ # A|B] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # C|D] - d[p.X₀₂ # X₂])
 
-lemma hU : H[U] = H[X₁' + X₂'] :=
+include h_indep h₁ h₂ in
+lemma hU [IsProbabilityMeasure (ℙ : Measure Ω)] : H[U] = H[X₁' + X₂'] :=
   IdentDistrib.entropy_eq (h₁.add h₂
     (h_indep.indepFun (show (0 : Fin 4) ≠ 1 by norm_cast))
      (h_indep.indepFun (show (2 : Fin 4) ≠ 3 by norm_cast)))
 
 variable {X₁ X₂ X₁' X₂'} in
-lemma independenceCondition1 : iIndepFun (fun _ ↦ hG) ![X₁, X₂, X₁' + X₂'] :=
+include h_indep hX₁ hX₂ hX₁' hX₂' in
+lemma independenceCondition1 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![X₁, X₂, X₁' + X₂'] :=
   h_indep.apply_two_last hX₁ hX₂ hX₁' hX₂' measurable_add
 
-lemma hV : H[V] = H[X₁ + X₂'] :=
+include h₁ h₂ h_indep in
+lemma hV [IsProbabilityMeasure (ℙ : Measure Ω)] : H[V] = H[X₁ + X₂'] :=
 IdentDistrib.entropy_eq (h₁.symm.add h₂
   (h_indep.indepFun (show (2 : Fin 4) ≠ 1 by norm_cast))
   (h_indep.indepFun (show (0 : Fin 4) ≠ 3 by norm_cast)))
 
+include h_indep hX₁ hX₂ hX₁' hX₂' in
 variable {X₁ X₂ X₁' X₂'} in
-lemma independenceCondition2 : iIndepFun (fun _ ↦ hG) ![X₂, X₁, X₁' + X₂'] :=
+lemma independenceCondition2 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![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₂'] :=
+lemma independenceCondition3 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![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₂'] :=
+lemma independenceCondition4 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![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₂'] :=
+lemma independenceCondition5 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![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₁] :=
+lemma independenceCondition6 [IsProbabilityMeasure (ℙ : Measure Ω)] :
+    iIndepFun (fun _ ↦ hG) ![X₂, X₂', X₁' + X₁] :=
   independenceCondition1 hX₂ hX₂' hX₁' hX₁ h_indep.reindex_four_bdca
 
 set_option maxHeartbeats 400000 in
+include h_indep hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_min in
 /--
 $$ \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$$
 is less than or equal to
 $$ \leq (6 - 3\eta) k + 3(2 \eta k - I_1).$$
 -/
-lemma sum_dist_diff_le :
-  c[U|S # U|S] + c[V|S # V|S] + c[W|S # W|S] ≤ (6 - 3 * p.η)*k + 3 * (2*p.η*k - I₁) := by
+lemma sum_dist_diff_le [IsProbabilityMeasure (ℙ : Measure Ω)] [ElementaryAddCommGroup G 2] :
+    c[U|S # U|S] + c[V|S # V|S] + c[W|S # W|S] ≤ (6 - 3 * p.η)*k + 3 * (2*p.η*k - I₁) := by
   let X₀₁ := p.X₀₁
   let X₀₂ := p.X₀₂
   have ineq1 : d[X₀₁ # U | S] - d[X₀₁ # X₁] ≤ (H[S ; ℙ] - H[X₁ ; ℙ])/2 := by
@@ -326,14 +326,15 @@ lemma sum_dist_diff_le :
      _ = (6 - 3 * p.η)*k + 3 * (2*p.η*k - I₁) := by ring
 
 /-- `U + V + W = 0`. -/
-lemma sum_uvw_eq_zero : U+V+W = 0 := by
+lemma sum_uvw_eq_zero [ElementaryAddCommGroup G 2] : U+V+W = 0 := by
   rw [add_comm X₁' X₂, ElementaryAddCommGroup.sum_add_sum_add_sum_eq_zero]
 
 section construct_good
-variable {Ω' : Type*} [MeasureSpace Ω'] [IsProbabilityMeasure (ℙ : Measure Ω')]
+variable {Ω' : Type*} [MeasureSpace Ω']
 variable {T₁ T₂ T₃ : Ω' → G} (hT : T₁+T₂+T₃ = 0)
 variable (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃)
-
+  [IsProbabilityMeasure (ℙ : Measure Ω')] [ElementaryAddCommGroup G 2]
+  [IsProbabilityMeasure (ℙ : Measure Ω)]
 
 local notation3:max "δ[" μ "]" => I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ]
 local notation3:max "δ" => I[T₁ : T₂] + I[T₂ : T₃] + I[T₃ : T₁]
@@ -342,6 +343,7 @@ local notation3:max "ψ[" A " # " B "]" => d[A # B] + p.η * (c[A # B])
 local notation3:max "ψ[" A "; " μ " # " B " ; " μ' "]" =>
   d[A ; μ # B ; μ'] + p.η * c[A ; μ # B ; μ']
 
+include hT₁ hT₂ hT₃ hT h_min in
 /-- If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and
 $$ \delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$$
 Then there exist random variables $T'_1, T'_2$ such that
@@ -350,7 +352,7 @@ is at most
 $$ \delta + \eta ( d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2]) $$
 $$ + \tfrac12 \eta I[T_1: T_3] + \tfrac12 \eta I[T_2: T_3].$$
 -/
-lemma construct_good_prelim :
+lemma construct_good_prelim   :
     k ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁: T₃] + I[T₂ : T₃])/2 := by
   let sum1 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[T₁; ℙ[|T₃ ⁻¹' {t}] # T₂; ℙ[|T₃ ⁻¹' {t}]]]
   let sum2 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[p.X₀₁; ℙ # T₁; ℙ[|T₃ ⁻¹' {t}]] - d[p.X₀₁ # X₁]]
@@ -406,6 +408,7 @@ lemma construct_good_prelim :
     linarith only [distance_ge_of_min' (μ := ℙ[|T₃ ⁻¹' {t}]) (μ' := ℙ[|T₃ ⁻¹' {t}]) p h_min hT₁ hT₂]
   exact hk.trans h4
 
+include hT₁ hT₂ hT₃ hT h_min in
 /-- If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and
 -
 $$ \delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$$
@@ -419,20 +422,24 @@ is at most
 $$\delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3
     (d[X^0_i;T_j] - d[X^0_i; X_i]) \biggr).$$
 -/
-lemma construct_good : k ≤ δ + (p.η/3) * (δ + c[T₁ # T₁] + c[T₂ # T₂] + c[T₃ # T₃]) := by
+lemma construct_good
+    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')] :
+    k ≤ δ + (p.η/3) * (δ + c[T₁ # T₁] + c[T₂ # T₂] + c[T₃ # T₃]) := by
   have v2 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₁ hT₃ hT₂
   have v3 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₂ hT₁ hT₃
   have v6 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₃ hT₂ hT₁
   simp only [mutualInfo, entropy_comm hT₂ hT₁, entropy_comm hT₃ hT₁, entropy_comm hT₃ hT₂]
     at *
   linarith
 
-lemma construct_good' (μ : Measure Ω') [IsProbabilityMeasure μ]:
+include hT₁ hT₂ hT₃ hT h_min in
+lemma construct_good' (μ : Measure Ω') [IsProbabilityMeasure μ] :
     k ≤ δ[μ] + (p.η/3) * (δ[μ] + c[T₁ ; μ # T₁ ; μ] + c[T₂ ; μ # T₂ ; μ] + c[T₃ ; μ # T₃ ; μ]) := by
   letI : MeasureSpace Ω' := ⟨μ⟩
   apply construct_good p X₁ X₂ h_min hT hT₁ hT₂ hT₃
 
-lemma cond_c_eq_integral {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable Z) : c[Y | Z # Y | Z] =
+lemma cond_c_eq_integral
+    {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,
     Finset.sum_add_distrib]
@@ -445,10 +452,12 @@ lemma cond_c_eq_integral {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable
 variable {R : Ω' → G} (hR : Measurable R)
 local notation3:max "δ'" => I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁|R]
 
-lemma delta'_eq_integral : δ' = (Measure.map R ℙ)[fun r => δ[ℙ[|R⁻¹' {r}]]] := by
+lemma delta'_eq_integral :
+    δ' = (Measure.map R ℙ)[fun r => δ[ℙ[|R⁻¹' {r}]]] := by
   simp_rw [condMutualInfo_eq_integral_mutualInfo, integral_eq_sum, smul_add,
     Finset.sum_add_distrib]
 
+include hT₁ hT₂ hT₃ hT h_min hR hX₁ hX₂ in
 lemma cond_construct_good :
     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,
@@ -476,9 +485,11 @@ lemma cond_construct_good :
 
 end construct_good
 
+include hX₁ hX₂ h_min h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂' in
 /-- If `d[X₁ ; X₂] > 0` then there are `G`-valued random variables `X'₁, X'₂` such that
 Phrased in the contrapositive form for convenience of proof. -/
-theorem tau_strictly_decreases_aux (hpη: p.η = 1/9): d[X₁ # X₂] = 0 := by
+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)
@@ -490,7 +501,7 @@ theorem tau_strictly_decreases_aux (hpη: p.η = 1/9): d[X₁ # X₂] = 0 := by
       invFun := ![0, 1, 3, 2]
       left_inv := by intro i; fin_cases i <;> rfl
       right_inv := by intro i; fin_cases i <;> rfl }
-    refine' iIndepFun.reindex σ.symm _
+    refine iIndepFun.reindex σ.symm ?_
     convert h_indep using 1
     ext i; fin_cases i <;> rfl
   have h3 := first_estimate p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep' h_min

PFR/EntropyPFR.lean

@@ -26,9 +26,11 @@ variable {G : Type uG} [AddCommGroup G] [ElementaryAddCommGroup G 2] [Fintype G]
   [MeasurableSingletonClass G]
 variable (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ : Ω → G} {X₂ : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂)
 
+include hX₁ hX₂ in
 /-- If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$.
 Phrased in the contrapositive form for convenience of proof. -/
-theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1/9): d[X₁ # X₂] = 0 := by
+theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1/9) :
+    d[X₁ # X₂] = 0 := by
   let ⟨A, mA, μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩
     := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ
   rw [← h_id1.rdist_eq h_id2]
@@ -38,7 +40,6 @@ theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η
   apply tau_strictly_decreases_aux p Y₁ Y₂ Y₁' Y₂' hY₁ hY₂ hY₁' hY₂' (h_id1.trans h_id1'.symm)
     (h_id2.trans h_id2'.symm) h_indep h_min hpη
 
-
 /-- `entropic_PFR_conjecture`: For two $G$-valued random variables $X^0_1, X^0_2$, there is some
     subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$. -/
 theorem entropic_PFR_conjecture (hpη : p.η = 1/9):

PFR/Fibring.lean

@@ -136,15 +136,15 @@ lemma sum_of_rdist_eq_step_condMutualInfo {Y : Fin 4 → Ω → G}
     condMutualInfo_comm hmf hmij,
     ← condMutualInfo_of_inj_map hmij hmf hm0123 (fun z x ↦ (x + z, x)),
     condMutualInfo_comm hmg hmf]
-  . congr 1
+  · congr 1
     { ext ω
       { simp only [comp_apply, Pi.sub_apply, sub_sub_cancel] }
       { simp only [comp_apply, Pi.sub_apply, sub_sub_cancel] } }
     { rw [sub_sub, add_sub_left_comm, ← sub_sub]
       ext ω
       { simp only [comp_apply, Pi.sub_apply, add_sub_cancel] }
       { simp only [comp_apply, Pi.sub_apply, sub_sub_cancel] } }
-  . exact fun _ _ _ h ↦ (Prod.ext_iff.1 h).2
+  · exact fun _ _ _ h ↦ (Prod.ext_iff.1 h).2
   exact fun _ _ _ h ↦ (Prod.ext_iff.1 h).1