AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling

- A joint finite law is recovered by combining its first marginal with the conditional distribution of the second coordinate given the first. This is the source-neutral law identity behind one-block Gibbs/heat-bath resampling. It says nothing about scan order, irreducibility, convergence, or mixing; those are downstream kernel obligations. The nonempty Standard Borel hypothesis concerns the resampled coordinate `β`, not `α`. It is the regular-conditional-distribution existence contract used by Mathlib; the selected version agrees with the conditional law only almost everywhere for the first marginal. No conditional-support assertion on null fibers is made. Finite measures, including the zero measure, are allowed: this is not restricted to probability laws.

theorem fst_compProd_condDistrib_snd_eq_self
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [StandardBorelSpace β] [Nonempty β]
    {μ : Measure (α × β)} [IsFiniteMeasure μ] :
    (μ.map Prod.fst) ⊗ₘ
        ProbabilityTheory.condDistrib Prod.snd Prod.fst μ = μ := by
  have h := ProbabilityTheory.compProd_map_condDistrib
    (μ := μ) (X := Prod.fst) (Y := Prod.snd) (mβ := inferInstance)
    measurable_snd.aemeasurable
  simpa using h

end ConditionalResampling
end Probability
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Probability/ConditionalResampling.lean:32published source at 0e31a3cda412