From conditional detailed balance to a retained-coordinate joint kernel
AutoSamplingTheory.TechnicalLemmas.Probability.KernelRetainedReversibility.retained_coordinate_isReversible · theorem · Teaching coverage
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.
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.
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)Proof roadmap
- 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.
- 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.
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.
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.
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.KernelRetainedReversibilitySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Standard source-neutral s-finite/a.e. detailed-balance contract, not a complete paper theorem. | Arbitrary measurable A,B; SFinite mu; s-finite R and joint F; a.e. fiber IsReversible. | same | These are the explicit premises of the shared theorem. Paper adapters must discharge them using the actual produced laws. |
| Nonnegative disintegration and deterministic product in the standard s-finite setting. | SFinite mu and IsSFiniteKernel R,F. | API-limitation | These classes give the intended semantics of the pinned compProd/product APIs; no use of their totalized zero fallbacks outside scope. |
| Actual PBPS operator A.2/A.9 and quantitative paper results. | 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. | unresolved | This lemma alone has no actual process witness, coordinate-transport or L2 operator; no paper completion follows. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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
- Pinned Mathlib detailed-balance and compProd definitions; ASTIS standard derived theorem — 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.
- PBPS A.2/A.9: motivating actual half-turn consumer only — Actual disintegration, swap transport and all-L2 realization are separate red adapters.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.