ProbabilityTheory.Kernel.max_entropy_le_entropy_div_prod

@[to_additive max_entropy_le_entropy_sub_prod]lemma max_entropy_le_entropy_div_prod    (κ : Kernel T G) [IsMarkovKernel κ] (η : Kernel T G) [IsMarkovKernel η]    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :    max (Hk[κ, μ]) (Hk[η, μ]) ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1 / p.2), μ] := by  calc max (Hk[κ, μ]) (Hk[η, μ])    = max (Hk[κ, μ]) (Hk[η, μ]) - Ik[κ ×ₖ η, μ] := by        rw [mutualInfo_prod _ hκ hη, sub_zero]  _ ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1 / p.2), μ] := by        convert max_entropy_sub_mutualInfo_le_entropy_div (κ ×ₖ η) μ (hκ.prod hη)        · simp        · simp