\begin{lemma}[Kaimanovich-Vershik-Madiman inequality]\label{kv}
  \lean{kaimanovich_vershik}\leanok
Suppose that $X, Y, Z$ are independent $G$-valued random variables. Then
\[
  \bbH[X + Y + Z] - \bbH[X + Y] \leq \bbH[Y+ Z] - \bbH[Y].
\]
\end{lemma}
\begin{proof}\uses{submodularity, add-entropy, relabeled-entropy}\leanok
From \Cref{submodularity} we have
$$ \bbH[X, X + Y+ Z] + \bbH[Z, X + Y+ Z] \geq \bbH[X, Z, X + Y+ Z] + \bbH[X + Y+ Z].$$
However, using Lemmas \ref{add-entropy}, \ref{relabeled-entropy} repeatedly we have $\bbH[X, X + Y+ Z] = \bbH[X, Y+ Z] = \bbH[X] + \bbH[Y+ Z]$, $\bbH[Z, X + Y + Z] = \bbH[Z, X + Y] = \bbH[Z] + \bbH[X + Y]$ and $\bbH[X, Z, X + Y+ Z] = \bbH[X, Y, Z] = \bbH[X] + \bbH[Y] + \bbH[Z]$.  The claim then follows from a calculation.
\end{proof}
/-- The **Kaimanovich-Vershik inequality**. `H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y]`. -/
lemma kaimanovich_vershik {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    H[X + Y + Z ; μ] - H[X + Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by
  have : IsProbabilityMeasure μ := h.isProbabilityMeasure
  suffices (H[X ; μ] + H[Y ; μ] + H[Z ; μ]) + H[X + Y + Z ; μ]
    ≤ (H[X ; μ] + H[Y + Z ; μ]) + (H[Z ; μ] + H[X + Y ; μ]) by linarith
  have : ∀ (i : Fin 3), Measurable (![X, Y, Z] i) := fun i ↦ by fin_cases i <;> assumption
  convert entropy_triple_add_entropy_le μ hX hZ (show Measurable (X + (Y + Z)) by fun_prop)
    using 2
  · calc
      H[X ; μ] + H[Y ; μ] + H[Z ; μ] = H[⟨X, Y⟩ ; μ] + H[Z ; μ] := by
        rw [IndepFun.entropy_pair_eq_add hX hY]
        convert h.indepFun (show 0 ≠ 1 by decide)
      _ = H[⟨⟨X, Y⟩, Z⟩ ; μ] := by
        rw [IndepFun.entropy_pair_eq_add (hX.prodMk hY) hZ]
        exact h.indepFun_prodMk this 0 1 2 (by decide) (by decide)
      _ = H[⟨X, ⟨Z , X + (Y + Z)⟩⟩ ; μ] := by
        apply entropy_of_comp_eq_of_comp μ (by fun_prop) (by fun_prop)
          (fun ((x, y), z) ↦ (x, z, x + y + z)) (fun (a, b, c) ↦ ((a, c - a - b), b))
        all_goals { funext ω; dsimp [prod]; ext <;> dsimp; abel }
  · rw [add_assoc]
  · symm
    refine (entropy_add_right hX (by fun_prop) _).trans $
      IndepFun.entropy_pair_eq_add hX (by fun_prop) ?_
    exact h.indepFun_add_right this 0 1 2 (by decide) (by decide)
  · rw [eq_comm, ← add_assoc]
    refine (entropy_add_right' hZ (by fun_prop) _).trans $
      IndepFun.entropy_pair_eq_add hZ (by fun_prop) ?_
    exact h.indepFun_add_right this 2 0 1 (by decide) (by decide)