Why retaining one coordinate and conditionally resampling the other is invariant

1. The deterministic projection \((a,b)\mapsto a\) is measurable. Pushing \(μ\) through it gives exactly its first marginal \(\mu_1=(\mathrm{fst})_\#\mu\). This assertion uses the actual input \(μ\), not an arbitrary starting law with a different first marginal.

2. The product kernel \(a\mapsto δₐ⊗κ(a,·)\) is measurable because it is the product of the identity kernel and the measurable conditional kernel. Composition with the deterministic projection gives K. Associativity of kernel/measure composition yields \[\mu K=\mu_1(\mathrm{id}\times\kappa)=\mu_1\otimes\kappa.\] The last expression is a measure–kernel composition product, not the independent product of \(μ_{1}\) and a fixed marginal.

3. The supplied finite-measure disintegration identity now gives \[\mu K=\mu_1\otimes\kappa=\mu.\] It is justified by the standard-Borel, nonempty \(β\) and finite \(μ\) interface. No density, positivity, normalization to mass one or division by a marginal density is required. For \(μ=0\) both sides are zero; this is invariant as a finite measure, not a probability law.

4. Conditional versions agree in their prescribed conditional meaning only for \(μ_{1}\)-almost every a. Replacing them on a \(μ_{1}\)-null set does not change the integrated identity. The chosen global Markov version still yields a legitimate mass-one update there, but no claim about conditional support or convergence from such exceptional starting states follows.

5. For lack of convergence take \(α=\{0,1\}\), \(β=\{∗\}\) with discrete measurable structures and \(\mu=(\tfrac12\delta_0+\tfrac12\delta_1)\otimes\delta_\ast\). The update never changes either coordinate, so K is the identity kernel. Starting from \(\rho=\delta_{(0,\ast)}\), \[\begin{gathered}\rho K^n=\rho,\\ d_{\mathrm{TV}}(\rho K^n,\mu)=\tfrac12\quad(n\ge0).\end{gathered}\] Thus the actual invariant target does not imply uniqueness, irreducibility, mixing or convergence from a different first marginal.

/- 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
  change ((Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ) ∘ₖ
    Kernel.deterministic Prod.fst measurable_fst) ∘ₘ μ = μ
  rw [← Measure.comp_assoc, Measure.deterministic_comp_eq_map,
    ← Measure.compProd_eq_comp_prod]
  exact ConditionalResampling.fst_compProd_condDistrib_snd_eq_self

1. Identifies the measurable deterministic projection and its exact pushforward \(μ_{1}\) under the actual input law. (1 point)
2. Expresses the actual kernel as a deterministic composition and uses associativity and the measure–kernel product, not an independent product, to obtain \(μ_{1}⊗κ\). (1 point)
3. Applies the finite standard-Borel disintegration with the precise \(β\) hypotheses, permits zero \(μ\) and distinguishes global Markov normalization from almost-everywhere conditional support claims. (1 point)
4. Gives any valid finite-state instance of this conditional-resampling kernel that preserves its target yet fails to converge from a different initial probability law, with a correct persistent discrepancy calculation; the reference identity-kernel example and TV=1/2 are sufficient, not required. (1 point)

/- 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.

Download task template

The context supplies only the exact existing heatBathSnd definition, not its invariance theorem or Markov instance. The reference unfolds that kernel in the measure equality, reassociates composition, rewrites deterministic composition as the first pushforward and the identity-product composition as a composition product, then calls ConditionalResampling.fst_compProd_condDistrib_snd_eq_self. This is the actual finite-target invariance theorem, not an assumed stationarity premise. Its conclusion does not separately formalize the prose's identity-kernel counterexample or a mixing assertion.

/- 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
  change ((Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ) ∘ₖ
    Kernel.deterministic Prod.fst measurable_fst) ∘ₘ μ = μ
  rw [← Measure.comp_assoc, Measure.deterministic_comp_eq_map,
    ← Measure.compProd_eq_comp_prod]
  exact ConditionalResampling.fst_compProd_condDistrib_snd_eq_self

Download runnable reference