ProbabilityTheory.Kernel.abs_sub_entropy_le_rdist

lemma abs_sub_entropy_le_rdist {κ : Kernel T G} {η : Kernel T' G}    [IsMarkovKernel κ] [IsMarkovKernel η]    {μ : Measure T} {ν : Measure T'} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]    [FiniteSupport μ] [FiniteSupport ν]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η ν) :    |Hk[κ, μ] - Hk[η, ν]| ≤ 2 * dk[κ ; μ # η ; ν] := by  have h := max_entropy_le_entropy_sub_prod (prodMkRight T' κ) (prodMkLeft T η) (μ.prod ν)    (hκ.prodMkRight ν) (hη.prodMkLeft μ)  rw [entropy_prodMkRight', entropy_prodMkLeft] at h  rw [rdist_eq', abs_le]  constructor  · linarith [le_max_right (Hk[κ, μ]) (Hk[η, ν])]  · linarith [le_max_left (Hk[κ, μ]) (Hk[η, ν])]