second_estimate

lemma second_estimate : I₂ ≤ 2 * p.η * k + (2 * p.η * (2 * p.η * k - I₁)) / (1 - p.η) := by  have hX₁_indep : IndepFun X₁ X₁' (μ := ℙ) := h_indep.indepFun (show 0 ≠ 2 by decide)  have hX₂_indep : IndepFun X₂ X₂' (μ := ℙ) := h_indep.indepFun (show 1 ≠ 3 by decide)  let Y : Fin 4 → Ω → G := ![X₂, X₁, X₂', X₁']  have hY : ∀ i, Measurable (Y i) := fun i => by fin_cases i <;> assumption  have hY_indep : iIndepFun Y := by exact h_indep.reindex_four_badc  have h := sum_of_rdist_eq_char_2 Y hY_indep hY  rw [show Y 0 = X₂ by rfl, show Y 1 = X₁ by rfl, show Y 2 = X₂' by rfl, show Y 3 = X₁' by rfl] at h  rw [← h₂.rdist_congr h₁, rdist_symm, rdist_symm (X := X₂ + X₂'),    condRuzsaDist_symm (Z := X₂ + X₂') (W := X₁ + X₁') (hX₂.add hX₂') (hX₁.add hX₁'),    ← two_mul] at h  replace h : 2 * k = d[X₁ + X₁' # X₂ + X₂'] + d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂']      + I[X₁ + X₂ : X₁ + X₁'|X₁ + X₂ + X₁' + X₂'] := by    convert h using 3 <;> abel  have h' := condRuzsaDistance_ge_of_min p h_min hX₁ hX₂ (X₁ + X₁') (X₂ + X₂') (hX₁.add hX₁')    (hX₂.add hX₂')  have h₁' := condRuzsaDist_diff_le''' ℙ p.hmeas1 hX₁ hX₁' hX₁_indep  have h₂' := condRuzsaDist_diff_le''' ℙ p.hmeas2 hX₂ hX₂' hX₂_indep  rw [h₁.entropy_congr, add_sub_cancel_right,    ← (IdentDistrib.refl hX₁.aemeasurable).rdist_congr h₁] at h₁'  rw [h₂.entropy_congr, add_sub_cancel_right,    ← (IdentDistrib.refl hX₂.aemeasurable).rdist_congr h₂] at h₂'  have h'' : I₂ ≤ p.η * (d[X₁ # X₁] + d[X₂ # X₂]) := by    simp_rw [← add_comm X₁ X₁']    have h₁'' := mul_le_mul_of_nonneg_left h₁' (show 0 ≤ p.η by linarith [p.hη])    have h₂'' := mul_le_mul_of_nonneg_left h₂' (show 0 ≤ p.η by linarith [p.hη])    have := rdist_of_sums_ge' p _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min    linarith  nth_rewrite 1 [mul_div_assoc, ← mul_add, mul_assoc, mul_left_comm]  refine h''.trans (mul_le_mul_of_nonneg_left ?_ (show 0 ≤ p.η by linarith [p.hη]))  exact second_estimate_aux p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min