condRuzsaDist_of_indep

lemma condRuzsaDist_of_indep    {X : Ω → G} {Z : Ω → S} {Y : Ω → G} {W : Ω → T}    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)    (μ : Measure Ω) [IsProbabilityMeasure μ]    (h : IndepFun (⟨X, Z⟩) (⟨Y, W⟩) μ) [FiniteRange Z] [FiniteRange W] :    d[X | Z ; μ # Y | W ; μ] = H[X - Y | ⟨Z, W⟩ ; μ] - H[X | Z ; μ]/2 - H[Y | W ; μ]/2 := by  have : IsProbabilityMeasure (μ.map Z) := isProbabilityMeasure_map hZ.aemeasurable  have : IsProbabilityMeasure (μ.map W) := isProbabilityMeasure_map hW.aemeasurable  rw [condRuzsaDist_def, Kernel.rdist_eq', condEntropy_eq_kernel_entropy _ (hZ.prodMk hW),    condEntropy_eq_kernel_entropy hX hZ, condEntropy_eq_kernel_entropy hY hW]  swap; · exact hX.sub hY  congr 2  have hZW : IndepFun Z W μ := h.comp measurable_snd measurable_snd  have hZW_map : μ.map (⟨Z, W⟩) = (μ.map Z).prod (μ.map W) :=    (indepFun_iff_map_prod_eq_prod_map_map hZ.aemeasurable hW.aemeasurable).mp hZW  rw [← hZW_map]  refine Kernel.entropy_congr ?_  have : Kernel.map (condDistrib (⟨X, Y⟩) (⟨Z, W⟩) μ) (fun x ↦ x.1 - x.2)      =ᵐ[μ.map (⟨Z, W⟩)] condDistrib (X - Y) (⟨Z, W⟩) μ :=    (condDistrib_comp _ (by fun_prop) (by fun_prop)).symm  refine (this.symm.trans ?_).symm  suffices Kernel.prodMkRight T (condDistrib X Z μ)        ×ₖ Kernel.prodMkLeft S (condDistrib Y W μ)      =ᵐ[μ.map (⟨Z, W⟩)] condDistrib (⟨X, Y⟩) (⟨Z, W⟩) μ by    filter_upwards [this] with x hx    rw [Kernel.map_apply _ (by fun_prop), Kernel.map_apply _ (by fun_prop), hx]  exact (condDistrib_eq_prod_of_indepFun hX hZ hY hW μ h).symm