Balog-Szemerédi-Gowers

Stream: Polynomial Freiman-Ruzsa conjecture

[Yaël Dillies]

I just wrote most of the proof of entropic BSG. There's three sorries left:

• The last one is just rewriting under a sum, but I wasn't feeling like doing it
• The first two are wrong, I'm afraid. The prerequisite lemma condIndependent_copies (fun ω ↦ (A ω, B ω)) Z (hA.prod_mk hB) hZ μ gives me

AB₁ AB₂: Ω' → G × G
Z': Ω' → G
ν: Measure Ω'
left✝: IsProbabilityMeasure ν
hAB₁: Measurable AB₁
hAB₂: Measurable AB₂
hZ': Measurable Z'
hABZ: condIndepFun AB₁ AB₂ Z'
hAB₁Z: IdentDistrib (⟨AB₁, Z'⟩) (⟨fun ω ↦ (A ω, B ω), Z⟩)
hAB₂Z: IdentDistrib (⟨AB₂, Z'⟩) (⟨fun ω ↦ (A ω, B ω), Z⟩)

but nothing is ensuring that ∀ ω, (AB₁ ω).1 + (AB₁ ω).2 = (AB₂ ω).1 + (AB₂ ω).2 (A₁ + B₁ = A₂ + B₂ in the blueprint), which is what I need later in the proof.

[Yaël Dillies]

cc @Bhavik Mehta who is taking over the proof for now

[Terence Tao]

I think the way this should work is that because A ω + B ω = Z ω, one should get from hAB₁Z that (AB₁ ω).1 + (AB₁ ω).2 = Z' ω for almost all (but not all) ω, and similarly (AB₂ ω).1 + (AB₂ ω).2 = Z' ω for almost all ω, so that ∀ᵐ ω, (AB₁ ω).1 + (AB₁ ω).2 = (AB₂ ω).1 + (AB₂ ω).2, which should hopefully be enough.

[Yaël Dillies]

After a two days fight against the measure theory API...

#print axioms ent_bsg
-- 'ent_bsg' depends on axioms: [Quot.sound, propext, Classical.choice]

[Terence Tao]

Wow, it looks like we are down to just one outstanding task, for which there is already a lot of partial progress (and an outstanding PR). Well done everybody!

@Paul Lezeau and @Jonas Bayer , let us know if there is any component of the remaining task that could be done in parallel, in particular filling in a sorry for a sublemma that one knows how to use in the rest of the argument.

Concurrently with all the formalization contributions, I have added content to each of the sections of the examples file. But there may still be some illustrative examples of what was accomplished in this project that could still go in this file, so feel free to propose such contributions (either here or as PRs).

[Yaël Dillies]

For your information, I am now formalising the combinatorial version of BSG. So we could also aim for the last version of PFR you were mentioning.

[Paul Lezeau]

Terence Tao said:

Wow, it looks like we are down to just one outstanding task, for which there is already a lot of partial progress (and an outstanding PR). Well done everybody!

Paul Lezeau and Jonas Bayer , let us know if there is any component of the remaining task that could be done in parallel, in particular filling in a sorry for a sublemma that one knows how to use in the rest of the argument.

Concurrently with all the formalization contributions, I have added content to each of the sections of the examples file. But there may still be some illustrative examples of what was accomplished in this project that could still go in this file, so feel free to propose such contributions (either here or as PRs).

Sure! I think the current PR should deal with the last annoying technical issues (notably the independence proofs) so the remainder of the proof should be relatively quick!

Concerning sorries that people could help fill in, the PR adds a lemma called iIndepFun.prod which I don't think we've proven yet (although it might be best to check with @Jonas Bayer in case he has a proof locally). The other remaining sorries should be relatively easy (they are in the proof of the main result we've been working on) and I'm planning on finishing them off tomorrow (together with fixing the merge conflicts in the PR)

[Jonas Bayer]

Currently, I don't have a proof of iIndepFun.prod yet, so if someone else wants to work on that they're very welcome. I would also be interested in looking into this, but I won't be able to spend much time on it before Thursday.

[Terence Tao]

Just for reference, here is what I believe is the specification for iIndepFun.prod:

import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.IdentDistrib

open MeasureTheory ProbabilityTheory Function Set BigOperators

namespace ProbabilityTheory

variable {Ω ι ι' : Type*} [MeasurableSpace Ω] {α β : ι → Type*}
  {n : (i : ι) → MeasurableSpace (α i)}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → α i}
  {μ : Measure Ω}

variable {ST : ι' → Finset ι} (hS : Pairwise (Disjoint on ST)) in
lemma iIndepFun.prod (h : iIndepFun n f μ) :
    let β := fun k ↦ Π i : ST k, α i
    iIndepFun (β := β) (fun k ↦ MeasurableSpace.pi)
      (fun (k : ι') (x : Ω) (i : ST k) ↦ f i x) μ := by
      sorry

In principle I think this can be deduced from pfr#ProbabilityTheory.iIndepFun_iff_map_prod_eq_prod_map_map but there are some reindexing and dependent type issues. It also generalizes docs#ProbabilityTheory.iIndepFun.indepFun_finset but it is not clear to me how to get from that special case to the general case.

[Yaël Dillies]

Oh I can probably do that

[Paul Lezeau]

sum_dist_diff_le is now sorry free!

[Paul Lezeau]

(except for iIndepFun.prod of course)

[Yaël Dillies]

(still working on it)

[Rémy Degenne]

That means that iIndepFun.prod is the last sorry in the project?

[Paul Lezeau]

I think so!

[Yaël Dillies]

This lemma is pretty horrible. I think it's stated suboptimally for proving purposes. I have just merged your PR and will try to find a better statement.

[Paul Lezeau]

Yeah the independence part of the proof is rather horrendous so feel free to improve it!

[Yaël Dillies]

I think it boils down to the fact that you're using a finset-indexed collection of finsets instead of a type-indexed collection of types (namely a sigma type). Tinkering...

[Yaël Dillies]

Giving up for now. I've written three different approaches that people can try.

[Sebastien Gouezel]

I'd like to work on iIndepFun.pi', unless someone is already on it.

[Yaël Dillies]

Please do, Sébastien! I already know what lemma I'll be having nightmares about tonight...

[Terence Tao]

Yaël Dillies said:

Please do, Sébastien! I already know what lemma I'll be having nightmares about tonight...

By the way, it seems that PFR's version of ProbabilityTheory/Independence/Basic now differs (rather substantially) from Mathlib's version. Is the plan eventually to merge the two somehow?

Also, I wonder if iIndepFun.prod could be established from pfr#ProbabilityTheory.iIndepFun_iff' and docs#Finset.prod_disjiUnion EDIT: Ah, one also needs to mess around with Pi systems in order to reduce to the case of testing with rectangles and not arbitrary measurable sets. So some tool like docs#ProbabilityTheory.iIndepSets.iIndep may also be needed.

[Yaël Dillies]

Oh, sorry if that wasn't clear! Everything in file PFR.Mathlib.X.Y.Z is meant to be upstreamed to the mathlib file Mathlib.X.Y.Z. So yeah, they diverge, by definition.

[Yaël Dillies]

Yes, exactly. I got stuck because I needed to apply something like docs#MeasurableSpace.induction_on_inter through an induction on the number of elements of ι. Not very appetising.

[Yaël Dillies]

Of course our end use only requires one application of MeasurableSpace.induction_on_inter, but the general case is probably easier to prove anyway. In case, it is not, you can try proving pfr#hopelessly_specific.

[Terence Tao]

Yaël Dillies said:

Yes, exactly. I got stuck because I needed to apply something like docs#MeasurableSpace.induction_on_inter through an induction on the number of elements of ι. Not very appetising.

I see now. It does seem like one really does have to get into the bowels of measure theory if we want to prove the statement in full generality. (For our application of course we only need finite probability spaces and in the worst case we could retreat to that setting, though it would be a shame since these lemmas are certainly true and worth having in mathlib.)

I took a look at the proof of docs#ProbabilityTheory.kernel.iIndepFun.indepFun_finset (which would cover the special case of breaking up into two disjoint families rather than finitely many) and it does indeed go through a lot of Pi system machinery. So this looks sort of inevitable that one has to do something similar here (but perhaps we can reuse some of the subresults proved there?)

[Terence Tao]

I was able to get somewhere with iIndepFun.prod but I don't want to touch endgame.lean as it is giving me a lot of build errors right now and was hoping I could either hand this off to someone else or get some advice on how to do the next step. Basically I managed to adapt the pi system reduction from docs#ProbabilityTheory.kernel.iIndepFun.indepFun_finset to reduce to showing that the preimages of boxes coming from disjoint index sets are independent sets. This remaining task should be straightforward, the only issue is that I am not sufficiently good with dependent types (or classical choice) to obtain the various sets needed to describe the boxes. Basically once one can extract the analogues of the data sets_s', hs1, hs2, sets_t', ht1, ht2 that appears in the source code from docs#ProbabilityTheory.kernel.iIndepFun.indepFun_finset , I believe one can continue adapting the rest of that code to finish off the proof. [Specifically, at the sorry in the code below, I am stuck in trying to express E k (for k ∈ s) as the preimage (fun a (i : (ST k)) => f i a) ⁻¹' (Set.pi (Set.univ : Set (ST k)) (sets k) ) for some sets k ∈ Set.pi Set.univ fun i ↦ {s | MeasurableSet s}.]

import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.IdentDistrib

open MeasureTheory ProbabilityTheory Function Set BigOperators

variable {Ω ι ι' : Type*} [m: MeasurableSpace Ω] {α : ι → Type*}
  {n : (i : ι) → MeasurableSpace (α i)} {f : (i : ι) → Ω → α i}
  {μ : Measure Ω} [IsProbabilityMeasure μ] {hf : (i : ι) → Measurable (f i)}

variable {ST : ι' → Finset ι} (hS : Pairwise (Disjoint on ST)) in
lemma iIndepFun.prod (h : iIndepFun n f μ) :
    let β := fun k ↦ Π i : ST k, α i
    iIndepFun (β := β) (fun k ↦ MeasurableSpace.pi)
      (fun (k : ι') (x : Ω) (i : ST k) ↦ f i x) μ := by
      set F := fun (k : ι') (x : Ω) (i : ST k) ↦ f i x
      set M := fun (k : ι') ↦ MeasurableSpace.pi (m := fun (i: ST k) ↦ n i)
      rw [ProbabilityTheory.iIndepFun_iff_iIndep]
      let πβ (k : ι') := Set.pi (Set.univ : Set (ST k)) ''
    Set.pi (Set.univ : Set (ST k)) fun i => { s : Set (α i) | MeasurableSet[n i] s }
      let π (k : ι') : Set (Set Ω) := { s : Set Ω | ∃ t ∈ (πβ k), (fun a (i : (ST k)) => f i a) ⁻¹' t = s }
      apply ProbabilityTheory.iIndepSets.iIndep (π := π)
      . intro k
        rw [<-measurable_iff_comap_le, measurable_pi_iff]
        intro i
        exact hf i
      . intro k
        apply IsPiSystem.comap
        apply isPiSystem_pi
      . intro k
        have : M k = MeasurableSpace.generateFrom (πβ k) :=  generateFrom_pi.symm
        rw [this, MeasurableSpace.comap_generateFrom]
        congr
      rw [iIndepSets_iff]
      intro s E hE
      sorry

[Terence Tao]

Ohh, I need to invoke the axiom of choice now. :grinning_face_with_smiling_eyes: OK, I think I'm unstuck.

[Terence Tao]

I have a (rather convoluted) proof of iIndepFun.prod (see below for a self-contained treatment) but I'm having a weird local problem in that endgame.lean is reporting a huge number of build errors and so I can't merge directly. If someone with a working build could merge this in that would be great. (Note that the code should probably go somewhere else than endgame.lean, such as Mathlib.Probability.Independence.Basic, especially since it uses the symbol "k" which was used for something else in endgame.lean. Also my set of hypotheses for iIndepFun.prod is slightly different from what it was before, so the application of this lemma in endgame.lean will also need to be tweaked.)

import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.IdentDistrib

open MeasureTheory ProbabilityTheory Function Set BigOperators

namespace ProbabilityTheory


-- The following lemma has a completely inefficient proof; should be done better

lemma exists_indexfn {ι ι': Type*} [hι': Nonempty ι'] {ST : ι' → Finset ι} (hS : Pairwise (Disjoint on ST)) : ∃ K : ι → ι', ∀ k : ι', ∀ i ∈ ST k, K i = k := by
  classical
  let inv (i : ι) : Set ι' := { k | i ∈ ST k }
  let K := fun i => if h : Set.Nonempty (inv i) then   (Classical.choice (Set.Nonempty.to_subtype h)).1 else Classical.choice hι'
  use K
  intro k i hi
  have : Set.Nonempty (inv i) :=  nonempty_of_mem hi
  simp [this]
  set k' := (Classical.choice (Set.Nonempty.to_subtype this)).1
  have : k' ∈ inv i := by
    exact Subtype.mem (Classical.choice (Nonempty.to_subtype this))
  have : i ∈ ST k' := by
    simp at this; assumption
  apply Pairwise.eq hS
  unfold Disjoint; simp
  use {i}
  simp [this, hi]

variable {Ω ι ι' : Type*} [MeasurableSpace Ω] {α : ι → Type*} [hι': Nonempty ι']
  {n : (i : ι) → MeasurableSpace (α i)} {f : (i : ι) → Ω → α i}
  {μ : Measure Ω} [IsProbabilityMeasure μ] {hf : (i : ι) → Measurable (f i)}  {ST : ι' → Finset ι} (hS : Pairwise (Disjoint on ST)) in
lemma iIndepFun.prod (h : iIndepFun n f μ) :
    let β := fun k ↦ Π i : ST k, α i
    iIndepFun (β := β) (fun k ↦ MeasurableSpace.pi)
      (fun (k : ι') (x : Ω) (i : ST k) ↦ f i x) μ := by
      set F := fun (k : ι') (x : Ω) (i : ST k) ↦ f i x
      set M := fun (k : ι') ↦ MeasurableSpace.pi (m := fun (i: ST k) ↦ n i)
      rw [iIndepFun_iff_iIndep]
      let πβ (k : ι') := Set.pi (Set.univ : Set (ST k)) ''
    Set.pi (Set.univ : Set (ST k)) fun i => { s : Set (α i) | MeasurableSet[n i] s }
      let π (k : ι') : Set (Set Ω) := { s : Set Ω | ∃ t ∈ (πβ k), (fun a (i : (ST k)) => f i a) ⁻¹' t = s }
      apply iIndepSets.iIndep (π := π)
      . intro k
        rw [<-measurable_iff_comap_le, measurable_pi_iff]
        intro i
        exact hf i
      . intro k
        apply IsPiSystem.comap
        apply isPiSystem_pi
      . intro k
        have : M k = MeasurableSpace.generateFrom (πβ k) :=  generateFrom_pi.symm
        rw [this, MeasurableSpace.comap_generateFrom]
        congr
      rw [iIndepSets_iff]
      intro s E hE
      simp at hE
      have hE' (k : s) := hE k (Finset.coe_mem k)
      classical
      obtain ⟨ sets, h_sets ⟩ := Classical.axiomOfChoice hE'
      rcases exists_indexfn hS with ⟨ K, hK ⟩
      let sets' (k : ι') (i : ι) : Set (α i) := if h : k ∈ s then (if h' : i ∈ ST k then sets ⟨k, h⟩ ⟨i, h'⟩ else Set.univ) else Set.univ
      let sets'' (i : ι) : Set (α i) := sets' (K i) i
      have box (k : ι') (hk : k ∈ s) : E k = ⋂ i ∈ ST k, (f i)⁻¹' (sets'' i) := by
        rw [<-(h_sets ⟨ k, hk ⟩).2]
        simp [hk]
        ext1 ω
        simp_rw [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
        constructor <;> intro h
        · intro i hi; rw [hK k i hi]; simp [hi, hk]; exact h ⟨ i, hi ⟩
        · intro i; have := h i; rw [hK k i.1 i.2] at this; simp [hk] at this; exact this
      suffices : μ (⋂ k ∈ s, ⋂ i ∈ ST k, (f i)⁻¹' (sets'' i) ) = ∏ k in s, μ (⋂ i ∈ ST k, (f i)⁻¹' (sets'' i))
      . convert this with k hk k hk
        all_goals {
          exact box k hk
        }
      rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
      have hS' : PairwiseDisjoint s ST := by
        intro k _ k' _ hkk'
        exact hS hkk'
      set A : Finset ι := Finset.disjiUnion s ST hS'
      have big_inter : ⋂ k ∈ s, ⋂ i ∈ ST k, (f i)⁻¹' (sets'' i) = ⋂ i ∈ A, (f i)⁻¹' (sets'' i) := by
        simp
      rw [big_inter, h A _, Finset.prod_disjiUnion]
      . apply Finset.prod_congr rfl
        intro k hk
        symm
        apply h (ST k)
        intro i hi
        have := (h_sets ⟨k, hk⟩).1 i hi
        convert this
        simp
        rw [hK k i hi]
        simp [hi, hk]
      intro i hi
      simp at hi
      rcases hi with ⟨ k, hk, hik ⟩
      simp
      rw [hK k i hik]
      simp [hk, hik]
      exact (h_sets ⟨ k, hk ⟩).1 i hik

[Terence Tao]

Actually, I think I can get my local build to compile now. Working on it...

[Johan Commelin]

Does this mean we should get the champagne ready?

[Terence Tao]

Very nearly! I just got iIndepFun.Prod to work. There is just one sorry left I think, which is to prove that the sets {0}, {1}, and {2,3} are pairwise disjoint. I tried to bash this out with fin_cases but it got very tedious, surely there is a better way?

[Johan Commelin]

Ouch, that shouldn't be hard. Do you have the formal statement?

[Johan Commelin]

Statements like Finset.disjoint_singleton_left and Finset.disjoint_singleton_right should help.

[Johan Commelin]

example : Disjoint ({0} : Set ℕ) {2,3} := by
  rw [Set.disjoint_singleton_left]
  simp

[Johan Commelin]

@Terence Tao Are these sets of natural numbers? Or real numbers? Or something else?

[Terence Tao]

Natural numbers. We need

abbrev S1 : Fin 3 → Finset (Fin 4)
  | 0 => {0}
  | 1 => {1}
  | 2 => {2, 3}

example: Pairwise (Disjoint on fun x ↦ S1 x) := by sorry

There's some slight problem with the build because I also put in some measurability conditions that now need to propagate downstream, working on that now.

[Johan Commelin]

abbrev S1 : Fin 3 → Finset (Fin 4)
  | 0 => {0}
  | 1 => {1}
  | 2 => {2, 3}

example: Pairwise (Disjoint on S1) := by
  rw [@pairwise_disjoint_on]
  intro m n h
  fin_cases m <;> fin_cases n <;> simp at h <;> decide

[Johan Commelin]

Golfed:

example: Pairwise (Disjoint on S1) := by
  rw [pairwise_disjoint_on]
  decide

[Terence Tao]

OK that worked. Just need to paste in a bunch of measurability conditions and should be done soon :fingers_crossed:

[Terence Tao]

OK I think I removed all the sorries from endgame.lean. Is there an easy way to see that there are no essential sorries in the entire project?

[Johan Commelin]

#print axioms your_theorem_name

[Johan Commelin]

You hope to see

-- 'PFR' depends on axioms: [propext, Quot.sound, Classical.choice]

or something like that.

[Terence Tao]

(Building lean files)

[Terence Tao]

image.png

[Johan Commelin]

Congratulations to all contributors!

[Yaël Dillies]

And that took quite precisely three weeks! :running:

[Rémy Degenne]

And the "Build project" CI step for the last commit is also successful, so it looks like the online version is good as well (there are still a few sorry in independence, but I guess they are the alternative approaches that were not used in the end).
All green: https://teorth.github.io/pfr/blueprint/dep_graph_document.html :)

[Sebastien Gouezel]

Yaël Dillies said:

Please do, Sébastien! I already know what lemma I'll be having nightmares about tonight...

If you want to see how it can be done, you can have a look at https://github.com/teorth/pfr/pull/131. In the end it wasn't too bad using the right pi_system lemmas.

[Yaël Dillies]

Very impressive :) I genuinely had no clue here