\begin{definition}[Conditioned Ruzsa distance]\label{cond-dist-def}
  \uses{ruz-dist-def}
  \lean{condRuzsaDist}\leanok
If $(X, Z)$ and $(Y, W)$ are random variables (where $X$ and $Y$ are $G$-valued) we define
$$ d[X  | Z; Y | W] := \sum_{z,w}  \bbP[Z=z]  \bbP[W=w] d[(X|Z=z); (Y|(W=w))].$$
similarly
$$ d[X ; Y | W] := \sum_{w}  \bbP[W=w] d[X ; (Y|(W=w))].$$
\end{definition}
def condRuzsaDist (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T)
    (μ : Measure Ω := by volume_tac) [IsFiniteMeasure μ]
    (μ' : Measure Ω' := by volume_tac) [IsFiniteMeasure μ'] : ℝ :=
  dk[condDistrib X Z μ ; μ.map Z # condDistrib Y W μ' ; μ'.map W]

@[inherit_doc condRuzsaDist]
notation3:max "d[" X " | " Z " ; " μ " # " Y " | " W " ; " μ'"]" => condRuzsaDist X Z Y W μ μ'

@[inherit_doc condRuzsaDist]
notation3:max "d[" X " | " Z " # " Y " | " W "]" => condRuzsaDist X Z Y W volume volume