Copy / identically distributed

Stream: Polynomial Freiman-Ruzsa conjecture

[Kalle Kytölä]

I am not very convinced that Copy deserves a new definition: we already have docs#MeasureTheory.Measure.map, which gives the law of a random variable (and more general push-forwards of measures). Maybe the only thing I'd consider is using := by volume_tac for the Measure-argument of Measure.map, so that one can omit referring to it if one prefers to have volume as the canonical (probability) measure on the sample space.

Specifically, does "Copy" need to do anything besides the following?

import Mathlib.MeasureTheory.Measure.MeasureSpace

open MeasureTheory

def IsCopy [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace S]
    (X₁ : Ω₁ → S) (X₂ : Ω₂ → S)
    (μ₁ : Measure Ω₁ := by volume_tac) (μ₂ : Measure Ω₂ := by volume_tac) : Prop :=
  μ₁.map X₁ = μ₂.map X₂


section Test

variable [MeasureSpace Ω₁] [MeasureSpace Ω₂] [MeasurableSpace S]
variable (X₁ : Ω₁ → S) (X₂ : Ω₂ → S)

#check IsCopy X₁ X₂ -- IsCopy X₁ X₂ : Prop

end Test

[Kalle Kytölä]

We also have docs#ProbabilityTheory.IdentDistrib which does otherwise the same thing, but it further packages a.e.-measurability properties of the random variables.

[Rémy Degenne]

Indeed, IsCopy does not look very useful as a new definition, given that we already have IdentDistrib. What might be more useful though is a definition copy X, which returns a new random variable with same law as X, independent of X (and of other things passed as parameters? I am not sure and need to look at the paper to see why copy exists).

[Kalle Kytölä]

I'd tend to think that that construction is just defining binary products of probability spaces and the component maps from them. But maybe I have to understand the use cases better, too.

[Rémy Degenne]

looks like copy is defined in order to get 3.8 here: https://teorth.github.io/pfr/blueprint/sect0003.html#ruz-dist-def

[Terence Tao]

Rémy Degenne said:

looks like copy is defined in order to get 3.8 here: https://teorth.github.io/pfr/blueprint/sect0003.html#ruz-dist-def

Yeah, the main thing is to have a method (https://teorth.github.io/pfr/blueprint/sect0003.html#independent-exist) that starts with k random variables $X_1,\dots,X_k$ defined on various probability spaces $\Omega_1,\dots,\Omega_k$ and return k copies $X'_1,\dots,X'_k$ all defined on a single space $\Omega$ which are in addition jointly independent. The canonical choice would be to take $\Omega$ to be the product of the probability distribution spaces of the $X_1,\dots,X_k$ and make $X'_1,\dots,X'_k$ the coordinate maps. This construction is key to defining Ruzsa distance, and in the main argument we also require some additional copies of existing variables (and to prove the entropic Balog-Szemeredi-Gowers lemma https://teorth.github.io/pfr/blueprint/sect0003.html#lem-bsg we also need a more general conditional copy construction, https://teorth.github.io/pfr/blueprint/sect0003.html#cond-indep-exist). The precise choice of copy constructed is not important, but I guess in order to make the definition of Ruzsa distance well defined (or to avoid using Classical.Choice) we would like to have a canonical construction, and the above choice seems to be the natural one to use.

But "isCopy" is, indeed, just a synonym for μ₁.map X₁ = μ₂.map X₂ and we could just use that instead and delete it from the blueprint (or just add an informal sentence saying what we mean by a "copy" of a random variable. I don't know whether it is preferable to introduce lots of trivial wrappers like isCopy X₁ X₂ for frequently used concepts like this, or to unfold all such wrappers into existing Mathlib routines to use μ₁.map X₁ = μ₂.map X₂ instead. Happy to defer to whatever is common practice already.

[Rémy Degenne]

The Ruzsa distance is just this, no?

/-- The Ruzsa distance `dist X Y` between two random variables is defined as
$H[X'-Y'] - H[X']/2 - H[Y']/2$, where $X',Y'$ are independent copies of $X, Y$. -/
noncomputable
def dist (X : Ω → G) (Y : Ω' → G) (μ : Measure Ω := by volume_tac)
    (μ' : Measure Ω' := by volume_tac) : ℝ :=
  H[fun x ↦ x.1 - x.2 ; (μ.map X).prod (μ'.map Y)] - H[X ; μ]/2 - H[Y ; μ']/2

I'm not writing this to say that copying random variables is not useful in general though. I can also imagine that this measure based definition might not scale when conditioning, etc.

[Terence Tao]

Rémy Degenne said:

The Ruzsa distance is just this, no?

/-- The Ruzsa distance `dist X Y` between two random variables is defined as
$H[X'-Y'] - H[X']/2 - H[Y']/2$, where $X',Y'$ are independent copies of $X, Y$. -/
noncomputable
def dist [MeasurableSpace G] (X : Ω → G) (Y : Ω' → G) : ℝ :=
  H[fun x ↦ x.1 - x.2 ; (μ.map X).prod (μ'.map Y)] - H[X ; μ]/2 - H[Y ; μ']/2

Actually the proof of the triangle inequality is a good test case. Starting with three different random variables X, Y, Z on different probability spaces, one passes to the product measure (something like (μ.map X).prod ((μ'.map Y).prod (μ''.map Z)) to create three new variables (something like fun x ↦ x.1, fun x ↦ x.2.1, fun x ↦ x.2.2 with my product conventions, though I may have the dot notation slightly incorrect). One can call these variables X', Y', Z', and one can introduce some helper lemmas stating that these variables are independent and have the laws of X, Y, Z respectively. Then one can start the rest of the proof of the triangle inequality.

There is a later point in the paper where one has to work with independent copies of four different variables (see Section 6.0.2 of https://teorth.github.io/pfr/blueprint/sect0006.html), so it could be good to have a more systematic way of doing this than just working with iterated products.