/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling
import Mathlib.Probability.Kernel.Invariance

open MeasureTheory ProbabilityTheory
namespace AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath
noncomputable def heatBathSnd {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [StandardBorelSpace β] [Nonempty β] (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    Kernel (α × β) (α × β) :=
  (Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ) ∘ₖ
    Kernel.deterministic Prod.fst measurable_fst
end AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath
open AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath
open AutoSamplingTheory.TechnicalLemmas.Probability
variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
  [StandardBorelSpace β] [Nonempty β]

example (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    (heatBathSnd μ).Invariant μ := by
  -- Replace this comment with your proof.