\begin{lemma}[Rho and sums]\label{rho-sums}\lean{rhoMinus_of_sum, rhoPlus_of_sum, rho_of_sum}\leanok  If $X,Y$ are independent, one has
  $$ \rho^-(X+Y) \leq \rho^-(X)$$
  $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$
and
  $$ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X] ).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-sums}
The first inequality follows from \Cref{kl-sums}. The second and third inequalities are direct corollaries of the first.
\end{proof}
lemma rhoMinus_of_sum [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y)
    (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ⁻[X + Y ; μ # A] ≤ ρ⁻[X ; μ # A] := by
  rcases eq_zero_or_isProbabilityMeasure μ with hμ | hμ
  · simp [rhoMinus_zero_measure hμ]
  apply le_csInf (nonempty_rhoMinusSet hA)
  have : IsProbabilityMeasure (uniformOn (A : Set G)) :=
    uniformOn_isProbabilityMeasure A.finite_toSet hA
  rintro - ⟨μ', μ'_prob, habs, rfl⟩
  obtain ⟨Ω', hΩ', m, X', Y', T, U, hm, h_indep', hX', hY', hT, hU, hXX', hYY', hTμ, hU_unif⟩ :=
    independent_copies4_nondep (X₁ := X) (X₂ := Y) (X₃ := id) (X₄ := id) hX hY measurable_id
    measurable_id μ μ μ' (uniformOn (A : Set G))
  let _ : MeasureSpace Ω' := ⟨m⟩
  have hP : (ℙ : Measure Ω') = m := rfl
  have hTU : IdentDistrib (T + U) (Prod.fst + Prod.snd) ℙ (μ'.prod (uniformOn (A : Set G))) := by
    apply IdentDistrib.add
    · exact hTμ.trans IdentDistrib.fst_id.symm
    · exact hU_unif.trans IdentDistrib.snd_id.symm
    · exact h_indep'.indepFun (i := 2) (j := 3) (by simp)
    · exact indepFun_fst_snd
  have hXY : IdentDistrib (X + Y) (X' + Y') μ ℙ := by
    apply IdentDistrib.add hXX'.symm hYY'.symm h_indep
    exact h_indep'.indepFun zero_ne_one
  have hX'TUY' : IndepFun (⟨X', T + U⟩) Y' ℙ := by
    have I : iIndepFun ![X', Y', T + U] m :=
      ProbabilityTheory.iIndepFun.apply_two_last h_indep' hX' hY' hT hU
        (phi := fun a b ↦ a + b) (by fun_prop)
    exact (I.reindex_three_bac.pair_last_of_three hY' hX' (by fun_prop)).symm
  have I₁ : ρ⁻[X + Y ; μ # A] ≤ KL[X + Y ; μ # (T + Y') + U ; ℙ] := by
    apply rhoMinus_le (by fun_prop) hA _ (by fun_prop) (by fun_prop)
    · have : iIndepFun ![U, X', T, Y'] := h_indep'.reindex_four_dacb
      have : iIndepFun ![U, X', T + Y'] :=
        this.apply_two_last (phi := fun a b ↦ a + b) hU hX' hT hY' (by fun_prop)
      apply this.indepFun (i := 2) (j := 0)
      simp
    · rw [hXY.map_eq]
      have : T + Y' + U = (T + U) + Y' := by abel
      rw [this]
      apply absolutelyContinuous_add_of_indep hX'TUY' hX' (by fun_prop) hY'
      rw [hTU.map_eq, hP, hXX'.map_eq]
      exact habs
    · exact isUniform_uniformOn.of_identDistrib hU_unif.symm A.measurableSet
  have I₂ : KL[X + Y ; μ # (T + Y') + U ; ℙ] = KL[X' + Y' # (T + U) + Y'] := by
    apply IdentDistrib.KLDiv_eq _ _ hXY
    have : T + Y' + U = T + U + Y' := by abel
    rw [this]
    apply IdentDistrib.refl
    fun_prop
  have I₃ : KL[X' + Y' # (T + U) + Y'] ≤ KL[X' # T + U] := by
    apply KLDiv_add_le_KLDiv_of_indep _ (by fun_prop) (by fun_prop) (by fun_prop)
    · rw [hTU.map_eq, hP, hXX'.map_eq]
      exact habs
    · exact hX'TUY'
  have I₄ : KL[X' # T + U] = KL[X ; μ # Prod.fst + Prod.snd ; μ'.prod (uniformOn (A : Set G))] :=
    IdentDistrib.KLDiv_eq _ _ hXX' hTU
  exact ((I₁.trans_eq I₂).trans I₃).trans_eq I₄

/-- If $X,Y$ are independent, one has
$$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$ -/