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

KernelRetainedReversibility: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. From conditional detailed balance to a retained-coordinate joint kernel
Samplinglib mathematical lesson

From conditional detailed balance to a retained-coordinate joint kernel

AutoSamplingTheory.TechnicalLemmas.Probability.KernelRetainedReversibility.retained_coordinate_isReversible · theorem · Teaching coverage

Read this first

Mathematical statement

Let \(A,B\) be arbitrary measurable spaces, \(\mu\) an s-finite measure on \(A\), \(R:A\rightsquigarrow B\) an s-finite kernel, and \(F:A\times B\rightsquigarrow B\) a jointly measurable s-finite kernel. Suppose that, for \(\mu\)-almost every \(a\), the kernel \(F_a(b,\cdot)=F((a,b),\cdot)\) is reversible under \(R(a,\cdot)\), in the sense of equality of nonnegative fluxes between every pair of measurable subsets of \(B\). Put \(\nu(da,db)=\mu(da)R(a,db)\). Then the transition \(L((a,b),d(a\prime,b\prime))=\delta_a(da\prime)F((a,b),db\prime)\), which retains the first coordinate, is reversible under \(\nu\). Neither the measures nor the kernels need be normalized or finite; zero measures, empty spaces and infinite fluxes are allowed.

\[\nu=\mu\otimes_m R,\qquad L((a,b),d(a\prime,b\prime))=\delta_a(da\prime)F((a,b),db\prime),\qquad\int_S L(z,T)\,\nu(dz)=\int_T L(z,S)\,\nu(dz).\]
Lean statement · retained_coordinate_isReversible

Let \(A,B\) be arbitrary measurable spaces, \(\mu\) an s-finite measure on \(A\), \(R:A\rightsquigarrow B\) an s-finite kernel, and \(F:A\times B\rightsquigarrow B\) a jointly measurable s-finite kernel. Suppose that, for \(\mu\)-almost every \(a\), the kernel \(F_a(b,\cdot)=F((a,b),\cdot)\) is reversible under \(R(a,\cdot)\), in the sense of equality of nonnegative fluxes between every pair of measurable subsets of \(B\). Put \(\nu(da,db)=\mu(da)R(a,db)\). Then the transition \(L((a,b),d(a\prime,b\prime))=\delta_a(da\prime)F((a,b),db\prime)\), which retains the first coordinate, is reversible under \(\nu\). Neither the measures nor the kernels need be normalized or finite; zero measures, empty spaces and infinite fluxes are allowed.

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.

Download module (.lean)
theorem retained_coordinate_isReversible
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [SFinite μ]
    (R : Kernel A B) [IsSFiniteKernel R]
    (F : Kernel (A × B) B) [IsSFiniteKernel F]
    (hF : ∀ᵐ a ∂μ, (F.comap (fun b => (a, b))
      (measurable_const.prodMk measurable_id)).IsReversible (R a)) :
    ((Kernel.deterministic Prod.fst measurable_fst) ×ₖ F).IsReversible (μ ⊗ₘ R)

Exact module and namespace context

Proof roadmap

  1. 1Disintegrate the flux through measurable sections

    Fix arbitrary measurable joint sets S,T, and define their sections S_a={b:(a,b) belongs to S} and T_a similarly. Each section is measurable because b maps to (a,b) measurably. The function z maps to L(z,T) is measurable since L is a kernel. Replace its restricted integral over S by the integral of the measurable indicator-weighted function. Nonnegative compProd integration then separates the retained coordinate a and the updated coordinate b. The deterministic first-coordinate kernel forces the new first coordinate to equal a, so L((a,b),T)=F((a,b),T_a). Restricting the inner integral to S_a gives exactly the displayed identity.

  2. 2Apply fiber balance almost everywhere, then reassemble

    For almost every retained coordinate a, apply the assumed reversible-kernel equality to the measurable sets S_a and T_a. This equates the two inner fluxes. Equality almost everywhere suffices to equate their outer nonnegative integrals. Apply the previous disintegration identity once to S,T and once to T,S. The resulting equality is the definition of joint reversibility. No subtraction of infinite quantities and no exchange of signed integrals occurs.

Full assumptions and notation

All objects and hypotheses

  • A kernel includes genuine measurability for every measurable output set. Joint measurability of F is a real premise encoded by its type; separate fiber measurability would not suffice for the disintegration argument.
  • The s-finite assumptions select the meaningful pinned Mathlib compProd and kernel-product interfaces. They are not asserted to be logically minimal for every possible independently defined extension. Outside these classes, totalized zero defaults must not be used as mathematical evidence.
  • The fiber detailed-balance premise holds simultaneously for all measurable fiber sets outside one mu-null set. Its good set needs no separately supplied measurability certificate. Joint-set sections are measurable preimages, not projections.
  • No Markov, probability, finite-mass, sigma-finite, Standard-Borel, topology, measurable-singleton, nonempty or real-integrability premise is present. All flux integrals are nonnegative and may be infinite.
  • This shared theorem does not construct a paper-specific conditional law. An actual PBPS or Gibbs adapter must identify its SAME selected R and joint disintegration. Detailed balance alone, without Markovness, is not an invariance assertion.

Mathematical proof

1. Disintegrate the flux through measurable sections

Fix arbitrary measurable joint sets S,T, and define their sections S_a={b:(a,b) belongs to S} and T_a similarly. Each section is measurable because b maps to (a,b) measurably. The function z maps to L(z,T) is measurable since L is a kernel. Replace its restricted integral over S by the integral of the measurable indicator-weighted function. Nonnegative compProd integration then separates the retained coordinate a and the updated coordinate b. The deterministic first-coordinate kernel forces the new first coordinate to equal a, so L((a,b),T)=F((a,b),T_a). Restricting the inner integral to S_a gives exactly the displayed identity.

\[\begin{aligned}S_a&=\{b:(a,b)\in S\},\qquad T_a=\{b:(a,b)\in T\},\\ \int_S L(z,T)\,\nu(dz)&=\int_A\int_B\mathbf1_S(a,b)L((a,b),T)\,R(a,db)\,\mu(da)\\ &=\int_A\int_{S_a}F_a(b,T_a)\,R(a,db)\,\mu(da).\end{aligned}\]
Corresponding Lean step
private theorem retained_flux
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [SFinite μ]
    (R : Kernel A B) [IsSFiniteKernel R]
    (F : Kernel (A × B) B) [IsSFiniteKernel F]
    {S T : Set (A × B)} (hS : MeasurableSet S) (hT : MeasurableSet T) :
    (∫⁻ z in S, ((Kernel.deterministic Prod.fst measurable_fst) ×ₖ F) z T
      ∂(μ ⊗ₘ R)) =
    ∫⁻ a, ∫⁻ b in Prod.mk a ⁻¹' S, F (a, b) (Prod.mk a ⁻¹' T) ∂R a ∂μ := by
  rw [← lintegral_indicator hS]
  rw [Measure.lintegral_compProd
    ((((Kernel.deterministic Prod.fst measurable_fst) ×ₖ F).measurable_coe hT).indicator hS)]
  apply lintegral_congr
  intro a
  rw [← lintegral_indicator (hS.preimage measurable_prodMk_left)]
  apply lintegral_congr
  intro b
  by_cases hab : (a, b) ∈ S
  · rw [Set.indicator_of_mem hab,
      Set.indicator_of_mem (show b ∈ Prod.mk a ⁻¹' S from hab)]
    exact Kernel.deterministic_prod_apply' measurable_fst F (a, b) hT
  · rw [Set.indicator_of_notMem hab,
      Set.indicator_of_notMem (show b ∉ Prod.mk a ⁻¹' S from hab)]

This step proves the formula for arbitrary joint sets, not only rectangles. The Lean helper uses lintegral_indicator and lintegral_compProd; the rectangular setLIntegral_compProd theorem is deliberately not used. In its last case split, membership in S and in S_a are definitionally the same condition.

2. Apply fiber balance almost everywhere, then reassemble

For almost every retained coordinate a, apply the assumed reversible-kernel equality to the measurable sets S_a and T_a. This equates the two inner fluxes. Equality almost everywhere suffices to equate their outer nonnegative integrals. Apply the previous disintegration identity once to S,T and once to T,S. The resulting equality is the definition of joint reversibility. No subtraction of infinite quantities and no exchange of signed integrals occurs.

\[\begin{aligned}\int_{S_a}F_a(b,T_a)\,R(a,db)&=\int_{T_a}F_a(b,S_a)\,R(a,db)\quad(\mu\text{-a.e. }a),\\ \int_S L(z,T)\,\nu(dz)&=\int_A\int_{T_a}F_a(b,S_a)\,R(a,db)\,\mu(da)\\ &=\int_T L(z,S)\,\nu(dz).\end{aligned}\]
Corresponding Lean step
  intro S T hS hT
  rw [retained_flux μ R F hS hT, retained_flux μ R F hT hS]
  apply lintegral_congr_ae
  filter_upwards [hF] with a ha
  exact ha (hS.preimage measurable_prodMk_left) (hT.preimage measurable_prodMk_left)

In Lean, filter_upwards obtains a fiber satisfying detailed balance; the two measurable-preimage proofs make its section sets admissible. lintegral_congr_ae performs the outer integration. The public theorem does not add a pointwise reversibility or a Markov premise.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · retained_coordinate_isReversible

Joint-set indicator -> compProd Tonelli -> fiber flux -> a.e. conditional balance -> reverse disintegration.

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.

Download module (.lean)
theorem retained_coordinate_isReversible
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [SFinite μ]
    (R : Kernel A B) [IsSFiniteKernel R]
    (F : Kernel (A × B) B) [IsSFiniteKernel F]
    (hF : ∀ᵐ a ∂μ, (F.comap (fun b => (a, b))
      (measurable_const.prodMk measurable_id)).IsReversible (R a)) :
    ((Kernel.deterministic Prod.fst measurable_fst) ×ₖ F).IsReversible (μ ⊗ₘ R) := by
  intro S T hS hT
  rw [retained_flux μ R F hS hT, retained_flux μ R F hT hS]
  apply lintegral_congr_ae
  filter_upwards [hF] with a ha
  exact ha (hS.preimage measurable_prodMk_left) (hT.preimage measurable_prodMk_left)

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelRetainedReversibility

Exact module and namespace context

Scope and omitted-condition boundaries
  • Detailed-balance gluing only. No invariance without Markovness, no coordinate-swap transport, actual PBPS A.2 operator, full-K reversibility, restart/semigroup, rate, error/cap/cost, initialization/composition or full paper.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • MeasureTheory.Measure.lintegral_compProd
    • ProbabilityTheory.Kernel.deterministic_prod_apply'
    • MeasureTheory.lintegral_indicator
    • MeasureTheory.lintegral_congr_ae
    • measurable_prodMk_left

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.