kvm_ineq_II

lemma kvm_ineq_II {I : Type*} {i₀ : I} {s : Finset I} (hs : ¬ i₀ ∈ s)    (hs' : Finset.Nonempty s) {Y : I → Ω → G} [∀ i, FiniteRange (Y i)]    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :    d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ] := by  classical  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure  let φ i : G → G := if i = i₀ then id else - id  have hφ i : Measurable (φ i) := .of_discrete  let Y' i : Ω → G := φ i ∘ Y i  have mnY : ∀ i, Measurable (Y' i) := fun i ↦ (hφ i).comp (hY i)  have h_indep2 : IndepFun (Y i₀) (∑ i ∈ s, Y i) μ :=    h_indep.indepFun_finsetSum_of_notMem (fun i ↦ hY i) hs |>.symm  have ineq4 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ] + 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ])      ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ])) := by    calc      _ = H[Y i₀ - ∑ i ∈ s, Y i ; μ] - H[Y i₀ ; μ] := by        rw [h_indep2.rdist_eq (hY i₀) (by fun_prop)]        ring      _ = H[Y' i₀ + ∑ x ∈ s, Y' x ; μ] - H[Y' i₀ ; μ] := by        simp only [sub_eq_add_neg, ← Finset.sum_neg_distrib, ↓reduceIte, CompTriple.comp_eq,          _root_.add_left_inj, Y', φ]        congr! 3 with i hi        simp [ne_of_mem_of_not_mem hi hs, Pi.neg_comp]      _ ≤ ∑ x ∈ s, (H[Y' i₀ + Y' x ; μ] - H[Y' i₀ ; μ]) := kvm_ineq_I hs mnY (h_indep.comp φ hφ)      _ = ∑ i ∈ s, (H[Y i₀ - Y i ; μ] - H[Y i₀ ; μ]) := by        congr! 1 with i hi; simp [Y', φ, ne_of_mem_of_not_mem hi hs, Pi.neg_comp, sub_eq_add_neg]      _ = _ := by        refine Finset.sum_congr rfl fun i hi ↦ ?_        rw [(h_indep.indepFun (ne_of_mem_of_not_mem hi hs).symm).rdist_eq (hY i₀) (hY i)]        ring  replace ineq4 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ]      + 1/2 * (H[Y i; μ] - H[Y i₀; μ])) - 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ]) :=    le_tsub_of_add_le_right ineq4  have ineq5 (j : I) (hj : j ∈ s) : H[Y j ; μ] ≤ H[∑ i ∈ s, Y i; μ] :=    max_entropy_le_entropy_sum hj hY h_indep  have ineq6 :      (s.card : ℝ)⁻¹ * ∑ i ∈ s, (H[Y i; μ] - H[Y i₀; μ]) ≤ H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ] := by    rw [inv_mul_le_iff₀ (by exact_mod_cast Finset.card_pos.mpr hs'), ← smul_eq_mul,      Nat.cast_smul_eq_nsmul, ← Finset.sum_const]    refine Finset.sum_le_sum fun i hi ↦ ?_    gcongr    exact ineq5 i hi  have ineq7 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ]    ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) := by    calc      _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ]))          - 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ]) := ineq4      _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ]))          - 1/2 * ((s.card : ℝ)⁻¹ * ∑ i ∈ s, (H[Y i; μ] - H[Y i₀; μ])) := by gcongr      _ = ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ])          - 1/2 * ((s.card : ℝ)⁻¹ * (H[Y i; μ] - H[Y i₀; μ]))) := by        rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_sub_distrib]      _ = ∑ i ∈ s,          (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) := by        refine Finset.sum_congr rfl fun i _ ↦ ?_        rw [add_sub_assoc, ← mul_assoc, ← sub_mul]        field_simp  have ineq8 (i : I) : H[Y i; μ] - H[Y i₀; μ] ≤ 2 * d[Y i₀; μ # Y i; μ] := by    calc      _ ≤ |H[Y i₀ ; μ] - H[Y i ; μ]| := by        rw [← neg_sub]        exact neg_le_abs _      _ ≤ 2 * d[Y i₀; μ # Y i; μ] := diff_ent_le_rdist (hY i₀) (hY i)  calc    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) :=      ineq7    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / s.card * d[Y i₀; μ # Y i; μ]) := by      simp_rw [div_eq_mul_inv, mul_inv, mul_comm (2 : ℝ)⁻¹, mul_assoc]      gcongr ∑ i ∈ s, (d[Y i₀ ; μ # Y i ; μ] + (s.card - 1) * ((s.card : ℝ)⁻¹ * ?_))      · simp only [sub_nonneg, Nat.one_le_cast]        exact Nat.one_le_iff_ne_zero.mpr <| Finset.card_ne_zero.mpr hs'      · exact (inv_mul_le_iff₀ zero_lt_two).mpr (ineq8 _)    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + d[Y i₀; μ # Y i; μ]) := by      gcongr ∑ i ∈ s, (d[Y i₀ ; μ # Y i ; μ] + ?_) with i      refine mul_le_of_le_one_left (rdist_nonneg (hY i₀) (hY i)) ?_      exact (div_le_one (Nat.cast_pos.mpr <| Finset.card_pos.mpr hs')).mpr (by simp)    _ = 2 * ∑ i ∈ s, d[Y i₀ ; μ # Y i ; μ] := by      ring_nf      exact (Finset.sum_mul ..).symm