Bump mathlib

PFR.lean

@@ -22,7 +22,8 @@ import PFR.ForMathlib.FiniteMeasureProd
 import PFR.ForMathlib.FiniteRange.ConditionalProbability
 import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.GroupQuot
-import PFR.ForMathlib.MeasureReal
+import PFR.ForMathlib.MeasureReal.Defs
+import PFR.ForMathlib.MeasureReal.UniformOn
 import PFR.ForMathlib.Pair
 import PFR.ForMathlib.ProbabilityMeasureProdCont
 import PFR.ForMathlib.Uniform

PFR/ForMathlib/ConditionalIndependence.lean

@@ -1,5 +1,4 @@
 import Mathlib.Tactic.Finiteness
-import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib
 import PFR.ForMathlib.FiniteRange.ConditionalProbability
 import PFR.ForMathlib.Pair

PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean

@@ -20,8 +20,7 @@ variable {T T' T'' G : Type*} [MeasurableSpace T] [MeasurableSpace T'] [Measurab
 /-- The Rusza distance between two measures, defined as `H[X - Y] - H[X]/2 - H[Y]/2` where `X`
 and `Y` are independent variables distributed according to the two measures. -/
 noncomputable
-def rdistm (μ : Measure G) (ν : Measure G) : ℝ :=
-    Hm[(μ.prod ν).map (fun x ↦ x.1 - x.2)] - Hm[μ]/2 - Hm[ν]/2
+def rdistm (μ ν : Measure G) : ℝ := Hm[(μ.prod ν).map (fun x ↦ x.1 - x.2)] - Hm[μ]/2 - Hm[ν]/2
 
 /-- The Rusza distance between two kernels taking values in the same space, defined as the average
 Rusza distance between the image measures. -/

PFR/ForMathlib/Entropy/Measure.lean

@@ -1,10 +1,8 @@
 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.ForMathlib.MeasureReal.Defs
 
 /-!
 # Entropy of a measure

PFR/ForMathlib/FiniteMeasureComponent.lean

@@ -1,5 +1,5 @@
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-import PFR.ForMathlib.MeasureReal
+import PFR.ForMathlib.MeasureReal.Defs
 
 /-!
 # The measure of a connected component of a space depends continuously on a finite measure

PFR/ForMathlib/MeasureReal/UniformOn.lean

@@ -0,0 +1,40 @@
+import PFR.Mathlib.Probability.UniformOn
+import PFR.ForMathlib.Entropy.Measure
+import PFR.ForMathlib.MeasureReal.Defs
+
+open MeasureTheory Measure Real
+
+namespace ProbabilityTheory
+variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} {x : Ω}
+
+lemma uniformOn_apply' (hs : s.Finite) (t : Set Ω) :
+    (uniformOn s).real t = (Nat.card ↑(s ∩ t)) / Nat.card s := by
+  simp [measureReal_def, uniformOn_apply hs]
+
+end ProbabilityTheory
+
+namespace ProbabilityTheory
+
+variable {S : Type*} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite H]
+
+/-- The entropy of a uniform measure is the log of the cardinality of its support. -/
+lemma entropy_of_uniformOn [Nonempty H] : measureEntropy (uniformOn H) = log (Nat.card H) := by
+  simp only [measureEntropy_def', IsProbabilityMeasure.measureReal_univ, inv_one, Pi.smul_apply,
+    uniformOn_apply', Set.toFinite, smul_eq_mul, one_mul]
+  classical
+  calc ∑' s, negMulLog ((Nat.card (H ∩ {s} : Set S)) / (Nat.card H))
+    _ = ∑' s, if s ∈ H then negMulLog (1 / (Nat.card H)) else 0 := by
+      congr with s
+      by_cases h : s ∈ H <;> simp [h, Finset.filter_true_of_mem, Finset.filter_false_of_mem]
+    _ = ∑ s in H.toFinite.toFinset, negMulLog (1 / (Nat.card H)) := by
+      convert tsum_eq_sum (s := H.toFinite.toFinset) ?_ using 2 with s hs
+      · simp at hs; simp [hs]
+      intro s hs
+      simp only [Set.Finite.mem_toFinset] at hs; simp [hs]
+    _ = (Nat.card H) * negMulLog (1 / (Nat.card H)) := by
+      simp [← Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq]
+    _ = log (Nat.card H) := by
+      simp only [negMulLog, one_div, log_inv, mul_neg, neg_mul, neg_neg, ← mul_assoc]
+      rw [mul_inv_cancel₀, one_mul]
+      simp only [ne_eq, Nat.cast_eq_zero, Nat.card_ne_zero]
+      exact ⟨ ‹_›, ‹_› ⟩

PFR/ForMathlib/Uniform.lean

@@ -1,10 +1,9 @@
 import Mathlib.Probability.IdentDistrib
-import Mathlib.Probability.ConditionalProbability
-import PFR.ForMathlib.MeasureReal
-import PFR.ForMathlib.FiniteRange.Defs
 import PFR.Mathlib.Probability.UniformOn
+import PFR.ForMathlib.FiniteRange.Defs
+import PFR.ForMathlib.MeasureReal.Defs
 
-open Function MeasureTheory Set
+open Function MeasureTheory Measure Set
 open scoped ENNReal
 
 namespace ProbabilityTheory
@@ -269,3 +268,46 @@ lemma IsUniform.map_eq_uniformOn [Countable S] [IsProbabilityMeasure μ]
   have : IdentDistrib X id μ (uniformOn (H : Set S)) :=
     IdentDistrib.of_isUniform (H := H) hX measurable_id h isUniform_uniformOn
   simpa using this.map_eq
+
+/-- A random variable is uniform iff its distribution is. -/
+lemma isUniform_iff_map_eq_uniformOn [Finite H] {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω)
+    [Countable S] [IsProbabilityMeasure μ] {U : Ω → S} (hU : Measurable U) :
+  ProbabilityTheory.IsUniform H U μ ↔ μ.map U = uniformOn H := by
+  constructor
+  · intro h_unif
+    ext A hA
+    let Hf := H.toFinite.toFinset
+    have h_unif': ProbabilityTheory.IsUniform Hf U μ := (Set.Finite.coe_toFinset H.toFinite).symm ▸ h_unif
+    let AHf := (A ∩ H).toFinite.toFinset
+    rw [uniformOn_apply ‹_›, ← MeasureTheory.Measure.tsum_indicator_apply_singleton _ _ hA]
+    classical
+    calc ∑' x, Set.indicator A (fun x => (μ.map U) {x}) x
+      _ = ∑' x, (if x ∈ (A ∩ H) then (1:ENNReal) / (Nat.card H) else 0) := by
+        congr with x
+        by_cases h : x ∈ A
+        · by_cases h' : x ∈ H
+          · simp [h, h', Hf, map_apply hU (MeasurableSet.singleton x), ProbabilityTheory.IsUniform.measure_preimage_of_mem h_unif' hU ((Set.Finite.coe_toFinset H.toFinite).symm ▸ h')]
+          simp [h, h', map_apply hU (MeasurableSet.singleton x), ProbabilityTheory.IsUniform.measure_preimage_of_nmem h_unif' ((Set.Finite.coe_toFinset H.toFinite).symm ▸ h')]
+        simp [h]
+      _ = Finset.sum AHf (fun _ ↦ (1:ENNReal) / (Nat.card H)) := by
+        rw [tsum_eq_sum (s := (A ∩ H).toFinite.toFinset)]
+        · apply Finset.sum_congr (by rfl)
+          intro x hx
+          simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff, AHf] at hx
+          simp [hx]
+        intro x hx
+        simp at hx
+        simpa
+      _ = Nat.card ↑(H ∩ A) / Nat.card H := by
+        simp [Finset.sum_const, ← Set.ncard_eq_toFinset_card (A ∩ H), Set.Nat.card_coe_set_eq,
+          Set.inter_comm]
+        rfl
+  intro this
+  constructor
+  · intro x hx y hy
+    replace hx : {x} ∩ H = {x} := by simp [hx]
+    replace hy : {y} ∩ H = {y} := by simp [hy]
+    simp [← map_apply hU (MeasurableSet.singleton _), this, uniformOn_apply, hx, hy, Set.toFinite,
+      Set.inter_comm H]
+  · rw [← map_apply hU (by measurability), this, uniformOn_apply ‹_›]
+    simp

PFR/ImprovedPFR.lean

@@ -4,10 +4,6 @@ import PFR.Main
 # Improved PFR
 
 An improvement to PFR that lowers the exponent from 12 to 11.
-
-## Main results
-
-*
 -/
 
 /- In this file the power notation will always mean the base and exponent are real numbers. -/
@@ -904,7 +900,7 @@ lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤
   rw [← hHH'] at VH'unif
   have H_fin : Finite (H : Set G) := by infer_instance
 
-  have : d[VA # VH] ≤ 10/2 * log K := by rw [idVA.rdist_eq idVH]; linarith
+  have : d[VA # VH] ≤ 5 * log K := by rw [idVA.rdist_eq idVH]; linarith
   have H_pos : (0 : ℝ) < Nat.card H := by
     have : 0 < Nat.card H := Nat.card_pos
     positivity
@@ -927,15 +923,15 @@ lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤
     · exact (exp_log H_pos).symm
     · rw [exp_add, exp_log A_pos, ← rpow_def_of_pos K_pos]
   -- entropic PFR shows that the entropy of `VA - VH` is small
-  have I : log K * (-10/2) + log (Nat.card A) * (-1/2) + log (Nat.card H) * (-1/2)
+  have I : log K * (-5) + log (Nat.card A) * (-1/2) + log (Nat.card H) * (-1/2)
       ≤ - H[VA - VH] := by
     rw [Vindep.rdist_eq VAmeas VHmeas] at this
     linarith
   -- therefore, there exists a point `x₀` which is attained by `VA - VH` with a large probability
   obtain ⟨x₀, h₀⟩ : ∃ x₀ : G, rexp (- H[VA - VH]) ≤ (ℙ : Measure Ω).real ((VA - VH) ⁻¹' {x₀}) :=
     prob_ge_exp_neg_entropy' _ ((VAmeas.sub VHmeas).comp measurable_id')
   -- massage the previous inequality to get that `A ∩ (H + {x₀})` is large
-  have J : K ^ (-10/2) * Nat.card A ^ (1/2) * Nat.card H ^ (1/2) ≤
+  have J : K ^ (-5) * Nat.card A ^ (1/2) * Nat.card H ^ (1/2) ≤
       Nat.card (A ∩ (H + {x₀}) : Set G) := by
     rw [VA'unif.measureReal_preimage_sub VAmeas VH'unif VHmeas Vindep] at h₀
     have := (Real.exp_monotone I).trans h₀
@@ -950,7 +946,7 @@ lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤
     · rw [hAA', hHH']
     positivity
 
-  have Hne : Set.Nonempty (A ∩ (H + {x₀} : Set G)) := by
+  have Hne : (A ∩ (H + {x₀} : Set G)).Nonempty := by
     by_contra h'
     have : (0 : ℝ) < Nat.card (A ∩ (H + {x₀}) : Set G) := lt_of_lt_of_le (by positivity) J
     simp only [Nat.card_eq_fintype_card, card_of_isEmpty, CharP.cast_eq_zero, lt_self_iff_false,
@@ -959,30 +955,27 @@ lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤
   (which is contained in `H`). The number of translates is at most
   `#(A + (A ∩ (H + {x₀}))) / #(A ∩ (H + {x₀}))`, where the numerator is controlled as this is
   a subset of `A + A`, and the denominator is bounded below by the previous inequality`. -/
-  rcases Set.exists_subset_add_sub (toFinite A) (toFinite (A ∩ ((H + {x₀} : Set G)))) Hne with
-    ⟨u, hu, Au, -⟩
-  have Iu : Nat.card u ≤ K ^ 6 * Nat.card A ^ (1/2) * Nat.card H ^ (-1/2) := by
-    have : (0 : ℝ) ≤ Nat.card u := by simp
-    have Z1 := mul_le_mul_of_nonneg_left J this
-    have Z2 : (Nat.card u * Nat.card (A ∩ (H + {x₀}) : Set G) : ℝ)
-      ≤ Nat.card (A + A ∩ (↑H + {x₀})) := by norm_cast
-    have Z3 : (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ) ≤ K * Nat.card A := by
-      apply le_trans _ hA
-      simp only [Nat.cast_le]
-      apply Nat.card_mono (toFinite _)
-      apply add_subset_add_left inter_subset_left
-    have : 0 ≤ K ^ (10/2) * Nat.card A ^ (-1/2) * Nat.card H ^ (-1/2) := by positivity
-    have T := mul_le_mul_of_nonneg_left ((Z1.trans Z2).trans Z3) this
-    convert T using 1 <;> rpow_ring <;> norm_num
+  have Z3 :
+      (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ) ≤ (K ^ 6 * Nat.card A ^ (1/2 : ℝ) *
+        Nat.card H ^ (-1/2 : ℝ)) * Nat.card ↑(A ∩ (↑H + {x₀})) := by
+    calc
+      (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ)
+      _ ≤ Nat.card (A + A) := by
+        gcongr; exact Nat.card_mono (toFinite _) <| add_subset_add_left inter_subset_left
+      _ ≤ K * Nat.card A := hA
+      _ = (K ^ 6 * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ)) *
+          (K ^ (-5 : ℝ) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (1/2 : ℝ)) := by
+        rpow_ring; norm_num
+      _ ≤ (K ^ 6 * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ)) *
+        Nat.card ↑(A ∩ (↑H + {x₀})) := by gcongr
+  obtain ⟨u, huA, hucard, hAu, -⟩ :=
+    Set.ruzsa_covering_add (toFinite A) (toFinite (A ∩ ((H + {x₀} : Set G)))) Hne (by convert Z3)
   have A_subset_uH : A ⊆ u + H := by
-    apply Au.trans
-    rw [add_sub_assoc]
-    apply add_subset_add_left
-    apply (sub_subset_sub inter_subset_right inter_subset_right).trans
-    rintro - ⟨-, ⟨y, hy, xy, hxy, rfl⟩, -, ⟨z, hz, xz, hxz, rfl⟩, rfl⟩
-    simp only [mem_singleton_iff] at hxy hxz
-    simpa [hxy, hxz] using H.sub_mem hy hz
-  exact ⟨H, u, Iu, IHA, IAH, A_subset_uH⟩
+    refine hAu.trans $ add_subset_add_left $
+      (sub_subset_sub (inter_subset_right ..) (inter_subset_right ..)).trans ?_
+    rw [add_sub_add_comm, singleton_sub_singleton, sub_self]
+    simp
+  exact ⟨H, u, hucard, IHA, IAH, A_subset_uH⟩
 
 /-- The polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian
 2-group of doubling constant at most $K$, then $A$ can be covered by at most $2K^{11$} cosets of

PFR/Main.lean

@@ -188,7 +188,7 @@ lemma PFR_conjecture_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat
   rw [← hAA'] at VA'unif
   have VHunif : IsUniform H VH := UHunif.of_identDistrib idVH.symm .of_discrete
   let H' := (H : Set G).toFinite.toFinset
-  have hHH' : H' = (H : Set G) := Finite.coe_toFinset (toFinite (H : Set G))
+  have hHH' : H' = (H : Set G) := (toFinite (H : Set G)).coe_toFinset
   have VH'unif := VHunif
   rw [← hHH'] at VH'unif
 
@@ -238,7 +238,7 @@ lemma PFR_conjecture_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat
     · rw [hAA', hHH']
     positivity
 
-  have Hne : Set.Nonempty (A ∩ (H + {x₀} : Set G)) := by
+  have Hne : (A ∩ (H + {x₀} : Set G)).Nonempty := by
     by_contra h'
     have : (0 : ℝ) < Nat.card (A ∩ (H + {x₀}) : Set G) := lt_of_lt_of_le (by positivity) J
     simp only [Nat.card_eq_fintype_card, card_of_isEmpty, CharP.cast_eq_zero, lt_self_iff_false,
@@ -247,30 +247,27 @@ lemma PFR_conjecture_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat
   (which is contained in `H`). The number of translates is at most
   `#(A + (A ∩ (H + {x₀}))) / #(A ∩ (H + {x₀}))`, where the numerator is controlled as this is
   a subset of `A + A`, and the denominator is bounded below by the previous inequality`. -/
-  rcases Set.exists_subset_add_sub (toFinite A) (toFinite (A ∩ ((H + {x₀} : Set G)))) Hne with
-    ⟨u, hu, Au, -⟩
-  have Iu :
-    Nat.card u ≤ K ^ (13/2 : ℝ) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ) := by
-    have : (0 : ℝ) ≤ Nat.card u := by simp
-    have Z1 := mul_le_mul_of_nonneg_left J this
-    have Z2 : (Nat.card u * Nat.card (A ∩ (H + {x₀}) : Set G) : ℝ)
-      ≤ Nat.card (A + A ∩ (↑H + {x₀})) := by norm_cast
-    have Z3 : (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ) ≤ K * Nat.card A := by
-      apply le_trans _ hA
-      simp only [Nat.cast_le]
-      apply Nat.card_mono (toFinite _)
-      apply add_subset_add_left inter_subset_left
-    have : 0 ≤ K ^ (11/2 : ℝ) * Nat.card A ^ (-1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ) := by
-      positivity
-    have T := mul_le_mul_of_nonneg_left ((Z1.trans Z2).trans Z3) this
-    convert T using 1 <;> rpow_ring <;> norm_num
+  have Z3 :
+      (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ) ≤ (K ^ (13/2 : ℝ) * Nat.card A ^ (1/2 : ℝ) *
+        Nat.card H ^ (-1/2 : ℝ)) * Nat.card ↑(A ∩ (↑H + {x₀})) := by
+    calc
+      (Nat.card (A + A ∩ (↑H + {x₀})) : ℝ)
+      _ ≤ Nat.card (A + A) := by
+        gcongr; exact Nat.card_mono (toFinite _) <| add_subset_add_left inter_subset_left
+      _ ≤ K * Nat.card A := hA
+      _ = (K ^ (13/2 : ℝ) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ)) *
+          (K ^ (-11/2 : ℝ) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (1/2 : ℝ)) := by
+        rpow_ring; norm_num
+      _ ≤ (K ^ (13/2 : ℝ) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (-1/2 : ℝ)) *
+        Nat.card ↑(A ∩ (↑H + {x₀})) := by gcongr
+  obtain ⟨u, huA, hucard, hAu, -⟩ :=
+    Set.ruzsa_covering_add (toFinite A) (toFinite (A ∩ ((H + {x₀} : Set G)))) Hne (by convert Z3)
   have A_subset_uH : A ⊆ u + H := by
-    rw [add_sub_assoc] at Au
-    refine Au.trans $ add_subset_add_left $
+    refine hAu.trans $ add_subset_add_left $
       (sub_subset_sub (inter_subset_right ..) (inter_subset_right ..)).trans ?_
     rw [add_sub_add_comm, singleton_sub_singleton, sub_self]
     simp
-  exact ⟨H, u, Iu, IHA, IAH, A_subset_uH⟩
+  exact ⟨H, u, hucard, IHA, IAH, A_subset_uH⟩
 
 /-- The polynomial Freiman-Ruzsa (PFR) conjecture: if `A` is a subset of an elementary abelian
 2-group of doubling constant at most `K`, then `A` can be covered by at most `2 * K ^ 12` cosets of