\begin{lemma}[Kullback--Leibler and sums]\label{kl-sums}\lean{KLDiv_add_le_KLDiv_of_indep}\leanok If $X, Y, Z$ are independent $G$-valued random variables, then
  $$D_{KL}(X+Z\Vert Y+Z) \leq D_{KL}(X\Vert Y).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-div-inj,kl-div-convex}
For each $z$, $D_{KL}(X+z\Vert Y+z)=D_{KL}(X\Vert Y)$ by \Cref{kl-div-inj}. Then apply \Cref{kl-div-convex} with $w_z=\mathbf{P}(Z=z)$.
\end{proof}
lemma KLDiv_add_le_KLDiv_of_indep [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Y Z : Ω → G} [IsZeroOrProbabilityMeasure μ]
    (h_indep : IndepFun (⟨X, Y⟩) Z μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (habs : ∀ x, μ.map Y {x} = 0 → μ.map X {x} = 0) :
    KL[X + Z ; μ # Y + Z ; μ] ≤ KL[X ; μ # Y ; μ] := by
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
  · simp [KLDiv]
  set X' : G → Ω → G := fun s ↦ (· + s) ∘ X with hX'
  set Y' : G → Ω → G := fun s ↦ (· + s) ∘ Y with hY'
  have AX' x i : μ.map (X' i) {x} = μ.map X {x - i} := by
    rw [hX', ← Measure.map_map (by fun_prop) (by fun_prop),
      Measure.map_apply (by fun_prop) (measurableSet_singleton x)]
    congr
    ext y
    simp [sub_eq_add_neg]
  have AY' x i : μ.map (Y' i) {x} = μ.map Y {x - i} := by
    rw [hY', ← Measure.map_map (by fun_prop) (by fun_prop),
      Measure.map_apply (by fun_prop) (measurableSet_singleton x)]
    congr
    ext y
    simp [sub_eq_add_neg]
  let w : G → ℝ := fun s ↦ (μ.map Z {s}).toReal
  have sum_w : ∑ s, w s = 1 := by
    have : IsProbabilityMeasure (μ.map Z) := isProbabilityMeasure_map hZ.aemeasurable
    simp [w]
  have A x : (μ.map (X + Z) {x}).toReal = ∑ s, w s * (μ.map (X' s) {x}).toReal := by
    have : IndepFun X Z μ := h_indep.comp (φ := Prod.fst) (ψ := id) measurable_fst measurable_id
    rw [this.map_add_singleton_eq_sum hX hZ, ENNReal.toReal_sum (by simp [ENNReal.mul_eq_top])]
    simp only [ENNReal.toReal_mul]
    congr with i
    congr 1
    rw [AX']
  have B x : (μ.map (Y + Z) {x}).toReal = ∑ s, w s * (μ.map (Y' s) {x}).toReal := by
    have : IndepFun Y Z μ := h_indep.comp (φ := Prod.snd) (ψ := id) measurable_snd measurable_id
    rw [this.map_add_singleton_eq_sum hY hZ, ENNReal.toReal_sum (by simp [ENNReal.mul_eq_top])]
    simp only [ENNReal.toReal_mul]
    congr with i
    congr 1
    rw [AY']
  have : KL[X + Z ; μ # Y + Z; μ] ≤ ∑ s, w s * KL[X' s ; μ # Y' s ; μ] := by
    apply KLDiv_of_convex (fun s _ ↦ by simp [w])
    · exact A
    · exact B
    · intro s _ x
      rw [AX', AY']
      exact habs _
  apply this.trans_eq
  have C s : KL[X' s ; μ # Y' s ; μ] = KL[X ; μ # Y ; μ] :=
    KLDiv_of_comp_inj (add_left_injective s) hX hY
  simp_rw [C, ← Finset.sum_mul, sum_w, one_mul]

/-- If $X,Y,Z$ are random variables, with $X,Z$ defined on the same sample space, we define
$$ D_{KL}(X|Z \Vert Y) := \sum_z \mathbf{P}(Z=z) D_{KL}( (X|Z=z) \Vert Y).$$ -/
noncomputable def condKLDiv {S : Type*} (X : Ω → G) (Y : Ω' → G) (Z : Ω → S)
    (μ : Measure Ω := by volume_tac) (μ' : Measure Ω' := by volume_tac) : ℝ :=
  ∑' z, (μ (Z⁻¹' {z})).toReal * KL[X ; (ProbabilityTheory.cond μ (Z⁻¹' {z})) # Y ; μ']

@[inherit_doc condKLDiv]
notation3:max "KL[" X " | " Z " ; " μ " # " Y " ; " μ' "]" => condKLDiv X Y Z μ μ'

@[inherit_doc condKLDiv]
notation3:max "KL[" X " | " Z " # " Y "]" => condKLDiv X Y Z volume volume

/-- If $X, Y$ are $G$-valued random variables, and $Z$ is another random variable
  defined on the same sample space as $X$, then
  $$D_{KL}((X|Z)\Vert Y) = D_{KL}(X\Vert Y) + \bbH[X] - \bbH[X|Z].$$ -/