ProbabilityTheory.Kernel.entropy_submodular_compProd

lemma entropy_submodular_compProd {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ]    {κ : Kernel (T × S) U} [IsZeroOrMarkovKernel κ] {η : Kernel (T × S × U) V} [IsMarkovKernel η]    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ (μ ⊗ₘ ξ))    (hη : AEFiniteKernelSupport η (μ ⊗ₘ (ξ ⊗ₖ κ))) (hξ : AEFiniteKernelSupport ξ μ) :    Hk[η, μ ⊗ₘ (ξ ⊗ₖ κ)]      ≤ Hk[snd (κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable)),            μ ⊗ₘ ξ] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  rcases eq_zero_or_isMarkovKernel ξ with rfl | hξ'  · simp  have : Nonempty S := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ ξ  have : Nonempty T := μ.nonempty_of_neZero  rcases eq_zero_or_isMarkovKernel κ with rfl | hκ'  · simp  have : Nonempty U := nonempty_of_isMarkovKernel κ  rcases eq_zero_or_isMarkovKernel η with rfl | hκ'  · simp  have : Nonempty V := nonempty_of_isMarkovKernel η  have h_meas := (MeasurableEquiv.prodAssoc : (T × S) × U ≃ᵐ T × S × U).measurable  have : FiniteSupport (μ ⊗ₘ ξ) := finiteSupport_of_compProd hξ  have : FiniteSupport (μ ⊗ₘ (ξ ⊗ₖ κ)) := finiteSupport_of_compProd (hξ.compProd hκ)  have h := entropy_condKernel_le_entropy_snd    (κ := κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc h_meas)) (μ := μ ⊗ₘ ξ) ?_  · simp only [fst_compProd] at h    have : condKernel (κ ⊗ₖ comap η ↑MeasurableEquiv.prodAssoc h_meas)        =ᵐ[μ ⊗ₘ ξ ⊗ₘ κ] comap η ↑MeasurableEquiv.prodAssoc h_meas := by      exact condKernel_compProd_ae_eq κ (comap η _ MeasurableEquiv.prodAssoc.measurable) (μ ⊗ₘ ξ)    rwa [entropy_congr this, Measure.compProd_compProd'', entropy_comap_equiv] at h  · refine (hκ.compProd ?_)    convert hη.comap_equiv MeasurableEquiv.prodAssoc    exact Measure.compProd_compProd'' _ _ _