ProbabilityTheory.Kernel.ent_of_diff_le

lemma ent_of_diff_le (κ : Kernel T (G × G)) (η : Kernel T G) [IsMarkovKernel κ] [IsMarkovKernel η]    (μ : Measure T) [IsProbabilityMeasure μ] [FiniteSupport μ]    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) :    Hk[map κ (fun p : G × G ↦ p.1 - p.2), μ]      ≤ Hk[map ((fst κ) ×ₖ η) (fun p : G × G ↦ p.1 - p.2), μ]        + Hk[map (η ×ₖ (snd κ)) (fun p : G × G ↦ p.1 - p.2), μ]        - Hk[η, μ] := by  have hκη := hκ.prod hη  have h1 : Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, (p.1.2, p.1.1 - p.1.2))), μ]        + Hk[map κ (fun p ↦ p.1 - p.2), μ]      ≤ Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, p.1.1 - p.1.2)), μ]        + Hk[map κ (fun p ↦ (p.2, p.1 - p.2)), μ] := by    have h := entropy_triple_add_entropy_le      (map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, (p.1.2, p.1.1 - p.1.2)))) μ    simp only [snd_map_prod _ .of_discrete] at h    rw [deleteMiddle_map_prod _ .of_discrete] at h    have : map (κ ×ₖ η) (fun x ↦ x.1.1 - x.1.2)        = map κ (fun p ↦ p.1 - p.2) := by      have : (fun x : (G × G) × G ↦ x.1.1 - x.1.2)        = (fun x ↦ x.1 - x.2) ∘ Prod.fst := by ext1 y; simp      rw [this, ← map_map _ (by fun_prop) (by fun_prop), ← Kernel.fst_eq, fst_prod]    rw [this] at h    refine (h ?_).trans_eq ?_    · apply FiniteKernelSupport.aefiniteKernelSupport      apply FiniteKernelSupport.map      exact hκ.prod hη    congr 2    have : (fun x : (G × G) × G ↦ (x.1.2, x.1.1 - x.1.2))      = (fun x ↦ (x.2, x.1 - x.2)) ∘ Prod.fst := by ext1 y; simp    rw [this, ← map_map _ (by fun_prop) (by fun_prop), ← Kernel.fst_eq, fst_prod]  have h2 : Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, p.1.1 - p.1.2)), μ]      ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1.1 - p.2), μ]        + Hk[map (κ ×ₖ η) (fun p ↦ p.1.2 - p.2), μ] := by    calc Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, p.1.1 - p.1.2)), μ]      ≤ Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, p.1.2 - p.2)), μ] := by          have : (fun p : (G × G) × G ↦ (p.1.1 - p.2, p.1.1 - p.1.2))            = (fun p ↦ (p.1, p.1 - p.2)) ∘ (fun p ↦ (p.1.1 - p.2, p.1.2 - p.2)) := by ext1; simp          rw [this, ← map_map _ (by fun_prop) (by fun_prop)]          apply entropy_map_le _ _          apply FiniteKernelSupport.aefiniteKernelSupport          apply hκη.map    _ ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1.1 - p.2), μ]        + Hk[map (κ ×ₖ η) (fun p ↦ p.1.2 - p.2), μ] := by          have h : 0 ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1.1 - p.2), μ]              + Hk[map (κ ×ₖ η) (fun p ↦ p.1.2 - p.2), μ]              - Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, p.1.2 - p.2)), μ] := by            have h' := mutualInfo_nonneg (κ := map (κ ×ₖ η)              (fun p ↦ (p.1.1 - p.2, p.1.2 - p.2))) (μ := μ) ?_            · rwa [mutualInfo, fst_map_prod _ .of_discrete, snd_map_prod _ .of_discrete] at h'            apply FiniteKernelSupport.aefiniteKernelSupport            apply hκη.map          linarith  have h3 : Hk[map κ (fun p : G × G ↦ (p.2, p.1 - p.2)), μ]      ≤ Hk[κ, μ] := by    exact entropy_map_le _ (hκ.aefiniteKernelSupport _)  have h4 : Hk[map (κ ×ₖ η) (fun p ↦ (p.1.1 - p.2, (p.1.2, p.1.1 - p.1.2))), μ]      = Hk[κ ×ₖ η, μ] := by    refine entropy_of_map_eq_of_map      (fun p : G × G × G ↦ ((p.2.2 + p.2.1, p.2.1), -p.1 + p.2.2 + p.2.1))      (fun p : (G × G) × G ↦ (p.1.1 - p.2, (p.1.2, p.1.1 - p.1.2))) ?_ ?_ ?_        (hκη.aefiniteKernelSupport _)    · rw [map_map _ (by fun_prop) (by fun_prop)]      suffices ((fun p : G × G × G ↦ ((p.2.2 + p.2.1, p.2.1), -p.1 + p.2.2 + p.2.1))          ∘ fun p ↦ (p.1.1 - p.2, p.1.2, p.1.1 - p.1.2)) = id by        simp_rw [this, map_id]      ext1 p      simp    · rfl    apply FiniteKernelSupport.aefiniteKernelSupport    apply hκη.map  have h5 : Hk[κ ×ₖ η, μ] = Hk[κ, μ] + Hk[η, μ] := by    rw [entropy_prod (hκ.aefiniteKernelSupport _) (hη.aefiniteKernelSupport _)]  rw [h4, h5] at h1  calc Hk[map κ (fun p : G × G ↦ p.1 - p.2), μ]    ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1.1 - p.2), μ]      + Hk[map (κ ×ₖ η) (fun p ↦ p.1.2 - p.2), μ] - Hk[η, μ] := by        linarith  _ = Hk[map (κ ×ₖ η) (fun p ↦ p.1.1 - p.2), μ]      + Hk[map (κ ×ₖ η) (fun p ↦ p.2 - p.1.2), μ] - Hk[η, μ] := by        congr 2        rw [← entropy_neg, map_map _ (by fun_prop) (by fun_prop)]        congr with p        simp  _ = Hk[map ((fst κ) ×ₖ η) (fun p : G × G ↦ p.1 - p.2), μ]      + Hk[map (η ×ₖ (snd κ)) (fun p : G × G ↦ p.1 - p.2), μ]      - Hk[η, μ] := by        congr 3        · ext x s hs          rw [map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ hs,            prod_apply', prod_apply', lintegral_fst]          · congr with x          · exact .of_discrete          · exact measurable_sub hs          · exact .of_discrete        · exact ruzsa_triangle_aux κ η