From atomic balance to reversibility

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.

/- 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 : α)

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)

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

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