\begin{lemma}[Distance from zero]\label{dist-zero}
  \uses{ruz-dist-def}\lean{rdist_zero_eq_half_ent}\leanok
If $X$ is a $G$-valued random variable and $0$ is the random variable taking the value $0$ everywhere then
\[d[X;0]=\mathbb{H}(X)/2.\]
\end{lemma}
\begin{proof}\leanok
This is an immediate consequence of the definitions and $X-0\equiv X$ and $\mathbb{H}(0)=0$.
\end{proof}
/-- `d[X ; 0] = H[X] / 2`. -/
lemma rdist_zero_eq_half_ent [IsFiniteMeasure μ] [IsProbabilityMeasure μ'] :
    d[X ; μ # fun _ ↦ 0 ; μ'] = H[X ; μ]/2 := by
  have aux : H[fun x => x.1 - x.2 ; Measure.prod (Measure.map X μ) (Measure.map (fun x => 0) μ')]
            = H[X ; μ] := by
    have h: Measure.map (fun x => x.1 - x.2)
                        (Measure.prod (Measure.map X μ) (Measure.map (fun x => 0) μ'))
            = Measure.map X μ := by
              simp [MeasureTheory.Measure.map_const, MeasureTheory.Measure.prod_dirac]
              rw [Measure.map_map (by fun_prop) (by fun_prop)]
              have helper : ((fun (x : G × G) => x.1 - x.2) ∘ fun x => (x, (0 : G))) = id := by
                funext; simp
              rw [helper, Measure.map_id]
    simp [entropy_def, h]
  simp [rdist_def, entropy_const (0 : G), aux]
  ring