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^0_1; X_1] + \eta d[X^0_2; 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|Z, X'_2|W]$ is at least $$k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] )$$ for any $X'_1, Z, X'_2, W$.
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₀₂
- η : ℝ
- hη : 0 < self.η
Instances For
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^0_1; X_1] + \eta d[X^0_2; X_2].$$
Here, $X^0_1$ and $X^0_2$ 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
Instances For
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^0_1; X_1] + \eta d[X^0_2; X_2].$$
Here, $X^0_1$ and $X^0_2$ 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.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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^0_1; X_1] + \eta d[X^0_2; X_2].$$
Here, $X^0_1$ and $X^0_2$ 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.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$.
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]
Instances For
If $X'_1, X'_2$ are copies of $X_1,X_2$, then $X_1, X_2$ minimize $\tau$ iff $X_1', X_2'$ do.
A pair of measures minimizing $\tau$ exists.
A pair of random variables minimizing $τ$ exists.
Let X₁ and X₂ be tau-minimizers associated to p, with $d[X_1,X_2]=k$, then
$$ d[X'_1;X'_2] \geq
k - \eta (d[X^0_1;X'_1] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2] - d[X^0_2;X_2] )$$
for any $G$-valued random variables $X'_1,X'_2$.
Version of distance_ge_of_min with the measures made explicit.
For any $G$-valued random variables $X'_1,X'_2$ and random variables $Z,W$, one can lower bound $d[X'_1|Z;X'_2|W]$ by $$k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] ).$$