dist_le_of_sum_zero

lemma dist_le_of_sum_zero {Ω' : Type*} [MeasurableSpace Ω'] {μ : Measure Ω'}    [IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G}    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :    k ≤ 3 * I[T₁ : T₂ ; μ] + (2 * H[T₃ ; μ] - H[T₁ ; μ] - H[T₂ ; μ])      + η * (ρ[T₁ | T₃ ; μ # A] + ρ[T₂ | T₃ ; μ #  A] - ρ[X₁ # A] - ρ[X₂ # A]) := by  cases nonempty_fintype G  let _ : MeasureSpace Ω' := ⟨μ⟩  have : μ = ℙ := rfl  simp only [this]  have : ∑ t, (Measure.real ℙ (T₃ ⁻¹' {t})) * d[ X₁ # X₂ ] ≤ ∑ t, (Measure.real ℙ (T₃ ⁻¹' {t})) *      (d[T₁ ; ℙ[|T₃ ← t] # T₂ ; ℙ[|T₃ ← t]]        + η * (ρ[T₁ ; ℙ[|T₃ ← t] # A] - ρ[X₁ # A]) + η * (ρ[T₂ ; ℙ[|T₃ ← t] # A] - ρ[X₂ # A])) := by    apply Finset.sum_le_sum (fun t ht ↦ ?_)    rcases eq_or_ne (Measure.real ℙ (T₃ ⁻¹' {t})) 0 with h't | h't    · simp [h't]    have : IsProbabilityMeasure (ℙ[|T₃ ← t]) := cond_isProbabilityMeasure_of_real h't    gcongr    exact le_rdist_of_phiMinimizes' h_min hT₁ hT₂  have : k ≤ ∑ x : G, (Measure.real ℙ (T₃ ⁻¹' {x})) * d[T₁ ; ℙ[|T₃ ← x] # T₂ ; ℙ[|T₃ ← x]] +      η * (ρ[T₁ | T₃ # A] - ρ[X₁ # A]) + η * (ρ[T₂ | T₃ # A] - ρ[X₂ # A]) := by    have S : ∑ i : G, (Measure.real ℙ (T₃ ⁻¹' {i})) = 1 := by      have : IsProbabilityMeasure (Measure.map T₃ ℙ) := isProbabilityMeasure_map hT₃.aemeasurable      simp [← map_measureReal_apply hT₃ (measurableSet_singleton _)]    simp_rw [← Finset.sum_mul, S, mul_add, Finset.sum_add_distrib, ← mul_assoc, mul_comm _ η,      mul_assoc, ← Finset.mul_sum, mul_sub, Finset.sum_sub_distrib, mul_sub,      ← Finset.sum_mul, S] at this    simpa [mul_sub, condRho, tsum_fintype] using this  have J : ∑ x : G, (Measure.real ℙ (T₃ ⁻¹' {x})) * d[T₁ ; ℙ[|T₃ ← x] # T₂ ; ℙ[|T₃ ← x]]      ≤ 3 * I[T₁ : T₂] + 2 * H[T₃] - H[T₁] - H[T₂] := by    have h2T₃ : T₃ = T₁ + T₂ :=      calc T₃ = T₁ + T₂ + T₃ - T₃ := by rw [hsum, _root_.zero_sub]; simp [ZModModule.neg_eq_self]        _ = T₁ + T₂ := by rw [add_sub_cancel_right]    subst h2T₃    simpa [integral_fintype .of_finite, map_measureReal_apply hT₃ (.singleton _)]      using ent_bsg hT₁ hT₂ (μ := ℙ)  linarith