Samplinglib · shared mathematical prerequisite

Why random-scan heat bath is reversible

Follow the proof from symmetric atomic flux to Mathlib’s full set-integral definition; zero target atoms are handled explicitly.

Theorem 1. Atomic balance implies reversibility

Statement

Let \(E\) be a countable measurable space with measurable singletons, \(\kappa\) a kernel on \(E\), and \(\mu\) a measure. Suppose every pair of atoms has equal forward and backward flux. Then the same symmetry holds between any two measurable sets.

\[\left[\forall x,y,\ \mu(\{x\})\kappa(x,\{y\})=\mu(\{y\})\kappa(y,\{x\})\right]\Longrightarrow\left[\forall A,B,\ \int_A\kappa(x,B)\,d\mu(x)=\int_B\kappa(y,A)\,d\mu(y)\right].\]

Sets \(A,B\) in the conclusion are measurable. Countability and measurable singletons allow atomic expansion.
No Markov, probability, finite-total-mass or integrability hypothesis is needed: integrals and sums here are nonnegative extended-valued ones.

Lean statement · isReversible_of_singleton_balance

α is an arbitrary state space. [Countable α] and [MeasurableSingletonClass α] express the two measurable-space hypotheses. The parameter h is the atomic balance equation. Kernel.IsReversible is Mathlib’s set-integral equality, not a new ASTIS definition.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isReversible_of_singleton_balance {α : Type*} [MeasurableSpace α]
    [Countable α] [MeasurableSingletonClass α] (κ : Kernel α α) (μ : Measure α)
    (h : ∀ x y, μ {x} * κ x {y} = μ {y} * κ y {x}) :
    Kernel.IsReversible κ μ

Exact module and namespace context

Mathematical proof

Write \(P=\kappa\) in the calculation below. Atomic balance is a hypothesis in this generic theorem; the next theorem proves it for the actual heat-bath kernel.

1. Pass from singletons to arbitrary sets

On a countable measurable-singleton space, expand each set integral into nonnegative atomic sums. Insert atomic balance, commute the two sums and regroup the measure of a set. Nonnegative extended sums allow this rearrangement without assuming integrability or finite total mass.

\[\begin{aligned}\int_A P(x,B)\,d\mu(x)&=\sum_{x\in A}\sum_{y\in B}\mu(\{x\})P(x,\{y\})\\&=\sum_{y\in B}\sum_{x\in A}\mu(\{y\})P(y,\{x\})\\&=\int_B P(y,A)\,d\mu(y).\end{aligned}\]

How this step appears in Lean

KernelReversibility.isReversible_of_singleton_balance uses lintegral_countable, ENNReal.tsum_mul_right and ENNReal.tsum_comm. randomScan_isReversible then applies that bridge to singleton_balance.

Lean proof · isReversible_of_singleton_balance

intro introduces arbitrary measurable sets. hm expresses a measure of a set as a countable sum of atom masses. lintegral_countable expands both integrals; tsum_mul_right distributes weights; tsum_comm swaps the nonnegative sums. The remaining equality is precisely the supplied balance hypothesis.

theorem isReversible_of_singleton_balance {α : Type*} [MeasurableSpace α]
    [Countable α] [MeasurableSingletonClass α] (κ : Kernel α α) (μ : Measure α)
    (h : ∀ x y, μ {x} * κ x {y} = μ {y} * κ y {x}) :
    Kernel.IsReversible κ μ := by
  intro A B _ _
  have hm (ν : Measure α) (s : Set α) : ν s = ∑' y : s, ν {(y : α)} := by
    simpa using (lintegral_countable (μ := ν) (fun _ => 1) (Set.to_countable s))
  rw [lintegral_countable _ (Set.to_countable A),
    lintegral_countable _ (Set.to_countable B)]
  conv_lhs => enter [1, x]; rw [hm (κ x) B, ← ENNReal.tsum_mul_right]
  conv_rhs => enter [1, y]; rw [hm (κ y) A, ← ENNReal.tsum_mul_right]
  rw [ENNReal.tsum_comm]
  apply tsum_congr
  intro y
  apply tsum_congr
  intro x
  simpa only [mul_comm] using h (x : α) (y : α)

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelReversibility

Exact module and namespace context

Theorem 2. The actual random-scan kernel is reversible

Statement

For any probability target \(\mu\) on \(\{0,1\}^{n+1}\), the actual uniform random-scan heat-bath kernel \(P\) is reversible. No full-support hypothesis is needed. For every pair of measurable sets \(A,B\):

\[\int_A P(x,B)\,d\mu(x)=\int_B P(y,A)\,d\mu(y).\]

The target is a probability measure on a finite Boolean cube with a nonempty site set. The kernel is the existing uniform randomScan. Zero-mass atoms are allowed.
This concerns weighted flux, not a claim about conditional normalization at unsupported inputs.

Lean statement · randomScan_isReversible

The single probability-measure premise is sufficient: no positivity premise is attached to the starting configuration. The conclusion applies to the existing randomScan μ rather than an abstract kernel assumed to be reversible.

theorem randomScan_isReversible {n : ℕ} (μ : Measure (Fin (n + 1) → Bool))
    [IsProbabilityMeasure μ] : Kernel.IsReversible (randomScan μ) μ

Exact module and namespace context

Mathematical proof

Prove atomic balance in the following cases, then apply Theorem 1. The finite Boolean space is countable and has measurable singletons, so all hypotheses of that bridge are available.

1. Compare flux at positive atoms

Use the supported-start transition law in both directions. Multiplying by the starting mass leaves a symmetric numerator in each matched-site summand.

\[\mu(\{x\})P(x,\{y\})=\frac1{n+1}\sum_i\mathbf1_{\{y_{-i}=x_{-i}\}}\frac{\mu(\{x\})\mu(\{y\})}{\mu(F_i(x))}.\]

How this step appears in Lean

The private singleton_balance lemma rewrites both randomScan_apply_singleton equations only after ruling out zero starting masses.

2. Identify the same retained-coordinate fiber

If the unselected coordinates match, the two fibers are the same set and therefore have the same mass. The matching condition itself is symmetric; if it fails, both summands vanish. This proves positive-atom flux symmetry term by term.

\[y_{-i}=x_{-i}\ \Longrightarrow\ F_i(y)=F_i(x),\qquad \mu(\{x\})P(x,\{y\})=\mu(\{y\})P(y,\{x\}).\]

How this step appears in Lean

hsym reverses the coordinate equalities; hf identifies retained-coordinate functions using Fin.succAbove_ne. Finset.sum_congr reduces to each site and ac_rfl handles the symmetric product.

3. Handle null atoms without a false conditional formula

If the first mass is zero and the second positive, evaluate the transition law from the positive atom. The numerator for arrival at the null atom is zero, so both weighted fluxes vanish. If both masses are zero, neither transition value needs to be identified.

\[\mu(\{x\})=0<\mu(\{y\})\ \Longrightarrow\ P(y,\{x\})=0,\qquad 0\cdot P(x,\{y\})=\mu(\{y\})\cdot0.\]

How this step appears in Lean

The local hz proof splits on the second mass. It calls randomScan_apply_singleton only with the supported start b; simp removes the zero numerator.

Lean proof · randomScan_isReversible

The public theorem applies KernelReversibility.isReversible_of_singleton_balance to the actual kernel and its privately proved singleton_balance. The private proof below contains the positive-atom and zero-atom case split; it does not assume the desired reversibility.

theorem randomScan_isReversible {n : ℕ} (μ : Measure (Fin (n + 1) → Bool))
    [IsProbabilityMeasure μ] : Kernel.IsReversible (randomScan μ) μ :=
  KernelReversibility.isReversible_of_singleton_balance _ μ (singleton_balance μ)

end AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBath

Exact module and namespace context

Lean proof · singleton_balance

Supporting proof called by the result above.

private theorem singleton_balance {n : ℕ} (μ : Measure (Fin (n + 1) → Bool))
    [IsProbabilityMeasure μ] (x y : Fin (n + 1) → Bool) :
    μ {x} * randomScan μ x {y} = μ {y} * randomScan μ y {x} := by
  classical
  have hz (a b : Fin (n + 1) → Bool) (ha : μ {a} = 0) :
      μ {a} * randomScan μ a {b} = μ {b} * randomScan μ b {a} := by
    by_cases hb : μ {b} = 0
    · simp only [ha, hb, zero_mul]
    · rw [randomScan_apply_singleton μ b a hb]
      simp only [ha, zero_mul, mul_zero, ite_self, Finset.sum_const_zero]
  by_cases hx : μ {x} = 0
  · exact hz x y hx
  by_cases hy : μ {y} = 0
  · exact (hz y x hy).symm
  rw [randomScan_apply_singleton μ x y hx, randomScan_apply_singleton μ y x hy]
  simp only [← mul_assoc]
  rw [mul_comm (μ {x}) (n + 1 : ℝ≥0∞)⁻¹,
    mul_comm (μ {y}) (n + 1 : ℝ≥0∞)⁻¹, mul_assoc, mul_assoc]
  congr 1
  rw [Finset.mul_sum, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro i _
  have hsym : (∀ j, j ≠ i → y j = x j) ↔ (∀ j, j ≠ i → x j = y j) :=
    ⟨fun h j hj => (h j hj).symm, fun h j hj => (h j hj).symm⟩
  by_cases h : ∀ j, j ≠ i → y j = x j
  · have hf : (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j)) :=
      funext (fun j => h _ (Fin.succAbove_ne _ _))
    simp only [if_pos h, if_pos (hsym.mp h), hf]
    ac_rfl
  · simp only [if_neg h, if_neg (mt hsym.mpr h), mul_zero]

/-- The actual uniform random-site heat-bath kernel is reversible for every
Boolean probability target, without a full-support or starting-atom premise.
Conditional versions at target-null inputs are immaterial to the flux. -/

Exact module and namespace context

What is still not proved by this result

Reversibility is not irreducibility, a spectral gap or a mixing bound. A probability target supported on two disconnected diagonal configurations can give two absorbing classes.
A deterministic composition of reversible coordinate kernels need not be reversible. This proof is for a uniform random mixture and one-update clock.
The source correspondence is the Boolean specialization of the standard finite-state argument, not all alphabets or every model-specific ergodicity claim.
Invariance and finite powers are existing downstream test consumers. They are not counted again as new mathematical leaves.

Proof dependencies

Declarations and reuse: ASTIS versus Mathlib

Results proved here by ASTIS

Existing ASTIS declarations reused

Mathlib results called, not re-proved here

ProbabilityTheory.Kernel.IsReversible — The set-integral reversibility definition
MeasureTheory.lintegral_countable — Atomic expansion
ENNReal.tsum_comm — Exchange nonnegative sums (exact pinned Mathlib implementation)

Focused tests · exact source

import AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBathReversibility
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance

namespace AutoSamplingTheory.Tests.RandomScanHeatBathReversibility

open MeasureTheory ProbabilityTheory
open scoped ENNReal NNReal
open AutoSamplingTheory.TechnicalLemmas.Probability
open AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBath

-- Infinite countable state space and infinite target/kernel mass are allowed
-- by the bridge: counting-measure constant kernel is not a Markov kernel.
example : Kernel.IsReversible (Kernel.const ℕ (Measure.count : Measure ℕ)) Measure.count := by
  apply KernelReversibility.isReversible_of_singleton_balance
  intro x y
  simp

example : (Kernel.const ℕ (Measure.count : Measure ℕ)) 0 Set.univ = ∞ := by
  exact Measure.count_apply_infinite Set.infinite_univ

example (κ : Kernel ℕ ℕ) : Kernel.IsReversible κ (0 : Measure ℕ) := by
  apply KernelReversibility.isReversible_of_singleton_balance
  intro x y
  simp

-- A generic target with null atoms still yields genuine set-flux equality.
example {n : ℕ} (μ : Measure (Fin (n + 1) → Bool)) [IsProbabilityMeasure μ]
    (A B : Set (Fin (n + 1) → Bool)) :
    ∫⁻ x in A, randomScan μ x B ∂μ = ∫⁻ y in B, randomScan μ y A ∂μ :=
  randomScan_isReversible μ (Set.to_countable A).measurableSet
    (Set.to_countable B).measurableSet

-- The standard existing consequence is consumed, not redefined in public.
example {n : ℕ} (μ : Measure (Fin (n + 1) → Bool)) [IsProbabilityMeasure μ]
    (k : ℕ) : ((randomScan μ) ^ k).Invariant μ :=
  KernelInvariance.invariant_pow (randomScan_isReversible μ).invariant k

private abbrev State := Fin 2 → Bool
private def a : State := ![false, false]
private def b : State := ![true, false]
private def d : State := ![true, true]

private noncomputable def nonuniform : Measure State :=
  (1 / 4 : ℝ≥0) • Measure.dirac a + (3 / 4 : ℝ≥0) • Measure.dirac b

local instance : IsProbabilityMeasure (α := Fin (1 + 1) → Bool) nonuniform := by
  constructor
  norm_num [nonuniform, Measure.add_apply, Measure.smul_apply, measure_univ]
  simpa [div_eq_mul_inv] using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
    (show (4 : ℝ≥0)⁻¹ + 3 * 4⁻¹ = 1 by norm_num)

private theorem nonuniform_a_pos : nonuniform {a} ≠ 0 := by
  norm_num [nonuniform, Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
    Set.indicator_apply, a, b, funext_iff, Fin.forall_fin_two]

private theorem nonuniform_b_pos : nonuniform {b} ≠ 0 := by
  norm_num [nonuniform, Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
    Set.indicator_apply, a, b, funext_iff, Fin.forall_fin_two]

private theorem forward_move : randomScan nonuniform a {b} = 3 / 8 := by
  rw [randomScan_apply_singleton nonuniform a b nonuniform_a_pos, Fin.sum_univ_two]
  norm_num [Fin.forall_fin_succ, nonuniform, Measure.smul_apply, Measure.add_apply,
    Measure.dirac_apply, Set.indicator_apply, a, b, funext_iff]
  have hsum : (4 : ℝ≥0∞)⁻¹ + 3 / 4 = 1 := by
    simpa [div_eq_mul_inv] using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
      (show (4 : ℝ≥0)⁻¹ + 3 / 4 = 1 by norm_num)
  rw [hsum, inv_one, one_mul]
  simpa [div_eq_mul_inv] using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
    (show (2 : ℝ≥0)⁻¹ * (3 / 4) = 3 / 8 by norm_num)

private theorem reverse_move : randomScan nonuniform b {a} = 1 / 8 := by
  rw [randomScan_apply_singleton nonuniform b a nonuniform_b_pos, Fin.sum_univ_two]
  norm_num [Fin.forall_fin_succ, nonuniform, Measure.smul_apply, Measure.add_apply,
    Measure.dirac_apply, Set.indicator_apply, a, b, funext_iff]
  have hsum : (4 : ℝ≥0∞)⁻¹ + 3 / 4 = 1 := by
    simpa [div_eq_mul_inv] using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
      (show (4 : ℝ≥0)⁻¹ + 3 / 4 = 1 by norm_num)
  rw [hsum, inv_one, one_mul]
  simpa using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
    (show (2 : ℝ≥0)⁻¹ * 4⁻¹ = 8⁻¹ by norm_num)

-- The actual transitions differ, while their stationary fluxes agree.
example : nonuniform {a} * randomScan nonuniform a {b} =
    nonuniform {b} * randomScan nonuniform b {a} := by
  simpa only [lintegral_singleton, mul_comm (nonuniform {a}), mul_comm (nonuniform {b})] using
    (randomScan_isReversible nonuniform (measurableSet_singleton a)
      (measurableSet_singleton b))

example : randomScan nonuniform a {b} ≠ randomScan nonuniform b {a} := by
  rw [forward_move, reverse_move]
  have hn : ((3 / 8 : ℝ≥0) : ℝ≥0∞) ≠ ((1 / 8 : ℝ≥0) : ℝ≥0∞) :=
    ENNReal.coe_injective.ne (by norm_num)
  simpa [div_eq_mul_inv] using hn

-- A forbidden ambient state does not need a positive-start hypothesis for
-- reversibility; its target flux is zero even when its kernel is still Markov.
private theorem forbidden_mass : nonuniform {d} = 0 := by
  norm_num [nonuniform, Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
    Set.indicator_apply, a, b, d, funext_iff, Fin.forall_fin_two]

example : nonuniform {d} * randomScan nonuniform d {a} = 0 := by
  simp only [forbidden_mass, zero_mul]

example : randomScan nonuniform a {d} = 0 := by
  rw [randomScan_apply_singleton nonuniform a d nonuniform_a_pos]
  simp [forbidden_mass]

-- Nonzero target with an invalid start whose every retained fiber is null.
private theorem null_fibers (i : Fin 2) :
    Measure.dirac a {z : State | (fun j => z (i.succAbove j)) =
      (fun j => d (i.succAbove j))} = 0 := by
  fin_cases i <;> norm_num [Measure.dirac_apply, Set.indicator_apply,
    a, d, funext_iff, Fin.forall_fin_one]

example : Kernel.IsReversible (randomScan (Measure.dirac a)) (Measure.dirac a) :=
  randomScan_isReversible _

example : randomScan (Measure.dirac a) d ≠
    (2 : ℝ≥0∞)⁻¹ • ∑ i : Fin 2,
      cond (Measure.dirac a) {z : State | (fun j => z (i.succAbove j)) =
        (fun j => d (i.succAbove j))} := by
  simp only [cond_eq_zero_of_meas_eq_zero (null_fibers _), Finset.sum_const_zero, smul_zero]
  intro h
  have hmass := congrArg (fun ν : Measure State => ν Set.univ) h
  simp only [measure_univ, Measure.coe_zero, Pi.zero_apply] at hmass
  exact one_ne_zero hmass

private noncomputable def diagonal : Measure State :=
  (1 / 2 : ℝ≥0) • (Measure.dirac a + Measure.dirac d)

local instance : IsProbabilityMeasure (α := Fin (1 + 1) → Bool) diagonal := by
  constructor
  norm_num [diagonal, Measure.add_apply, Measure.smul_apply, measure_univ]
  simpa using congrArg (fun r : ℝ≥0 => (r : ℝ≥0∞))
    (show (2 : ℝ≥0)⁻¹ + 2⁻¹ = 1 by norm_num)

private theorem diagonal_a_pos : diagonal {a} ≠ 0 := by
  norm_num [diagonal, Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
    Set.indicator_apply, a, d, funext_iff, Fin.forall_fin_two]

-- Reversible can be disconnected: a supported point is absorbing although
-- the target assigns positive mass to another supported point.
example : Kernel.IsReversible (randomScan diagonal) diagonal ∧
    randomScan diagonal a {a} = 1 ∧ diagonal {a} ≠ 1 := by
  refine ⟨randomScan_isReversible _, ?_, ?_⟩
  · rw [randomScan_apply_singleton diagonal a a diagonal_a_pos, Fin.sum_univ_two]
    norm_num [Fin.forall_fin_two, Fin.forall_fin_one, diagonal,
      Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
      Set.indicator_apply, a, d, funext_iff]
    rw [ENNReal.mul_inv_cancel (by norm_num) (by simp)]
    norm_num
    exact ENNReal.inv_mul_cancel (by norm_num) (by simp)
  · norm_num [diagonal, Measure.smul_apply, Measure.add_apply, Measure.dirac_apply,
      Set.indicator_apply, a, d, funext_iff, Fin.forall_fin_two]

-- Single-site (empty retained tuple) boundary.
example (μ : Measure (Fin 1 → Bool)) [IsProbabilityMeasure μ] :
    Kernel.IsReversible (randomScan μ) μ := randomScan_isReversible μ

#print axioms KernelReversibility.isReversible_of_singleton_balance
#print axioms randomScan_isReversible

end AutoSamplingTheory.Tests.RandomScanHeatBathReversibility

Source and evidence

This is original ASTIS exposition of a shared prerequisite, not a quotation or a replacement statement for a numbered source theorem. Expository coverage does not change formal completion.

Current checkout compilation not certified

Frontier Cell: independently_verified
Source comparison: source-reviewed / equivalent-after-elaboration / accepted
Registry membership: 0 of 2 displayed results; repository Registry total: 438. Compilation and Registry admission are separate.

Source correspondence and exact audit records

Levin–Peres with Wilmer, Markov Chains and Mixing Times, 2nd ed., §3.3.2, printed pp.42–43 / PDF pp.58–59 — Equations (3.6)–(3.7), with Exercise 3.2 on printed p.45 / PDF p.61: finite heat-bath update and reversibility.
Fearnhead, Nemeth, Oates, Sherlock, Scalable Monte Carlo for Bayesian Learning, §2.1.1, printed p.48 / PDF p.54 — Conditional-move balance; mixtures and deterministic compositions have different contracts.

Independent source comparison accepted the Boolean reversibility clause as equivalent-after-elaboration. Source acceptance, local compilation and Registry integration remain separate evidence fields.

Frontier Cell record · Independent source audit