Update thread!

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Hi everyone! The project is now quite active with a lot of parallel advances going on, so I thought it would be good to have a thread where people update the rest of the group on where they are at.

I'll start the ball rolling and then others can chime in. The blueprint is now in pretty good shape, with all the main steps described more or less completely in LaTeX, and formulated as statements in Lean. The bubbles are mostly green and blue! There are two key definitions that need to be formalized, https://teorth.github.io/pfr/blueprint/sect0003.html#cond-dist-def and https://teorth.github.io/pfr/blueprint/sect0002.html#uniform-def , but I think some of the participants are close to this goal (maybe they can report in on this thread).

Right now I'm working on formalizing the proof of https://teorth.github.io/pfr/blueprint/sect0003.html#kv , which is a very typical application of the "entropic Ruzsa calculus" that will be needed to fill in most of the other remaining blue bubbles. I've been able to successfully use many of the tools (e.g., submodularity) that have already been developed to achieve this, and am only running into some very minor technical issues (mostly involving how to handle vectors such as ![X,Y,Z]) that I hope to resolve soon. When I do, I'll open a separate thread to deconstruct the proof: what I have now is definitely clunky, and figuring out how to do this smoothly will facilitate the dozen or so other similar calculations that will be needed elsewhere. One of the ingredients was how to easily verify entropy identities such as H[⟨⟨X, Y⟩, Z⟩; μ] = H[⟨X, ⟨Z, X + (Y + Z)⟩⟩; μ] without a lot of "Rubik's cube" type chaining together of a half-dozen lemmas in a rw; I think I arrived at a somewhat workable solution to that following https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/.40simp.20lemmas.20for.20entropy.20of.20sums.3F/near/403088157 , but there could be a better way still.

Anyway, that's my update. What else has been going on?

[Rémy Degenne]

For the Ruzsa distance, I've made a measure and a kernel definition at https://github.com/RemyDegenne/pfr/blob/master/PFR/Entropy/KernelRuzsa.lean . I have not specialized it yet to get the conditional distance, nor have I proved any properties of it. This is the thing I am investigating now.
Apart from that, everything I've done was merged to master (a minute ago for the last part).

[Sebastien Gouezel]

I've changed the main part of the argument to use [MeasureSpace] instead of [MeasurableSpace] variables, so that the measure is always called ℙ and can be hidden from most notations. It went very smoothly, and now formulas are slightly more readable.

I've also worked on the compactness of the space of probability measures, and reformulated a little bit the existence of minimizers of the tau functional in terms of random variables (although the existence will be done using measures). All this has already been merged. To complete the existence of minimizers, we need continuity statements for entropy and Rusza distance, which @Kalle Kytölä is working on if I understand correctly.

[Kalle Kytölä]

Yes, sorry, I got distracted from the continuity --- by considerations of the spelling of uniformity of probability measures :sweat_smile:.

Thanks for phrasing tau_min_exists_measure in terms of the measures, @Sebastien Gouezel! That makes this a lot easier. I think just [MeasurableSingletonClass G] needs to be added in hypotheses, to get to use your compactness proof.

The main remaining thing for tau_min_exists_measure is continuous_tau_restrict_probabilityMeasure, for which I added the statement. The proof requires measure-spellings of Rusza distance and entropies, but the basic case (to which things should essentially reduce) of the continuity of the entropy in terms of measures exists in FiniteMeasureFintype.lean: it is continuous_measureEntropy_probabilityMeasure.

[Kalle Kytölä]

The continuity / existence of tau minimizer proofs are essentially done, except:

• There are two "funny" type class instance inference sorryes in tau_min_exists_measure.
• There is one sorry in continuous_rdist_restrict_probabilityMeasure, which requires API about products of ProbabilityMeasures, and especially the fact that taking products is continuous in the topology of convergence in distribution. (The same sorry also needs docs#MeasureTheory.ProbabilityMeasure.continuous_map, which fortunately exists since September.)

The API in the second point should definitely go to Mathlib, too. I'd be happy to work on it, although I'm not sure I'd get anything done before the weekend.

[Kalle Kytölä]

And I kind of wanted to say something about the spelling of uniformity of a probability measure.

I was not super happy about the spelling with PMFs, although docs#PMF.uniformOfFinset is in principle an option (it would be specific to discrete uniform distributions anyway and seems to moreover require countability of the underlying space).

I think prefer a version via Jason KY.'s docs#MeasureTheory.pdf.IsUniform, although I haven't carried out the necessary testing to be totally sure yet...

For this PFR project only discrete uniform measures on finite sets are needed. If the preference is to get things done rather than wait for the best or most general way to write this mathematical triviality, that would also make sense... So while I still plan to do some testing on my own, I don't want to claim uniform measures (not before the weekend, at least). There is a tiny bit of messy testing in the file FiniteMeasureFintype.lean, if that helps someone else make a choice of spelling.

[Kalle Kytölä]

By the way, I'm of course super excited about the project in general, and specifically because it is leading to so much development and improvements in probability in particular!

(Just a mixed feeling, since in doing that it is revealing so many things that are not yet what they should be in Mathlib...)

[Terence Tao]

Kalle Kytölä said:

And I kind of wanted to say something about the spelling of uniformity of a probability measure.

I was not super happy about the spelling with PMFs, although docs#PMF.uniformOfFinset is in principle an option (it would be specific to discrete uniform distributions anyway and seems to moreover require countability of the underlying space).

I think prefer a version via Jason KY.'s docs#MeasureTheory.pdf.IsUniform, although I haven't carried out the necessary testing to be totally sure yet...

For this PFR project only discrete uniform measures on finite sets are needed. If the preference is to get things done rather than wait for the best or most general way to write this mathematical triviality, that would also make sense... So while I still plan to do some testing on my own, I don't want to claim uniform measures (not before the weekend, at least). There is a tiny bit of messy testing in the file FiniteMeasureFintype.lean, if that helps someone else make a choice of spelling.

For the purposes of the project, I think the main things that are needed are to be able to use the lemmas exists_uniform, prob_of_uniform_of_in, prob_of_uniform_of_not_in, and entropy_of_uniform. If you feel confident that your final version of isUniform would be compatible with these four lemmas, then it would be possible to develop a definition of uniform distribution independently for the rest of the project, since I believe these four lemmas can be used as black boxes for everything else.

[Side note: is it possible to combine URLs with backtick notation in Zulip?]

[Eric Rodriguez]

Zulip has the capability to setup linkifiers such as docs#Nat, which could definitely be done for this project (cc @Mario Carneiro maybe?) but they won't have the monospace formatting. Alternatively you could do backticks and a unicode link like test, written as:

[`test`](example.com)

[Mario Carneiro]

pfr#ProbabilityTheory.prob_of_uniform_of_in

[Jonas Bayer]

Hello everyone! I'd like to get started on the project and wondered if there is any lemma in particular that could be suitable for this purpose. My formalization experience is mainly in Isabelle, but I've used Lean as a functional programming language before and would like to gain more experience formalizing in Lean as well. My mathematical background is in probability theory so I think this project could be an ideal start for this.

[Terence Tao]

Jonas Bayer said:

Hello everyone! I'd like to get started on the project and wondered if there is any lemma in particular that could be suitable for this purpose. My formalization experience is mainly in Isabelle, but I've used Lean as a functional programming language before and would like to gain more experience formalizing in Lean as well. My mathematical background is in probability theory so I think this project could be an ideal start for this.

Welcome Jonas! Here are some lemmas that should have fairly short and doable proofs, and which I don't think anyone else is claiming right now: you (or anyone else) are welcome to claim one or more of them to work on.

1. Bounded entropy implies concentration. This should follow from a pigeonhole principle argument and the monotonicity of the logarithm. It may help to take contrapositives (using contrapose!) in which case one should be able to use either the tactic gcongr or finite set sum monotonicity laws (e.g., docs#Finset.sum_le_sum ) together with basic properties of the logarithm or exponential. Claimed by @Jonas Bayer
2. Entropy of conditionally independent variables. This should follow by routine algebra from the indicated lemmas in the proofs. (One of these lemmas is still not yet proven, but that does not affect the task of locally proving this lemma.) Established by @Mauricio Collares
3. Distance controls entropy difference This should follow from the indicated lemmas by routine manipulation of inequalities (and the properties of the absolute value). Established by @Arend Mellendijk
4. Distance controls entropy growth Similar to previous lemma. Established by @Arend Mellendijk
5. Comparison of Ruzsa distances, II Although this is a moderately complex statement, its deduction from previous lemmas should be straightforward. Established by @Mantas Baksys
6. General 100% inverse theorem Similar to previous lemma: the complete proof here is rather tricky, but the deduction from the previous lemma (Symmetric 100% inverse theorem) and the [Ruzsa triangle inequality] (https://teorth.github.io/pfr/blueprint/sect0003.html#ruzsa-triangle) should be straightforward. Established by @Sebastien Gouezel

Note: many of the statements are missing some basic hypotheses, such as measurability, or that the measure is a probability measure. Part of the task of formalizing is to determine the necessary side conditions that need to be inserted into the statement.

Slightly more ambitious:

1. Comparison of Ruzsa distances, I Here the one tricky thing is the need to introduce independent copies at the beginning of the argument. It may help to split this lemma into two, one establishing the independent case, and the other deducing the general case from the independent case. Established by @Floris van Doorn
2. General fibring identity This will be an application of a large number of the entropic Ruzsa calculus lemmas, a bit similar to how the Kaimonovich-Vershik lemma is proven for instance, or the improved Ruzsa triangle inequality.
3. Special case of Fibring identity Again, mostly a large number of applications of preceding entropy identities.
4. Relating conditional Ruzsa distance to Ruzsa distance Again the one tricky thing is to first set up independent copies (we have a lemma for this, though) Claimed (and partially completed) by @Ben Eltschig
5. Entropy version of PFR Although this is one of the main theorems in the project, deriving it from previous propositions is actually rather short; the main issue is conceptually understanding what this result, and its predecessor results, mean. Established by @Arend Mellendijk

Other claims, for the record:

1. @Sebastien Gouezel established Symmetric 100% inverse theorem
2. @Yaël Dillies and @Bhavik Mehta claim Entropic Balog-Szemeredi-Gowers
3. @Kalle Kytölä claims what is left to prove for tau has a minimizer
4. @Rémy Degenne claims (I think?) conditioned Ruzsa distance
5. @Paul Lezeau established Ruzsa triangle inequality

And feel free to ask questions about Lean while formalizing, everyone here is very helpful and responsive!

[Sebastien Gouezel]

I'd like to claim the 100% version of PFR, i.e. if d[X, X]=0 then X is uniform on a translate of a subgroup (Lemma 4.1), unless someone is working on it. Tell me if it's the case, so that we don't waste efforts!

[Jonas Bayer]

Thanks a lot for this detailed list! I had a look at the very first one and would like to claim it (others to follow, potentially). So I just forked the repository and tried to lake build, but there seems to be an issue with Entropy/MeasureCompProb.lean. Probably these lemmas have been included in Mathlib already; deleting them solved the issue.

[Floris van Doorn]

I'm working on Comparison of Ruzsa distances, I.

[Floris van Doorn]

Jonas, I have no errors in that file on the current version...

[Floris van Doorn]

Did you run lake update(which you generally shouldn't do)?

[Jonas Bayer]

Yes, I did run it and now that you mention it, it makes sense why that could lead to problems. So the safe thing to do is to get the cache using the GUI button "Fetch Mathlib Build Cache"?

[Patrick Massot]

If you haven't started editing the project then you should use the menu item that allows to download a project. It should then get the cache for you.

[Terence Tao]

Sebastien Gouezel said:

I'd like to claim the 100% version of PFR, i.e. if d[X, X]=0 then X is uniform on a translate of a subgroup (Lemma 4.1), unless someone is working on it. Tell me if it's the case, so that we don't waste efforts!

Ah, good! I was just in the process of trying to break up this proof into simpler lemmas to encourage someone to work on this component. I just pushed a proof outline to github but it may take a while for the docs to update; in the meantime the raw LaTeX of the sketch is at https://github.com/teorth/pfr/blob/master/blueprint/src/chapter/100_percent.tex and some stubs for the file are at https://github.com/teorth/pfr/blob/master/PFR/HundredPercent.lean . It's not the only way to proceed but I think this way may be slightly simpler than the previous version I proposed.

[Floris van Doorn]

Floris van Doorn said:

I'm working on Comparison of Ruzsa distances, I.

I finished half of the lemma: #53. See the PR for some remarks.

[Terence Tao]

Floris van Doorn said:

Floris van Doorn said:

I'm working on Comparison of Ruzsa distances, I.

I finished half of the lemma: #53. See the PR for some remarks.

Thanks for this! I think you're right that the characteristic 2 hypothesis is required, I will update the blueprint to reflect this. [EDIT: This is actually also a typo in the paper, see Lemma 5.2 of https://arxiv.org/pdf/2311.05762.pdf . I will also inform my coauthors!]

The fact that the probability spaces are now required to lie in the same universe is a weird little quirk, but I'm sure we can live with it for our application. Maybe there is an elegant workaround.

The fact that setting up three independent copies was so difficult is slightly worrying, since for the main argument one needs to set up four independent random variables (all with the same codomain, fortunately). Can you talk a bit more about exactly what made it painful? Again there might be workarounds.

[Floris van Doorn]

We can get rid of the universe requirement by lifting all probability spaces to the same universe level using ULift, but that will require proving a bunch of annoying little lemmas about how ULift interacts with iIndepFun (and other things).

The reason that setting up 3 independent random variables was painful, since it's painful to define dependent functions (i : Fin 3 ) -> X i. You can do it by repeatedly applying docs#Fin.cases or docs#Fin.cons (which are the same definition), but it doesn't look very nice. Also the tactic fin_cases doesn't support constructing data, only proving propositions. You can see a partial attempt that I removed in this commit
What I did was quickly define an inductive type Triple with 3 elements, so that I can use Triple.rec to define function (i : Triple) -> X i and prove things about them using induction. Since I still want that ![X₁', X₂', X₃'] are independent in the conclusion, I defined and used the equivalence Triple ≃ Fin 3.

Doing it again with 4 will not be bad at all, you can just copy-paste the version for 3 variables and adapt it a bit. It's not the most elegant solution, but it will work.

[Terence Tao]

OK. So I guess for the short-term goal of getting PFR formalized, we will be okay, we can adapt what you did to create a custom version of independent_copies for two, three, and four variables (where in the latter two cases we also assume the codomains are all the same) and this is enough for our application. (It's also possible to painstakingly concatenate the two-independent-copies lemma together to create a three and four-independent copies lemma with some additional independence lemmas (e.g., if <X,Y> is independent of Z, and X is independent of Y, then X, Y, Z are jointly independent), but this is even less elegant, i think.)

Going beyond our project, I wonder if there is some way to build notation that can easily construct (using some analogue of matrix vector notation) a dependent type (i : Fin n) -> X i for small values of n without having to go through this sort of workaround. Hopefully it's not a fundamental limitation of Lean's parser to be unable to handle this level of dependency in the types.

In any event, the lemma independent_copies3_nondep you already proved will be useful for many of the other Ruzsa calculus bounds that are still outstanding, such as the Ruzsa triangle inequality.

[Shreyas Srinivas]

Why not use a vector here?

[Terence Tao]

I think the problem is that one can't build a vector ![ Ω₁, Ω₂, Ω₃ ] of three different probability spaces Ω₁, Ω₂ Ω₃, because they are not necessarily all of the same type. Nor can one build a vector ![ X₁, X₂, X₃ ] of three different random variables X₁: Ω₁ → G, X₂: Ω₂ → G X₃: Ω₃ → G, for the same reason, with the situation even worse if the random variables have different codomains. The solution should be to build some more flexible vector construct that can iterate to arbitrary length in a way that Lean can parse, but I'm struggling to figure out how to do this.

[Shreyas Srinivas]

You want a heterogenous list. These are not easy to build and work with.

[Shreyas Srinivas]

Something like this (very roughly):

inductive HetList : List Type → Type 1
| HNil : HetList []
| HCons {α : Type} : (x : α) → (xs : HetList αs) → HetList (α :: αs)

open HetList
example : HetList [Nat, Bool, Nat] := HCons 1 (HCons true (HCons 3 HNil))

I am certain some list like notation can be created for this.

[Shreyas Srinivas]

The difficulties start arising when you want to extract elements from this list.

[Shreyas Srinivas]

I came up with a brief demo to show where the difficulties arise)

[Adam Topaz]

Your demo isn't loading for me for some reason... is the code long, can you just post it here?

[Shreyas Srinivas]

Code

import Mathlib

inductive NEList (α : Type u)
| NEOne (x : α) : NEList α
| NECons (x : α) (xs : NEList α) : NEList α
open NEList

def nlength (l : NEList α) : ℕ :=
  match l with
  | NEOne _ => 1
  | NECons _ xs => 1 + nlength (xs)


def nhead (ls : NEList α) : α  :=
  match ls with
  | NEOne x => x
  | NECons x _ => x

def NEget (l : NEList α) (n : Nat) (h : n ≤ nlength l) : α :=
  match l with
  | NEOne x => x
  | NECons x xs => match hn : n with
      | 0 => x
      | n' + 1 =>
          have h' : n' ≤ nlength xs := by
            rw [←Nat.add_one] at hn
            unfold nlength at h
            linarith [h]
          NEget xs n' h'



inductive HetList : NEList Type → Type 1
| HOne (x : α) : HetList (NEOne α)
| HCons {α : Type} : (x : α) → (xs : HetList αs) → HetList (NECons α αs)
open HetList

example : HetList (NECons Nat (NECons Bool (NEOne Nat))) := HCons 1 (HCons true (HOne 3))

def hhead (h : HetList tl) : nhead tl:=
  match h with
  | HOne x => x
  | HCons x xs => x


def hLength (l : HetList α) : ℕ :=
  match l with
  | HOne _ => 1
  | HCons _ xs => 1 + hLength xs


-- incomplete
def hget {tl : NEList Type} (v : HetList tl) (i : ℕ) (h : i ≤ nlength tl)  : (NEget tl i (by exact h)) :=
  match hv : v with
  | HOne x => x -- dependent type hell
  | HCons x xs =>
      match hi : i with
      | 0 => x
      | i' + 1 =>
          have h' := by
            sorry
          hget v (i-1) h'



def HetVector n (tl : NEList Type) := {x : HetList tl // hLength x = n}

[Shreyas Srinivas]

Is there a way to make the message a collapsible code block?

[Adam Topaz]

use spoilers... as in

code

lean code.

[Adam Topaz]

Click the three dots and "view source" to see how I made that.

[Shreyas Srinivas]

done. The key thing I wanted to show is the dependent type hell in hget. I am guessing there is some (congr based?) fix, which isn't easy on the eye.

[Ben Eltschig]

I filled in condDist_le / the first variant of Lemma 3.22; see #54. I can try doing the other variant too tomorrow, but don't yet quite see how it follows from the first.

[Terence Tao]

Ben Eltschig said:

I filled in condDist_le / the first variant of Lemma 3.22; see #54. I can try doing the other variant too tomorrow, but don't yet quite see how it follows from the first.

Well there are basically two options here; one is to introduce some constant random variable like 0 and show that $latex d[X|0;Y|W] = d[X;Y|W]$ and $I[X:0]=0$; or else just redo the whole proof deleting various terms. The latter may end up being the path of least resistance (though a lemma that constant random variables have zero entropy and zero mutual information is potentially a useful @simp lemma or something if the entropy stuff ends up being repurposed for mathlib).

For the identDistrib stuff, shouldn't both lemmas follow rather quickly from docs#ProbabilityTheory.IdentDistrib.comp?

[Kyle Miller]

@Floris van Doorn I'm only loosely following this thread, but rather than Triple, could you define a custom induction lemma for Fin 3?

Not sure if it's useful at all, but I was messing around with defining a version of Fin that still lets you sort of automate proofs using the built-in induction principle.

code

import Mathlib.Data.Set.Finite

def Fin' : Nat → Type
  | 0 => Empty
  | n + 1 => Unit ⊕ Fin' n

instance (n k : Nat) [OfNat (Fin' n) k] : OfNat (Fin' (n + 1)) k where
  ofNat := .inr <| (OfNat.ofNat k : Fin' n)

instance (n : Nat) : OfNat (Fin' (n + 1)) n where
  ofNat := .inl ()

def α : Fin' 3 → Type
  | 0 => Fin 2
  | 1 => Fin 3
  | 2 => Fin 4

example (i : Fin' 3) : Finite (α i) := by
  obtain _ | i := i
  repeat
    dsimp [α]; infer_instance
    try obtain _ | i := i

[Adam Topaz]

@Kyle Miller You could alternatively define Fin' as an inductive family as follows:

inductive Fin' : Nat → Type where
  | zero {n} : Fin' (n+1)
  | succ {n} : Fin' n → Fin' (n+1)

which would allow you to easily use induction as well.

[Paul Lezeau]

Terence Tao said:

Floris van Doorn said:

Floris van Doorn said:

I'm working on Comparison of Ruzsa distances, I.

I finished half of the lemma: #53. See the PR for some remarks.

Thanks for this! I think you're right that the characteristic 2 hypothesis is required, I will update the blueprint to reflect this. [EDIT: This is actually also a typo in the paper, see Lemma 5.2 of https://arxiv.org/pdf/2311.05762.pdf . I will also inform my coauthors!]

The fact that the probability spaces are now required to lie in the same universe is a weird little quirk, but I'm sure we can live with it for our application. Maybe there is an elegant workaround.

The fact that setting up three independent copies was so difficult is slightly worrying, since for the main argument one needs to set up four independent random variables (all with the same codomain, fortunately). Can you talk a bit more about exactly what made it painful? Again there might be workarounds.

A bit late to the conversation, but I'd been having some trouble with setting up the same type of thing in the proof I'm currently working on, and also came to the conclusion that a 3 variable version of independent_copies was probably the easiest way to go

[Paul Lezeau]

The current version I have of this proof uses the general version of independent_copies, but is rather painful and sorry I haven't fully figured out yet (something to do with Lean not parsing an instance correctly)

[Terence Tao]

Paul Lezeau said:

The current version I have of this proof uses the general version of independent_copies, but is rather painful and sorry I haven't fully figured out yet (something to do with Lean not parsing an instance correctly)

Would you be able to use the new lemma pfr#ProbabilityTheory.independent_copies3_nondep that Floris proved as a substitute?

[Paul Lezeau]

Terence Tao said:

Paul Lezeau said:

The current version I have of this proof uses the general version of independent_copies, but is rather painful and sorry I haven't fully figured out yet (something to do with Lean not parsing an instance correctly)

Would you be able to use the new lemma pfr#ProbabilityTheory.independent_copies3_nondep that Floris proved as a substitute?

Sure! I tried that out at some point and I think I still have a copy of that code locally.

[Paul Lezeau]

This makes it a lot easier!

[Shreyas Srinivas]

@Adam Topaz : isn't that Fin2?

[Floris van Doorn]

Kyle Miller said:

Floris van Doorn I'm only loosely following this thread, but rather than Triple, could you define a custom induction lemma for Fin 3?

Not sure if it's useful at all, but I was messing around with defining a version of Fin that still lets you sort of automate proofs using the built-in induction principle.

Actually, I tried again, and working directly with Fin 3 also works. It's a little more verbose to construct a dependent function by giving the 3 function values, but it works fine.

code

/- This is neither `Fin.elim0` nor `Fin.elim0'` -/
def Fin.rec0 {α : Fin 0 → Sort*} (i : Fin 0) : α i := absurd i.2 (Nat.not_lt_zero _)

lemma independent_copies3_nondep {S : Type u}
    [mS : MeasurableSpace S]
    {Ω₁ Ω₂ Ω₃ : Type v}
    [mΩ₁ : MeasurableSpace Ω₁] [mΩ₂ : MeasurableSpace Ω₂] [mΩ₃ : MeasurableSpace Ω₃]
    {X₁ : Ω₁ → S} {X₂ : Ω₂ → S} {X₃ : Ω₃ → S}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃) :
    ∃ (A : Type (max u v)) (mA : MeasurableSpace A) (μA : Measure A)
      (X₁' X₂' X₃' : A → S),
    IsProbabilityMeasure μA ∧
    (iIndepFun (fun _ ↦ mS) ![X₁', X₂', X₃'] μA) ∧
      Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧
      IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ := by
  let Ω : Fin 3 → Type v := ![Ω₁, Ω₂, Ω₃]
  let mΩ : (i : Fin 3) → MeasurableSpace (Ω i) :=
    Fin.cons mΩ₁ <| Fin.cons mΩ₂ <| Fin.cons mΩ₃ Fin.rec0
  let X : (i : Fin 3) → Ω i → S := Fin.cons X₁ <| Fin.cons X₂ <| Fin.cons X₃ Fin.rec0
  have hX : ∀ (i : Fin 3), @Measurable _ _ (mΩ i) mS (X i) :=
    Fin.cases hX₁ <| Fin.cases hX₂ <| Fin.cases hX₃ Fin.rec0
    -- by intro i; fin_cases i <;> (dsimp; assumption)
  let μ : (i : Fin 3) → @Measure (Ω i) (mΩ i) := Fin.cons μ₁ <| Fin.cons μ₂ <| Fin.cons μ₃ Fin.rec0
  obtain ⟨A, mA, μA, X', hμ, hi, hX'⟩ := independent_copies' (mS := fun _ ↦ mS) (mΩ := mΩ) X hX μ
  refine ⟨A, mA, μA, X' 0, X' 1, X' 2, hμ, ?_,
    (hX' 0).1, (hX' 1).1, (hX' 2).1,
    (hX' 0).2, (hX' 1).2, (hX' 2).2⟩
  convert hi; ext i; fin_cases i <;> rfl

[Floris van Doorn]

Proving the version with three different codomains for the random variables is not harder (however, stating it is harder)

code

/- This is neither `Fin.elim0` nor `Fin.elim0'` -/
def Fin.rec0 {α : Fin 0 → Sort*} (i : Fin 0) : α i := absurd i.2 (Nat.not_lt_zero _)

/-- A version with exactly 3 random variables that have the same codomain.
It's unfortunately incredibly painful to prove this from the general case. -/
lemma independent_copies3 {S₁ S₂ S₃ : Type u}
    [mS₁ : MeasurableSpace S₁] [mS₂ : MeasurableSpace S₂] [mS₃ : MeasurableSpace S₃]
    {Ω₁ Ω₂ Ω₃ : Type v}
    [mΩ₁ : MeasurableSpace Ω₁] [mΩ₂ : MeasurableSpace Ω₂] [mΩ₃ : MeasurableSpace Ω₃]
    {X₁ : Ω₁ → S₁} {X₂ : Ω₂ → S₂} {X₃ : Ω₃ → S₃}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃) :
    let S : Fin 3 → Type u := ![S₁, S₂, S₃]
    let mS : (i : Fin 3) → MeasurableSpace (S i) :=
      Fin.cases mS₁ <| Fin.cases mS₂ <| Fin.cases mS₃ Fin.rec0
    ∃ (A : Type (max u v)) (mA : MeasurableSpace A) (μA : Measure A)
      (X₁' : A → S₁) (X₂' : A → S₂) (X₃' : A → S₃),
    let X' : (i : Fin 3) → A → S i := Fin.cases X₁' <| Fin.cases X₂' <| Fin.cases X₃' Fin.rec0
    IsProbabilityMeasure μA ∧
    iIndepFun mS X' μA ∧
      Measurable X₁' ∧ Measurable X₂' ∧ Measurable X₃' ∧
      IdentDistrib X₁' X₁ μA μ₁ ∧ IdentDistrib X₂' X₂ μA μ₂ ∧ IdentDistrib X₃' X₃ μA μ₃ := by
  intro S mS
  let Ω : Fin 3 → Type v := ![Ω₁, Ω₂, Ω₃]
  let mΩ : (i : Fin 3) → MeasurableSpace (Ω i) :=
    Fin.cases mΩ₁ <| Fin.cases mΩ₂ <| Fin.cases mΩ₃ Fin.rec0
  let X : (i : Fin 3) → Ω i → S i := Fin.cases X₁ <| Fin.cases X₂ <| Fin.cases X₃ Fin.rec0
  have hX : ∀ (i : Fin 3), Measurable (X i) :=
    Fin.cases hX₁ <| Fin.cases hX₂ <| Fin.cases hX₃ Fin.rec0
  let μ : (i : Fin 3) → Measure (Ω i) :=
    Fin.cases μ₁ <| Fin.cases μ₂ <| Fin.cases μ₃ Fin.rec0
  obtain ⟨A, mA, μA, X', hμ, hi, hX'⟩ := independent_copies' X hX μ
  refine ⟨A, mA, μA, X' 0, X' 1, X' 2, hμ, ?_,
    (hX' 0).1, (hX' 1).1, (hX' 2).1,
    (hX' 0).2, (hX' 1).2, (hX' 2).2⟩
  convert hi; ext i; fin_cases i <;> rfl

However, this version is not "better", since it's still painful to get the 'non-dependent' version from this (where the codomain is S for each random variable). The reason is that the latter is stated using the type family (fun _ : Fin 3 ↦ S) with measurable space structure (fun _ : Fin 3 ↦ mS), and the former is stated using the type family ![S, S, S] with measurable space structure Fin.cases mS <| Fin.cases mS <| Fin.cases mS Fin.rec0. Those are equal (or heterogeneously equal in the second case), but not definitionally so, which makes it easier to just prove the non-depedent version directly.

[Sebastien Gouezel]

Sebastien Gouezel said:

I'd like to claim the 100% version of PFR, i.e. if d[X, X]=0 then X is uniform on a translate of a subgroup (Lemma 4.1), unless someone is working on it. Tell me if it's the case, so that we don't waste efforts!

Completed at https://github.com/teorth/pfr/pull/56

[Floris van Doorn]

I finished Lemma 3.23

[Rémy Degenne]

I just finished proving the improved triangle inequality for the kernel version of the Ruzsa distance, because I thought we needed it for the conditional distance, but now I don't see it in the blueprint. I will make a pr with this and the definitions of the conditional distances in a few hours (I am now boarding a plane).

[Aaron Anderson]

(deleted)

[Paul Lezeau]

Is anyone currently working on Comparison of Ruzsa distances, II (Lemma 3.24)? If not I'd like to claim it.

[Arend Mellendijk]

I've done the final argument of the entropy version of PFR.

Nothing terribly exciting, as expected, but I did discover one very minor typo in the original paper.

[Terence Tao]

Paul Lezeau said:

Is anyone currently working on Comparison of Ruzsa distances, II (Lemma 3.24)? If not I'd like to claim it.

I'm not aware of any competing claims, so I've marked your claim on my previous post tracking these things. (I will probably have to send out an updated version soon, as most of the ones on this list are now already done.)

[Terence Tao]

Terence Tao said:

Paul Lezeau said:

Is anyone currently working on Comparison of Ruzsa distances, II (Lemma 3.24)? If not I'd like to claim it.

I'm not aware of any competing claims, so I've marked your claim on my previous post tracking these things. (I will probably have to send out an updated version soon, as most of the ones on this list are now already done.)

Actually... in the last few minutes I got a PR from @Mantas Baksys that establishes this lemma. Sorry for the duplication of effort!

[Mantas Baksys]

Hi everyone! I would also like to join this amazing formalization project and as my first contribution, I've proved Lemma 3.24. I didn't see @Paul Lezeau's message claiming to prove it in time and already messaged him to apologise (thankfully Paul hadn't started working on it).

[Paul Lezeau]

No worries at all!
@Terence Tao Are there any similar lemmas I could work on that haven't been claimed yet?

[Terence Tao]

Paul Lezeau said:

No worries at all!
Terence Tao Are there any similar lemmas I could work on that haven't been claimed yet?

I'm in a meeting right now, but I'll make a new post in an hour or so with a new set of outstanding lemmas to prove.

[Kevin Buzzard]

@Paul Lezeau aren't you supposed to be formalising stacks as part of your computing project? ;-)

[Yaël Dillies]

Advisors should be forbidden from reading Zulip :stuck_out_tongue:

[Paul Lezeau]

Kevin Buzzard said:

Paul Lezeau aren't you supposed to be formalising stacks as part of your computing project? ;-)

That is a good point - hopefully we should be done by tomorrow-ish! ;)

[Rémy Degenne]

Rémy Degenne said:

I just finished proving the improved triangle inequality for the kernel version of the Ruzsa distance, because I thought we needed it for the conditional distance, but now I don't see it in the blueprint. I will make a pr with this and the definitions of the conditional distances in a few hours (I am now boarding a plane).

PR: https://github.com/teorth/pfr/pull/63