KLDiv_add_le_KLDiv_of_indep

lemma KLDiv_add_le_KLDiv_of_indep [Finite 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  cases nonempty_fintype G  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)).real {x} = (μ.map X).real {x - i} := by    rw [measureReal_def, measureReal_def, 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)).real {x} = (μ.map Y).real {x - i} := by    rw [measureReal_def, measureReal_def, 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 (s : G) : ℝ := (μ.map Z).real {s}  have sum_w : ∑ s, w s = 1 := by    have : IsProbabilityMeasure (μ.map Z) := Measure.isProbabilityMeasure_map hZ.aemeasurable    simp [w]  have A x : (μ.map (X + Z)).real {x} = ∑ s, w s * (μ.map (X' s)).real {x} := by    have : IndepFun X Z μ := h_indep.comp (φ := Prod.fst) (ψ := id) measurable_fst measurable_id    rw [this.real_map_add_singleton_eq_sum hX hZ]    congr with i    congr 1    rw [AX']  have B x : (μ.map (Y + Z)).real {x} = ∑ s, w s * (μ.map (Y' s)).real {x} := by    have : IndepFun Y Z μ := h_indep.comp (φ := Prod.snd) (ψ := id) measurable_snd measurable_id    rw [this.real_map_add_singleton_eq_sum hY hZ]    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      simpa [AX', AY', measureReal_eq_zero_iff] using 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]