The tau functional

Definition of the tau functional and basic facts

Main definitions:

• η: $1/9$
• τ: The tau functional $\tau [X_1;X_2]=d[X_1;X_2]+\eta d[X_1^0;X_1]+\eta d[X_2^0;X_2].$

Main results

• tau_minimizer_exists: A pair of random variables minimizing $\tau$ exists.
• condRuzsaDistance_ge_of_min: If $X_1,X_2$ is a tau-minimizer with $k=d[X_1;X_2]$, then $d[X_1^{\prime }|Z,X_2^{\prime }|W]$ is at least $$k-\eta (d[X_1^0;X_1^{\prime }|Z]-d[X_1^0;X_1])-\eta (d[X_2^0;X_2^{\prime }|W]-d[X_2^0;X_2])$$ for any $X_1^{\prime },Z,X_2^{\prime },W$.

structure refPackage (Ω₀₁ : Type u_1) (Ω₀₂ : Type u_2) [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] (G : Type uG) [MeasurableSpace G] : Type (max (max uG u_1) u_2)

A structure that packages all the fixed information in the main argument. In this way, when defining the τ functional, we will only only need to refer to the package once in the notation instead of stating the reference spaces, the reference measures and the reference random variables.

The η parameter has now been incorporated into the package, in preparation for being able to manipulate the package.

• X₀₁ : Ω₀₁ → G

  The first variable in a package.

• X₀₂ : Ω₀₂ → G

  The second variable in a package.

• hmeas1 : Measurable self.X₀₁
• hmeas2 : Measurable self.X₀₂
• η : ℝ

  The constant that parameterizes how good the package is. The argument only works for small enough η, typically ≤ 1/9 or < 1/8.

• hη : 0 < self.η
• hη' : 8 * self.η ≤ 1

noncomputable def tau {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω₁ : Type u_11} {Ω₂ : Type u_12} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (X₁ : Ω₁ → G) (X₂ : Ω₂ → G) (μ₁ : MeasureTheory.Measure Ω₁) (μ₂ : MeasureTheory.Measure Ω₂) : ℝ

If $X_1,X_2$ are two $G$-valued random variables, then $$\tau [X_1;X_2]:=d[X_1;X_2]+\eta d[X_1^0;X_1]+\eta d[X_2^0;X_2].$$ Here, $X_1^0$ and $X_2^0$ are two random variables fixed once and for all in most of the argument. To lighten notation, We package X^0_1 and X^0_2 in a single object named p.

We denote it as τ[X₁ ; μ₁ # X₂ ; μ₂ | p] where p is a fixed package containing the information of the reference random variables. When the measurable spaces have a canonical measure ℙ, we can use τ[X₁ # X₂ | p]

Equations

• τ[X₁ ; μ₁ # X₂ ; μ₂ | p] = d[X₁ ; μ₁ # X₂ ; μ₂] + p.η * d[p.X₀₁ ; MeasureTheory.volume # X₁ ; μ₁] + p.η * d[p.X₀₂ ; MeasureTheory.volume # X₂ ; μ₂]

def «termτ[_;_#_;_|_]».«delab_app.tau» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «termτ[_;_#_;_|_]» : Lean.ParserDescr

If $X_1,X_2$ are two $G$-valued random variables, then $$\tau [X_1;X_2]:=d[X_1;X_2]+\eta d[X_1^0;X_1]+\eta d[X_2^0;X_2].$$ Here, $X_1^0$ and $X_2^0$ are two random variables fixed once and for all in most of the argument. To lighten notation, We package X^0_1 and X^0_2 in a single object named p.

We denote it as τ[X₁ ; μ₁ # X₂ ; μ₂ | p] where p is a fixed package containing the information of the reference random variables. When the measurable spaces have a canonical measure ℙ, we can use τ[X₁ # X₂ | p]

Equations

• One or more equations did not get rendered due to their size.

def «termτ[_#_|_]» : Lean.ParserDescr

If $X_1,X_2$ are two $G$-valued random variables, then $$\tau [X_1;X_2]:=d[X_1;X_2]+\eta d[X_1^0;X_1]+\eta d[X_2^0;X_2].$$ Here, $X_1^0$ and $X_2^0$ are two random variables fixed once and for all in most of the argument. To lighten notation, We package X^0_1 and X^0_2 in a single object named p.

We denote it as τ[X₁ ; μ₁ # X₂ ; μ₂ | p] where p is a fixed package containing the information of the reference random variables. When the measurable spaces have a canonical measure ℙ, we can use τ[X₁ # X₂ | p]

Equations

• One or more equations did not get rendered due to their size.

def «termτ[_#_|_]».«delab_app.tau» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem continuous_tau_restrict_probabilityMeasure {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G × MeasureTheory.ProbabilityMeasure G) => τ[id ; ↑μ.1 # id ; ↑μ.2 | p]

theorem ProbabilityTheory.IdentDistrib.tau_eq {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω₁ : Type u_5} {Ω₂ : Type u_6} {Ω'₁ : Type u_7} {Ω'₂ : Type u_8} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω'₁] [MeasurableSpace Ω'₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {μ'₁ : MeasureTheory.Measure Ω'₁} {μ'₂ : MeasureTheory.Measure Ω'₂} {X₁ : Ω₁ → G} {X₂ : Ω₂ → G} {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G} (h₁ : IdentDistrib X₁ X₁' μ₁ μ'₁) (h₂ : IdentDistrib X₂ X₂' μ₂ μ'₂) : τ[X₁ ; μ₁ # X₂ ; μ₂ | p] = τ[X₁' ; μ'₁ # X₂' ; μ'₂ | p]

If $X_1^{\prime },X_2^{\prime }$ are copies of $X_1,X_2$, then $\tau [X_1^{\prime };X_2^{\prime }]=\tau [X_1;X_2]$.

def tau_minimizes {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_11} [MeasureTheory.MeasureSpace Ω] (X₁ X₂ : Ω → G) : Prop

Property recording the fact that two random variables minimize the tau functional. Expressed in terms of measures on the group to avoid quantifying over all spaces, but this implies comparison with any pair of random variables, see Lemma is_tau_min.

Equations

• tau_minimizes p X₁ X₂ = ∀ (ν₁ ν₂ : MeasureTheory.Measure G), MeasureTheory.IsProbabilityMeasure ν₁ → MeasureTheory.IsProbabilityMeasure ν₂ → τ[X₁ # X₂ | p] ≤ τ[id ; ν₁ # id ; ν₂ | p]

theorem ProbabilityTheory.IdentDistrib.tau_minimizes {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_3} {Ω' : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.MeasureSpace Ω'] {X₁ X₂ : Ω → G} {X₁' X₂' : Ω' → G} (h₁ : IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) : _root_.tau_minimizes p X₁ X₂ ↔ _root_.tau_minimizes p X₁' X₂'

If $X_1^{\prime },X_2^{\prime }$ are copies of $X_1,X_2$, then $X_1,X_2$ minimize $\tau$ iff $X_1^{\prime },X_2^{\prime }$ do.

theorem tau_min_exists_measure {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) [MeasurableSingletonClass G] : ∃ (μ : MeasureTheory.Measure G × MeasureTheory.Measure G), MeasureTheory.IsProbabilityMeasure μ.1 ∧ MeasureTheory.IsProbabilityMeasure μ.2 ∧ ∀ (ν₁ ν₂ : MeasureTheory.Measure G), MeasureTheory.IsProbabilityMeasure ν₁ → MeasureTheory.IsProbabilityMeasure ν₂ → τ[id ; μ.1 # id ; μ.2 | p] ≤ τ[id ; ν₁ # id ; ν₂ | p]

A pair of measures minimizing $\tau$ exists.

theorem tau_minimizer_exists {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) [MeasurableSingletonClass G] : ∃ (Ω : Type uG) (x : MeasureTheory.MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G), Measurable X₁ ∧ Measurable X₂ ∧ MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ tau_minimizes p X₁ X₂

A pair of random variables minimizing $\tau$ exists.

theorem is_tau_min {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_3} {Ω'₁ : Type u_7} {Ω'₂ : Type u_8} [MeasureTheory.MeasureSpace Ω] [hΩ₁ : MeasureTheory.MeasureSpace Ω'₁] [hΩ₂ : MeasureTheory.MeasureSpace Ω'₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ : Ω → G} {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G} (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') : τ[X₁ # X₂ | p] ≤ τ[X₁' # X₂' | p]

theorem distance_ge_of_min {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_3} {Ω'₁ : Type u_7} {Ω'₂ : Type u_8} [MeasureTheory.MeasureSpace Ω] [hΩ₁ : MeasureTheory.MeasureSpace Ω'₁] [hΩ₂ : MeasureTheory.MeasureSpace Ω'₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ : Ω → G} {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G} (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') : d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁'] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂'] - d[p.X₀₂ # X₂]) ≤ d[X₁' # X₂']

Let X₁ and X₂ be tau-minimizers associated to p, with $d[X_1,X_2]=k$, then $$d[X_1^{\prime };X_2^{\prime }]\ge k-\eta (d[X_1^0;X_1^{\prime }]-d[X_1^0;X_1])-\eta (d[X_2^0;X_2^{\prime }]-d[X_2^0;X_2])$$ for any $G$-valued random variables $X_1^{\prime },X_2^{\prime }$.

theorem distance_ge_of_min' {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_3} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ : Ω → G} {Ω'₁ : Type u_11} {Ω'₂ : Type u_12} (h : tau_minimizes p X₁ X₂) [MeasurableSpace Ω'₁] [MeasurableSpace Ω'₂] {μ : MeasureTheory.Measure Ω'₁} {μ' : MeasureTheory.Measure Ω'₂} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G} (h1 : Measurable X₁') (h2 : Measurable X₂') : d[X₁ # X₂] - p.η * (d[p.X₀₁ ; MeasureTheory.volume # X₁' ; μ] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ ; MeasureTheory.volume # X₂' ; μ'] - d[p.X₀₂ # X₂]) ≤ d[X₁' ; μ # X₂' ; μ']

Version of distance_ge_of_min with the measures made explicit.

theorem condRuzsaDistance_ge_of_min {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {G : Type uG} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_3} {Ω'₁ : Type u_7} {Ω'₂ : Type u_8} {S : Type u_9} {T : Type u_10} [MeasureTheory.MeasureSpace Ω] [hΩ₁ : MeasureTheory.MeasureSpace Ω'₁] [hΩ₂ : MeasureTheory.MeasureSpace Ω'₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ : Ω → G} {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G} [MeasurableSingletonClass G] [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype T] [MeasurableSpace T] [MeasurableSingletonClass T] (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') (Z : Ω'₁ → S) (W : Ω'₂ → T) (hZ : Measurable Z) (hW : Measurable W) : d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁' | Z] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂' | W] - d[p.X₀₂ # X₂]) ≤ d[X₁' | Z # X₂' | W]

For any $G$-valued random variables $X_1^{\prime },X_2^{\prime }$ and random variables $Z,W$, one can lower bound $d[X_1^{\prime }|Z;X_2^{\prime }|W]$ by $$k-\eta (d[X_1^0;X_1^{\prime }|Z]-d[X_1^0;X_1])-\eta (d[X_2^0;X_2^{\prime }|W]-d[X_2^0;X_2]).$$