ProbabilityTheory.Kernel.rdist_triangle

lemma rdist_triangle (κ : Kernel T G) (η : Kernel T' G) (ξ : Kernel T'' G)    [IsMarkovKernel κ] [IsMarkovKernel η] [IsMarkovKernel ξ]    (μ : Measure T) (μ' : Measure T') (μ'' : Measure T'')    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [IsProbabilityMeasure μ'']    [FiniteSupport μ] [FiniteSupport μ'] [FiniteSupport μ'']    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) (hξ : FiniteKernelSupport ξ) :    dk[κ ; μ # ξ ; μ''] ≤ dk[κ ; μ # η ; μ'] + dk[η ; μ' # ξ ; μ''] := by  rw [rdist_eq', rdist_eq', rdist_eq']  have h := ent_of_diff_le (prodMkRight T' (prodMkRight T'' κ ×ₖ prodMkLeft T ξ))    (prodMkLeft (T × T'') η) ((μ.prod μ'').prod μ') ?_ ?_  rotate_left  · apply FiniteKernelSupport.prodMkRight    apply hκ.prodMkRight.prod hξ.prodMkLeft  · apply Kernel.FiniteKernelSupport.prodMkLeft hη  have h1 : Hk[map (prodMkRight T' (prodMkRight T'' κ ×ₖ prodMkLeft T ξ)) (fun p ↦ p.1 - p.2),      (μ.prod μ'').prod μ']      = Hk[map (prodMkRight T'' κ ×ₖ prodMkLeft T ξ) (fun x ↦ x.1 - x.2), μ.prod μ''] := by    rw [map_prodMkRight, entropy_prodMkRight']  have h2 :      Hk[map (fst (prodMkRight T' (prodMkRight T'' κ ×ₖ prodMkLeft T ξ)) ×ₖ prodMkLeft (T × T'') η)          (fun p ↦ p.1 - p.2), (μ.prod μ'').prod μ']      = Hk[map (prodMkRight T' κ ×ₖ prodMkLeft T η) (fun x ↦ x.1 - x.2), μ.prod μ'] := by    rw [fst_prodMkRight, fst_prod]    exact rdist_triangle_aux1 _ _ _ _ _  have h3 :      Hk[map (prodMkLeft (T × T'') η ×ₖ snd (prodMkRight T' (prodMkRight T'' κ ×ₖ prodMkLeft T ξ)))        (fun p ↦ p.1 - p.2), (μ.prod μ'').prod μ']      = Hk[map (prodMkRight T'' η ×ₖ prodMkLeft T' ξ) (fun x ↦ x.1 - x.2), μ'.prod μ''] := by    rw [snd_prodMkRight, snd_prod]    exact rdist_triangle_aux2 _ _ _ _ _  have h4 : Hk[prodMkLeft (T × T'') η, (μ.prod μ'').prod μ'] = Hk[η, μ'] := entropy_prodMkLeft  rw [h1, h2, h3, h4] at h  calc Hk[map (prodMkRight T'' κ ×ₖ prodMkLeft T ξ) (fun x ↦ x.1 - x.2), μ.prod μ'']      - Hk[κ , μ] / 2 - Hk[ξ , μ''] / 2    ≤ Hk[map (prodMkRight T' κ ×ₖ prodMkLeft T η) (fun x ↦ x.1 - x.2), μ.prod μ']      + Hk[map (prodMkRight T'' η ×ₖ prodMkLeft T' ξ) (fun x ↦ x.1 - x.2),        μ'.prod μ'']      - Hk[η, μ'] - Hk[κ , μ] / 2 - Hk[ξ , μ''] / 2 := by gcongr  _ = Hk[map (prodMkRight T' κ ×ₖ prodMkLeft T η) (fun x ↦ x.1 - x.2), μ.prod μ']      - Hk[κ , μ] / 2 - Hk[η , μ'] / 2      + (Hk[map (prodMkRight T'' η ×ₖ prodMkLeft T' ξ) (fun x ↦ x.1 - x.2), μ'.prod μ'']      - Hk[η , μ'] / 2 - Hk[ξ , μ''] / 2) := by ring