ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div

@[to_additive /-- `max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X - Y | Z]` -/]lemma max_condEntropy_sub_condMutualInfo_le_condEntropy_div [FiniteRange X] [FiniteRange Y]    {Z : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [IsProbabilityMeasure μ] [FiniteRange 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 ?_ hZ]  swap ; · exact hX.div hY  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_div _ _ ?_).trans_eq ?_  · exact Kernel.aefiniteKernelSupport_condDistrib _ _ _ (hY.prodMk hX) hZ  rw [Kernel.entropy_div_comm]  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