\begin{definition}[$\tau$-minimizer]\label{tau-min-def}
\uses{tau-def}
\lean{tau_minimizes}\leanok
A pair of $G$-valued random variables $X_1, X_2$ are said to be a $\tau$-minimizer if one has
  $$\tau[X_1;X_2] \leq \tau[X'_1;X'_2]
  $$
for all $G$-valued random variables $X'_1, X'_2$.
\end{definition}
def tau_minimizes {Ω : Type*} [MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) : Prop :=
  ∀ (ν₁ : Measure G) (ν₂ : Measure G), IsProbabilityMeasure ν₁ → IsProbabilityMeasure ν₂ →
      τ[X₁ # X₂ | p] ≤ τ[id ; ν₁ # id ; ν₂ | p]

omit [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)]
[Fintype G] in