Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / sampling

sogb-001 · public-dev · editorial and formal status separate

From atomic balance to reversibility

Markov Chain Monte Carlo / Discrete Sampling · natural-language: L3 / lean: L3 (author-assigned; calibration pending)

Why this difficulty?

Coordinate two nonnegative countable expansions, justify their exchange and audit infinite/null masses; Lean also reconstructs that argument.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • The target states only reversibility, not the natural-language explanations of why division/cancellation are unnecessary or explicit counterexamples to normalization, irreducibility and convergence implications.
  • No normalization, mixing, query-cost or empirical difficulty claim is formalized by this view.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • The state space is countable, carries a measurable space, and every singleton is measurable.
  • \(\mu\) is a nonnegative measure and \(K\) is a measurable kernel; neither is assumed finite or normalized.
  • For every pair \(x,y\), \(\mu(\{x\})K(x,\{y\})=\mu(\{y\})K(y,\{x\})\) in the extended nonnegative reals.

Natural-language question

Prove that for all measurable sets A,B, \(\int_A K(x,B)\,d\mu(x)=\int_B K(y,A)\,d\mu(y)\). Explain why infinite total mass and zero-mass states cause no cancellation problem. Does this imply convergence to a probability law?

Reference mathematical proof

  1. On a countable measurable-singleton space, expand each restricted integral and each kernel mass into singleton masses. The left side becomes \[\sum_{x\in A}\sum_{y\in B}K(x,\{y\})\mu(\{x\}).\] These sums take values in \([0,\infty]\).

  2. Apply the assumed balance identity to each summand. Nonnegativity permits exchanging the two sums even when the result is infinite: \[\sum_{x\in A}\sum_{y\in B}\mu(\{y\})K(y,\{x\})=\sum_{y\in B}K(y,A)\mu(\{y\}).\]

  3. Recognize the last expression as the right restricted integral. No division by a singleton mass, subtraction of infinities, or signed Fubini argument occurred. A zero atom needs no special conditional version for this flux identity.

  4. Reversibility alone proves neither normalization, irreducibility, convergence, nor a mixing or query-cost bound. Those require separate assumptions and arguments.

How the Lean proof follows these steps

The binders in square brackets supply the measurable and countable structures. The hypothesis h is pairwise flux balance. The proof expands countable lintegrals, rewrites kernel masses as sums, then uses ENNReal.tsum_comm and h. The final proposition is Mathlib's kernel reversibility, not a mixing theorem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Probability.Kernel.Invariance
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

open MeasureTheory ProbabilityTheory
open scoped ENNReal

example {α : 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 : α)

Download runnable reference

Assessment rubric · 4 points
  1. States the countability and measurable-singleton hypotheses and uses nonnegative extended-valued sums. (1 point)
  2. Expands both the outer restricted integral and the inner kernel mass. (1 point)
  3. Uses balance termwise and justifies sum exchange without dividing by masses or subtracting infinities. (1 point)
  4. Separates reversibility from normalization, convergence and computational cost. (1 point)

Lean question

Keep the target and context fixed; replace the comment slot with your proof. Ancestor libraries are allowed, but the target module is not imported directly.

Show fixed Lean task
/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Probability.Kernel.Invariance
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

open MeasureTheory ProbabilityTheory
open scoped ENNReal

example {α : Type*} [MeasurableSpace α]
    [Countable α] [MeasurableSingletonClass α] (κ : Kernel α α) (μ : Measure α)
    (h : ∀ x y, μ {x} * κ x {y} = μ {y} * κ y {x}) :
    Kernel.IsReversible κ μ := by
  -- Replace this comment with your proof.

Download task template

Reference Lean and explanation

The binders in square brackets supply the measurable and countable structures. The hypothesis h is pairwise flux balance. The proof expands countable lintegrals, rewrites kernel masses as sums, then uses ENNReal.tsum_comm and h. The final proposition is Mathlib's kernel reversibility, not a mixing theorem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Probability.Kernel.Invariance
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

open MeasureTheory ProbabilityTheory
open scoped ENNReal

example {α : 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 : α)

Download runnable reference

No current trusted-reference compiler receipt recorded in this build.

What this does—and does not—verify

The Lean target covers the flux identity. The explanatory non-implications are assessed in the natural-language track, not certified by that Lean target.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original exercise over the existing Samplinglib declaration; not a quotation of a paper theorem.

Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)

AutoSamplingTheory.TechnicalLemmas.Probability.KernelReversibility.isReversible_of_singleton_balance

ASTIS definitions / proof calls

    Mathlib facts / definitions

    • lintegral_countable
    • ENNReal.tsum_mul_right
    • ENNReal.tsum_comm
    • tsum_congr

    Binding SHA-256: ac978a2c81f53d2c0ce45bb253fdafd93de190bb9ff64e1eab954ea9e29249b8