ProbabilityTheory.Kernel.rdist_dirac_zero_right

@[simp] lemma rdist_dirac_zero_right {κ : Kernel T G} [IsFiniteKernel κ]    {μ : Measure T} {ν : Measure T'} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]    [FiniteSupport μ] [FiniteSupport ν] :    dk[κ ; μ # const T' (Measure.dirac 0) ; ν] = Hk[κ, μ] / 2 := by  rw [rdist_eq']  simp only [entropy_const, measure_univ, ENNReal.toReal_one, measureEntropy_dirac, mul_zero,    zero_div, sub_zero]  rw [sub_eq_iff_eq_add]  ring_nf  have : map (prodMkRight T' κ ×ₖ prodMkLeft T (const T' (Measure.dirac 0)))        (fun x ↦ x.1 - x.2)      = prodMkRight T' κ := by    ext x s hs    rw [prodMkRight_apply, map_apply _ (by fun_prop), prod_apply, prodMkLeft_apply, const_apply,      prodMkRight_apply, Measure.map_apply measurable_sub hs,      Measure.prod_apply (measurable_sub hs)]    have (x : G) : Prod.mk x ⁻¹' ((fun p : G × G ↦ p.1 - p.2) ⁻¹' s) = {y | x - y ∈ s} := by      ext; simp    simp_rw [this]    have (x : G) : Set.indicator {y | x - y ∈ s} (1 : G → ℝ≥0∞) 0 = s.indicator (fun _ ↦ 1) x := by      by_cases hx : x ∈ s <;> simp [hx]    simp only [Measure.dirac_apply, this]    rw [lintegral_indicator_const hs, one_mul]  rw [this, entropy_prodMkRight']