feat: complete the proof of PFR with exponent 9 (#231)

Also correct a few minor typos in the blueprint. And uniformize some notations throughout the Lean files (notably wrt `h_min` and `h_indep`).

PFR/ApproxHomPFR.lean

@@ -35,7 +35,6 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   let A := (Set.univ.graphOn f).toFinite.toFinset
   have hA : #A = Nat.card G := by rw [Set.Finite.card_toFinset]; simp [← Nat.card_eq_fintype_card]
   have hA_nonempty : A.Nonempty := by simp [-Set.Finite.toFinset_setOf, A]
-  have hA_pos : 0 < #A := by positivity
   have := calc
     (#A ^ 3 / K ^ 2 : ℝ)
       = (Nat.card G ^ 2 / K) ^ 2 / #A := by field_simp [hA]; ring
@@ -45,7 +44,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
       rw [← Nat.card_eq_finsetCard, ← Finset.coe_sort_coe, Finset.coe_filter,
         Set.Finite.toFinset_prod]
       simp only [Set.Finite.mem_toFinset, A, Set.graphOn_prod_graphOn]
-      rw [← Set.card_graphOn _ (Prod.map f f),
+      rw [← Set.natCard_graphOn _ (Prod.map f f),
         ← Nat.card_image_equiv (Equiv.prodProdProdComm G G' G G'), Set.image_equiv_eq_preimage_symm]
       congr
       aesop
@@ -66,7 +65,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     rewrite [← this, hA''_coe]
     simpa [← pow_mul] using hA'2
   obtain ⟨H, c, hc_card, hH_le, hH_ge, hH_cover⟩ := PFR_conjecture_improv_aux hA''_nonempty this
-  clear hA'2 hA''_coe hH_le hH_ge hA_pos
+  clear hA'2 hA''_coe hH_le hH_ge
   obtain ⟨H₀, H₁, φ, hH₀H₁, hH₀H₁_card⟩ := goursat H
 
   have h_le_H₀ : Nat.card A'' ≤ Nat.card c * Nat.card H₀ := by

PFR/BoundingMutual.lean

@@ -25,8 +25,8 @@ $$ {\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) (hindep:
+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)
-  (hmin : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω'] (X': Fin p.m × Fin p.m → Ω' → G) (hindep': iIndepFun (fun _ ↦ by infer_instance) X') (hperm:
+  (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

PFR/Endgame.lean

@@ -490,7 +490,7 @@ lemma cond_construct_good [IsProbabilityMeasure (ℙ : Measure Ω)] :
 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
+/-- 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
     [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2) G]

PFR/Fibring.lean

@@ -194,3 +194,11 @@ lemma sum_of_rdist_eq_char_2
         + 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 [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'] μ)
+  (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' ; μ]
+      + I[X + Y : Y + Y' | X + Y + X' + Y' ; μ] := by
+  apply sum_of_rdist_eq_char_2 _ h_indep (fun i ↦ by fin_cases i <;> assumption)

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)) (hindep : iIndepFun (fun (_ : I) => hG) X μ) :
+    (hX : (i : I) → Measurable (X i)) (h_indep : iIndepFun (fun (_ : I) => hG) X μ) :
     H[X i₀ ; μ] ≤ H[∏ i in s, X i ; μ] := by
   have hs : s.Nonempty := ⟨i₀, hi₀⟩
   induction' hs using Finset.Nonempty.cons_induction with i j s Hnot _ Hind
@@ -254,13 +254,13 @@ lemma max_entropy_le_entropy_prod {G : Type*} [Countable G] [hG : MeasurableSpac
         _ ≤ max H[X i₀ ; μ] H[∏ i ∈ s, X i ; μ] := le_max_left _ _
         _ ≤ H[X i₀ * ∏ i ∈ s, X i ; μ] := by
           refine max_entropy_le_entropy_mul (hX i₀) (by fun_prop) ?_
-          exact iIndepFun.indepFun_finset_prod_of_not_mem hindep hX Hnot |>.symm
+          exact iIndepFun.indepFun_finset_prod_of_not_mem h_indep hX Hnot |>.symm
     · calc
         _ ≤ H[∏ i ∈ s, X i ; μ] := Hind hi₀
         _ ≤ max H[X j ; μ] H[∏ i ∈ s, X i ; μ] := le_max_right _ _
         _ ≤ H[X j * ∏ x ∈ s, X x ; μ] := by
           refine max_entropy_le_entropy_mul (hX j) (by fun_prop) ?_
-          exact iIndepFun.indepFun_finset_prod_of_not_mem hindep hX Hnot |>.symm
+          exact iIndepFun.indepFun_finset_prod_of_not_mem h_indep hX Hnot |>.symm
 
 end IsProbabilityMeasure
 end ProbabilityTheory

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -246,7 +246,8 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
       simp at hu ⊢
       exact hu hs
     exact MeasurableSet.compl (Finset.measurableSet _)
-  rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht), integral_finset _ _ IntegrableOn.finset,
+  rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht),
+    integral_finset _ _ IntegrableOn.finset,
     ← Finset.sum_add_distrib, Finset.sum_product]
   apply Finset.sum_congr rfl
   intro s hs

PFR/ForMathlib/Entropy/Measure.lean

@@ -66,12 +66,35 @@ def _root_.MeasureTheory.Measure.support (μ : Measure S) [hμ : FiniteSupport 
   hμ.finite.choose.filter (μ {·} ≠ 0)
 
 lemma measure_compl_support (μ : Measure S) [hμ : FiniteSupport μ] : μ μ.supportᶜ = 0 := by
-  simp [Measure.support, compl_setOf, not_and_or, -not_and, setOf_or]
-  refine ⟨hμ.finite.choose_spec, ?_⟩
-  sorry
+  let A := hμ.finite.choose
+  have : (μ.support : Set S)ᶜ ⊆ (A : Set S)ᶜ ∪ ⋃ x ∈ A.filter (μ {·} = 0), {x} := by
+    intro z hz
+    simp only [Measure.support, ne_eq, Finset.coe_filter, mem_compl_iff, mem_setOf_eq, not_and,
+      Decidable.not_not] at hz
+    by_cases h'z : z ∈ A
+    · simp [hz h'z, h'z]
+    · simp [h'z]
+  apply le_antisymm ?_ bot_le
+  calc μ (μ.support : Set S)ᶜ ≤ μ ((A : Set S)ᶜ ∪ ⋃ x ∈ A.filter (μ {·} = 0), {x}) :=
+    measure_mono this
+  _ ≤ μ (Aᶜ) + ∑ x ∈ A.filter (μ {·} = 0), μ {x} := by
+    apply (measure_union_le _ _).trans
+    gcongr
+    apply measure_biUnion_finset_le
+  _ ≤ 0 + ∑ x ∈ A.filter (μ {·} = 0), 0 := by
+    gcongr with x hx
+    · exact hμ.finite.choose_spec.le
+    · simp only [Finset.mem_filter] at hx
+      exact hx.2.le
+  _ = 0 := by simp
 
 @[simp] lemma mem_support {μ : Measure S} [hμ : FiniteSupport μ] {x : S} :
-    x ∈ μ.support ↔ μ {x} ≠ 0 := sorry
+    x ∈ μ.support ↔ μ {x} ≠ 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · simp only [Measure.support, ne_eq, Finset.mem_filter] at h
+    exact h.2
+  · contrapose! h
+    exact measure_mono_null (by simpa using h) (measure_compl_support μ)
 
 instance finiteSupport_zero : FiniteSupport (0 : Measure S) where
   finite := ⟨(∅ : Finset S), by simp⟩
@@ -157,7 +180,7 @@ lemma integrable_of_finiteSupport (μ : Measure S) [FiniteSupport μ]
   apply Integrable.comp_measurable .of_finite
   fun_prop
 
-lemma integral_congr_finiteSupport {μ : Measure Ω} {G : Type*} [MeasurableSingletonClass Ω]
+lemma integral_congr_finiteSupport {μ : Measure Ω} {G : Type*}
     [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : Ω → G} [FiniteSupport μ]
     (hfg : ∀ x, μ {x} ≠ 0 → f x = g x) : ∫ x, f x ∂μ = ∫ x, g x ∂μ := by
   refine integral_congr_ae <| measure_mono_null ?_ <| measure_compl_support μ

PFR/ForMathlib/Entropy/RuzsaDist.lean

@@ -25,6 +25,7 @@ Here we define Ruzsa distance and establish its basic properties.
 -/
 
 open Filter Function MeasureTheory Measure ProbabilityTheory
+open scoped Topology
 
 variable {Ω Ω' Ω'' Ω''' G S T : Type*}
   [mΩ : MeasurableSpace Ω] {μ : Measure Ω}
@@ -130,6 +131,28 @@ lemma ProbabilityTheory.IdentDistrib.rdist_eq {X' : Ω'' → G} {Y' : Ω''' →
     d[X ; μ # Y ; μ'] = d[X' ; μ'' # Y' ; μ'''] := by
   simp [rdist, hX.map_eq, hY.map_eq, hX.entropy_eq, hY.entropy_eq]
 
+lemma tendsto_rdist_probabilityMeasure {α : Type*} {l : Filter α}
+    [TopologicalSpace Ω] [BorelSpace Ω] [TopologicalSpace G] [BorelSpace G] [Fintype G]
+    [DiscreteTopology G]
+    {X Y : Ω → G} (hX : Continuous X) (hY : Continuous Y)
+    {μ : α → ProbabilityMeasure Ω} {ν : ProbabilityMeasure Ω} (hμ : Tendsto μ l (𝓝 ν)) :
+    Tendsto (fun n ↦ d[X ; (μ n : Measure Ω) # Y ; (μ n : Measure Ω)]) l
+      (𝓝 (d[X ; ν # Y ; ν])) := by
+  have J (η : ProbabilityMeasure Ω) :
+      d[X ; η # Y ; η] = d[(id : G → G) ; η.map hX.aemeasurable # id ; η.map hY.aemeasurable] := by
+    apply ProbabilityTheory.IdentDistrib.rdist_eq
+    · exact ⟨hX.aemeasurable, aemeasurable_id, by simp⟩
+    · exact ⟨hY.aemeasurable, aemeasurable_id, by simp⟩
+  simp_rw [J]
+  have Z := ((continuous_rdist_restrict_probabilityMeasure (G := G)).tendsto
+    ((ν.map hX.aemeasurable), (ν.map hY.aemeasurable)))
+  have T : Tendsto (fun n ↦ (((μ n).map hX.aemeasurable), ((μ n).map hY.aemeasurable)))
+      l (𝓝 (((ν.map hX.aemeasurable), (ν.map hY.aemeasurable)))) := by
+    apply Tendsto.prod_mk_nhds
+    · exact ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous μ ν hμ hX
+    · exact ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous μ ν hμ hY
+  apply Z.comp T
+
 section rdist
 
 variable [Countable G] [MeasurableSingletonClass G]
@@ -151,10 +174,10 @@ lemma rdist_le_avg_ent {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRan
   [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
     d[X ; μ # Y ; μ'] ≤ (H[X ; μ] + H[Y ; μ'])/2 := by
   rcases ProbabilityTheory.independent_copies_finiteRange hX hY μ μ'
-    with ⟨ν, X', Y', hprob, hX', hY', hindep, hidentX, hidentY, hfinX, hfinY⟩
+    with ⟨ν, X', Y', hprob, hX', hY', h_indep, hidentX, hidentY, hfinX, hfinY⟩
   rw [← ProbabilityTheory.IdentDistrib.rdist_eq hidentX hidentY,
     ← IdentDistrib.entropy_eq hidentX, ← IdentDistrib.entropy_eq hidentY,
-    ProbabilityTheory.IndepFun.rdist_eq hindep hX' hY']
+    ProbabilityTheory.IndepFun.rdist_eq h_indep hX' hY']
   suffices H[X' - Y'; ν] ≤ H[X'; ν] + H[Y'; ν] by linarith
   change H[(fun x ↦ x.1 - x.2) ∘ ⟨X',Y' ⟩; ν] ≤ H[X'; ν] + H[Y'; ν]
   exact ((entropy_comp_le ν (by fun_prop) _).trans) (entropy_pair_le_add hX' hY' ν)
@@ -336,9 +359,13 @@ lemma ent_of_proj_le {UH: Ω' → G} [FiniteRange UH]
   linarith only [this, (abs_le.mp (diff_ent_le_rdist hX' hUH' (μ := ν) (μ' := ν))).2]
 
 /-- Adding a constant to a random variable does not change the Rusza distance. -/
-lemma rdist_add_const [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
+lemma rdist_add_const [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']
     (hX : Measurable X) (hY : Measurable Y) {c} :
     d[X ; μ # Y + fun _ ↦ c; μ'] = d[X ; μ # Y ; μ'] := by
+  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
+  · simp [rdist_def, entropy_add_const hY]
+  rcases eq_zero_or_isProbabilityMeasure μ' with rfl | hμ'
+  · simp [rdist_def]
   obtain ⟨ν, X', Y', _, hX', hY', hind, hIdX, hIdY, _, _⟩ := independent_copies_finiteRange hX hY μ μ'
   have A : IdentDistrib (Y' + fun _ ↦ c) (Y + fun _ ↦ c) ν μ' := by
     change IdentDistrib (fun ω ↦ Y' ω + c) (fun ω ↦ Y ω + c) ν μ'
@@ -353,8 +380,8 @@ lemma rdist_add_const [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
   exact hX'.sub hY'
 
 /-- A variant of `rdist_add_const` where one adds constants to both variables. -/
-lemma rdist_add_const' [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (c : G) (c' : G)
-    (hX : Measurable X) (hY : Measurable Y) :
+lemma rdist_add_const' [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']
+    (c : G) (c' : G) (hX : Measurable X) (hY : Measurable Y) :
     d[X + fun _ ↦ c; μ # Y + fun _ ↦ c'; μ'] = d[X ; μ # Y ; μ'] := by
   rw [rdist_add_const _ hY, rdist_symm, rdist_add_const hY hX, rdist_symm]
   fun_prop

PFR/ForMathlib/GroupQuot.lean

@@ -11,12 +11,15 @@ open Finsupp Function
 variable {G : Type*} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ}
 
 variable (G n) in
+/-- `modN G n` denotes the quotient of `G` by multiples of `n` -/
 abbrev modN : Type _ := G ⧸ LinearMap.range (LinearMap.lsmul ℤ G n)
 
 instance : Module (ZMod n) (modN G n) := QuotientAddGroup.zmodModule (by simp)
 
 variable [NeZero n]
 
+/-- Given a free module `G` over `ℤ`, construct the corresponding basis
+of `G / ⟨n⟩` over `ℤ / nℤ`. -/
 noncomputable def modNBasis : Basis (Module.Free.ChooseBasisIndex ℤ G) (ZMod n) (modN G n) := by
   set ψ : G →+ G := zsmulAddGroupHom n
   set nG := LinearMap.range (LinearMap.lsmul ℤ G n)

PFR/ForMathlib/MeasureReal.lean

@@ -479,7 +479,7 @@ theorem measureReal_prod_prod {μ : Measure α} {ν : Measure β} [SigmaFinite 
     (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t := by
   simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]
 
-theorem ext_iff_measureReal_singleton [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]
+theorem ext_iff_measureReal_singleton [Fintype S] [MeasurableSpace S]
     {μ1 μ2 : Measure S} [IsFiniteMeasure μ1] [IsFiniteMeasure μ2] :
     μ1 = μ2 ↔ ∀ x, μ1.real {x} = μ2.real {x} := by
   rw [Measure.ext_iff_singleton]

PFR/ForMathlib/ProbabilityMeasureProdCont.lean

@@ -1,5 +1,6 @@
 import PFR.ForMathlib.CompactProb
 import PFR.ForMathlib.FiniteMeasureProd
+import Mathlib.Tactic.Peel
 
 /-!
 # Continuity of products of probability measures on finite types
@@ -11,7 +12,7 @@ open scoped Topology ENNReal NNReal BoundedContinuousFunction
 namespace MeasureTheory
 
 /-- Probability measures on a finite space tend to a limit if and only if the probability masses
-of all points tend to the corresponding limits. -/
+of all points tend to the corresponding limits. Version in ℝ≥0. -/
 lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {ι α : Type*} {L : Filter ι} [Finite α]
     [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α]
     (μs : ι → ProbabilityMeasure α) (μ : ProbabilityMeasure α) :
@@ -27,6 +28,17 @@ lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {ι α : Type*} {L : F
     simp only [Function.comp_apply, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure, coe_toNNReal]
     simp only [ne_eq, ennreal_coeFn_eq_coeFn_toMeasure]
 
+/-- Probability measures on a finite space tend to a limit if and only if the probability masses
+of all points tend to the corresponding limits. Version in ℝ≥0∞. -/
+lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal
+    {ι α : Type*} {L : Filter ι} [Finite α]
+    [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α]
+    (μs : ι → ProbabilityMeasure α) (μ : ProbabilityMeasure α) :
+    Tendsto μs L (𝓝 μ) ↔ ∀ a, Tendsto (fun n ↦ (μs n : Measure α) {a}) L
+      (𝓝 ((μ : Measure α) {a})) := by
+  rw [ProbabilityMeasure.tendsto_iff_forall_apply_tendsto]
+  simp [← ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe]
+
 /-- If probability measures on two finite spaces tend to limits, then the products of them
 on the product space tend to the product of the limits.
 TODO: In Mathlib, this should be done on all separable metrizable spaces. -/
@@ -57,7 +69,7 @@ TODO: In Mathlib, this should be done on all separable metrizable spaces. -/
 lemma ProbabilityMeasure.continuous_prod_of_finite {α β : Type*}
     [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α]
     [Finite β] [TopologicalSpace β] [DiscreteTopology β] [MeasurableSpace β] [BorelSpace β] :
-    Continuous (fun (⟨μ, ν⟩ : ProbabilityMeasure α × ProbabilityMeasure β) ↦ (μ.prod ν)) := by
+    Continuous (fun (m : ProbabilityMeasure α × ProbabilityMeasure β) ↦ (m.1.prod m.2)) := by
   rw [continuous_iff_continuousAt]
   intro μν
   apply continuousAt_of_tendsto_nhds (y := μν.1.prod μν.2)

PFR/HundredPercent.lean

@@ -65,14 +65,14 @@ lemma sub_mem_symmGroup (hX : Measurable X) (hdist : d[X # X] = 0)
   In particular, `X' - x` and `X' - y` have the same distribution, which is equivalent to the
   claim of the lemma. -/
   rcases ProbabilityTheory.independent_copies_two hX hX with
-    ⟨Ω', mΩ', X', Y', hP, hX', hY', hindep, hidX, hidY⟩
+    ⟨Ω', mΩ', X', Y', hP, hX', hY', h_indep, hidX, hidY⟩
   rw [hidX.symm.symmGroup_eq hX hX']
   have A : H[X' - Y' | Y'] = H[X' - Y'] := calc
     H[X' - Y' | Y'] = H[X' | Y'] := condEntropy_sub_right hX' hY'
-    _ = H[X'] := hindep.condEntropy_eq_entropy hX' hY'
+    _ = H[X'] := h_indep.condEntropy_eq_entropy hX' hY'
     _ = H[X' - Y'] := by
       have : d[X' # Y'] = 0 := by rwa [hidX.rdist_eq hidY]
-      rw [hindep.rdist_eq hX' hY', ← (hidX.trans hidY.symm).entropy_eq] at this
+      rw [h_indep.rdist_eq hX' hY', ← (hidX.trans hidY.symm).entropy_eq] at this
       linarith
   have I : IndepFun (X' - Y') Y' := by
     refine (mutualInfo_eq_zero (by fun_prop) hY').1 ?_
@@ -87,7 +87,7 @@ lemma sub_mem_symmGroup (hX : Measurable X) (hdist : d[X # X] = 0)
       ℙ (F ⁻¹' s) * ℙ (Y' ⁻¹' {c}) = ℙ (F ⁻¹' s ∩ Y' ⁻¹' {c}) := by
         have hFY' : IndepFun F Y' := by
           have : Measurable (fun z ↦ z - c) := measurable_sub_const' c
-          apply hindep.comp this measurable_id
+          apply h_indep.comp this measurable_id
         rw [indepFun_iff_measure_inter_preimage_eq_mul.1 hFY' _ _ hs .of_discrete]
       _ = ℙ ((X' - Y') ⁻¹' s ∩ Y' ⁻¹' {c}) := by
         congr 1; ext z; simp (config := {contextual := true})

PFR/ImprovedPFR.lean

@@ -198,6 +198,7 @@ lemma gen_ineq_aux2 :
 include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 /-- Let `Z₁, Z₂, Z₃, Z₄` be independent `G`-valued random variables, and let `Y` be another
 `G`-valued random variable. Set `S := Z₁ + Z₂ + Z₃ + Z₄`. Then
+`d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤`
 `(d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4`
 `+ (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4`
 `+ (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8`.
@@ -1035,7 +1036,6 @@ theorem PFR_conjecture_improv (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K
           * (Nat.card H / (Nat.card A / 2)) := by
         gcongr
     _ = 2 * K ^ 6 * Nat.card A ^ (-1/2) * Nat.card H ^ (1/2) := by
-        have : (0 : ℝ) < Nat.card H := H_pos
         field_simp
         rpow_ring
         norm_num