ent_ofsum_le

lemma ent_ofsum_le    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :    H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁]/2 + H[X₂]/2 + (2+p.η)*k - I₁ := by  let D := d[X₁ + X₂' # X₂ + X₁']  let Dcc := d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']  let D1 := d[p.X₀₁ # X₁]  let Dc1 := d[p.X₀₁ # X₁ | X₁ + X₂']  let D2 := d[p.X₀₂ # X₂]  let Dc2 := d[p.X₀₂ # X₂ | X₂ + X₁']  have lem68 : D + Dcc + I₁ = 2 * k :=    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep  have lem610 : Dcc ≥ k - p.η * (Dc1 - D1) - p.η * (Dc2 - D2) :=    condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' hX₁ hX₂ (by fun_prop) (by aesop) h_min  have lem611c : Dc1 - D1 ≤ k / 2 + H[X₁] / 4 - H[X₂] / 4 :=    diff_rdist_le_3 p X₁ X₂ X₁' X₂' hX₁ hX₂' h₂ h_indep  have lem611d : Dc2 - D2 ≤ k / 2 + H[X₂] / 4 - H[X₁] / 4 :=    diff_rdist_le_4 p X₁ X₂ X₁' X₂' hX₂ hX₁' h₁ h_indep  have aux : D + I₁ ≤ (1 + p.η) * k := by    calc D + I₁       ≤ k + p.η * (Dc1 - D1) + p.η * (Dc2 - D2) := ?_     _ ≤ k + p.η * (k / 2 + H[X₁] / 4 - H[X₂] / 4) + p.η * (k / 2 + H[X₂] / 4 - H[X₁] / 4) := ?_     _ = (1 + p.η) * k := by ring    · linarith    · gcongr <;> exact p.hη.le  have ent_sub_eq_ent_add : H[X₁ + X₂' - (X₂ + X₁')] = H[X₁ + X₂' + (X₂ + X₁')] := by    simp [ZModModule.sub_eq_add]  have rw₁ : X₁ + X₂' + (X₂ + X₁') = X₁ + X₂ + X₁' + X₂' := by abel  have ind_aux : IndepFun (X₁ + X₂') (X₂ + X₁') := by    exact iIndepFun.indepFun_add_add h_indep (fun i ↦ by fin_cases i <;> assumption) 0 2 1 3      (by decide) (by decide) (by decide) (by decide)  have ind : D = H[X₁ + X₂' - (X₂ + X₁')] - H[X₁ + X₂'] / 2 - H[X₂ + X₁'] / 2 :=    ind_aux.rdist_eq (by fun_prop) (by fun_prop)  rw [ind, ent_sub_eq_ent_add, rw₁] at aux  have obs : H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁ := by    linarith  have rw₂ : H[X₁ + X₂'] = k + H[X₁]/2 + H[X₂]/2 := by    have HX₂_eq : H[X₂] = H[X₂'] :=      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₂.map_eq    have k_eq : k = H[X₁ - X₂'] - H[X₁] / 2 - H[X₂'] / 2 := by      have k_eq_aux : k = d[X₁ # X₂'] := h₂.rdist_congr_right hX₁.aemeasurable      rw [k_eq_aux]      exact (h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)).rdist_eq hX₁ hX₂'    rw [k_eq, ← ZModModule.sub_eq_add, ← HX₂_eq]    ring  have rw₃ : H[X₂ + X₁'] = k + H[X₁]/2 + H[X₂]/2 := by    have HX₁_eq : H[X₁] = H[X₁'] :=      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₁.map_eq    have k_eq' : k = H[X₁' - X₂] - H[X₁'] / 2 - H[X₂] / 2 := by      have k_eq_aux : k = d[X₁' # X₂] := h₁.rdist_congr_left hX₂.aemeasurable      rw [k_eq_aux]      exact (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)).rdist_eq hX₁' hX₂    rw [add_comm X₂ X₁', k_eq', ← ZModModule.sub_eq_add, ← HX₁_eq]    ring  calc H[X₁ + X₂ + X₁' + X₂']      ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁  := obs    _ = (k + H[X₁] / 2 + H[X₂] / 2) / 2        + (k + H[X₁] / 2 + H[X₂] / 2) / 2 + (1 + p.η) * k - I₁  := by rw [rw₂, rw₃]    _ = H[X₁] / 2 + H[X₂] / 2 + (2 + p.η) * k - I₁              := by ring