ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul

@[to_additive /-- `max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X + Y | Z]` -/]lemma max_condEntropy_sub_condMutualInfo_le_condEntropy_mul {Z : Ω → T} [FiniteRange Z]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) :    max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y | Z ; μ] ≤ H[X * Y | Z ; μ] := by  rw [condMutualInfo_comm hX hY, condEntropy_eq_kernel_entropy hX hZ,    condEntropy_eq_kernel_entropy hY hZ, condMutualInfo_eq_kernel_mutualInfo hY hX hZ,    condEntropy_eq_kernel_entropy (show Measurable (X * Y) from hX.mul hY) hZ]  rw [Kernel.entropy_congr (condDistrib_snd_ae_eq hY hX hZ μ).symm,    Kernel.entropy_congr (condDistrib_fst_ae_eq hY hX hZ μ).symm,    max_comm]  refine (Kernel.max_entropy_sub_mutualInfo_le_entropy_mul' _ _ ?_).trans_eq ?_  · exact Kernel.aefiniteKernelSupport_condDistrib _ _ _ (hY.prodMk hX) hZ  have h := condDistrib_comp Z (hY.prodMk hX).aemeasurable    (f := fun x ↦ x.2 * x.1) (by fun_prop) (μ := μ) (mβ := inferInstance)  rw [Kernel.entropy_congr h.symm]  rfl