Joint posterior recovery with measurable state-dependent RGO parameters

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; ASTIS expanded state-dependent joint-kernel semantics, no author endorsement implied.

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product Borel space, S any measurable space, and mu a probability measure on E. Let b,a:S to R and u:S to E be measurable, with b(s)>=0 and a(s)>0 everywhere. There exist Markov kernels T,H:S to E and B:S times E to S times E, chosen before every probability state law nu. Every T(s) is the normalized mu tilt by -b(s)*norm(x-u(s))^2/2; H(s) is its actual Gaussian smoothing at standard deviation sqrt(a(s)). Every B(s,y) retains s and draws x from the actual backward tilt of T(s) by -norm(x-y)^2/(2a(s)). Equivalently, it uses the original mu tilt with precision b(s)+1/a(s) and center (b(s)*u(s)+y/a(s))/(b(s)+1/a(s)). For every probability nu, B composed with nu compProd H equals nu compProd T.

Actual retained-state joint recovery

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Joint posterior recovery with measurable state-dependent RGO parameters

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO.state_dependent_recovery · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product Borel space, S any measurable space, and mu a probability measure on E. Let b,a:S to R and u:S to E be measurable, with b(s)≥0 and a(s)>0 everywhere. There exist Markov kernels T,H:S to E and B:S times E to S times E, chosen before every probability state law nu. Every T(s) is the normalized mu tilt by -b(s)*norm(x-u(s))^2/2; H(s) is its actual Gaussian smoothing at standard deviation sqrt(a(s)). Every B(s,y) retains s and draws x from the actual backward tilt of T(s) by -norm(x-y)^2/(2a(s)). Equivalently, it uses the original mu tilt with precision b(s)+1/a(s) and center (b(s)*u(s)+y/a(s))/(b(s)+1/a(s)). For every probability nu, B composed with nu compProd H equals nu compProd T.

\[B\circ_m(\nu\otimes_m H)=\nu\otimes_m T,\qquad T(s)=\mu.\mathrm{tilted}\!\left(-\frac{b(s)}2\|x-u(s)\|^2\right).\]

Lean statement · state_dependent_recovery

Globally measurable state-dependent RGO target, Gaussian observation and retained-state posterior with actual joint recovery.

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 state_dependent_recovery (μ : Measure E) [IsProbabilityMeasure μ]
    (b a : S → ℝ) (u : S → E) (hb : Measurable b) (ha : Measurable a)
    (hu : Measurable u) (hb0 : ∀ s, 0 ≤ b s) (ha0 : ∀ s, 0 < a s) :
    ∃ (T H : Kernel S E) (B : Kernel (S × E) (S × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ s, T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2)) ∧
      (∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        ((T s).tilted (fun x => -‖x-y‖^2/(2*a s)))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        (μ.tilted (fun x => -((b s+(a s)⁻¹)/2)*
          ‖x-(b s+(a s)⁻¹)⁻¹ • (b s • u s+(a s)⁻¹ • y)‖^2))) ∧
      ∀ (ν : Measure S), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T

Exact module and namespace context

Proof roadmap

1Normalize a jointly measurable quadratic weight
On the parameter space of nonnegative precision and center, the quadratic exponential weight is jointly measurable, strictly positive and at most one. Its integral against the probability base is therefore finite and strictly positive. The parameter integral is measurable. Divide by this integral to construct one global Markov kernel through withDensity, including zero precision.
2Use measurable current and updated parameters
Compose the same global parameter kernel with the current-state map to obtain T and with the updated state-observation map to obtain K. The new precision is positive and the weighted center is measurable. This proves joint measurability; separate existential kernels for each parameter would not suffice.
3Construct the state-dependent Gaussian observation
Retain the input state and draw an independent standard Gaussian. Map this pair to sqrt(a(s)) times the Gaussian to form N. The product of T and N followed by addition defines H. Product and pushforward formulas establish the exact smoothing fiber and Markov property.
4Identify the actual posterior and retain the state
Quadratic tilt closure identifies K with the backward tilt of T for every state and observation. Pair K with the deterministic state coordinate to form B. The already constructed section K(s,.) is identified with the existing pointwise recovery theorem; no measurable choice over pointwise witnesses is used.
5Recover the complete joint state-target law
For each measurable event in S times E, take its measurable section at a fixed state. The bind and compProd identities give the output event mass as an iterated nonnegative integral. Section recovery replaces the inner integral by T(s) of the section, yielding nu compProd T. No state coordinate or dependence is discarded.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero; mu is an arbitrary probability measure.
S has only a measurable-space structure. No topology, standard Borel condition, or moment condition on the state law is needed.
b,a,u are measurable on S, with b nonnegative and a strictly positive at every state. No fixed or deterministic schedule is imposed.
All global kernels precede the universally quantified probability state law. Both posterior formulas hold at every state and observation.
Recovery assumes the actual ideal input nu compProd H. State may encode past history and its parameters are fixed conditional on the current call input. This does not assume one predetermined schedule for all calls or construct the actual approximate sampler.

Mathematical proof

1. Normalize a jointly measurable quadratic weight

On the parameter space of nonnegative precision and center, the quadratic exponential weight is jointly measurable, strictly positive and at most one. Its integral against the probability base is therefore finite and strictly positive. The parameter integral is measurable. Divide by this integral to construct one global Markov kernel through withDensity, including zero precision.

\[w_{q,v}(x)=e^{-q\|x-v\|^2/2},\quad 0<Z(q,v)=\int w_{q,v}\,d\mu\le1,\quad R(q,v)=\frac{w_{q,v}}{Z(q,v)}\mu.\]

Corresponding Lean step

Local universalTilt: integrable_const domination, integral_exp_pos, StronglyMeasurable.integral_prod_right, Kernel.withDensity, isProbabilityMeasure_tilted.

2. Use measurable current and updated parameters

Compose the same global parameter kernel with the current-state map to obtain T and with the updated state-observation map to obtain K. The new precision is positive and the weighted center is measurable. This proves joint measurability; separate existential kernels for each parameter would not suffice.

\[q^+(s)=b(s)+a(s)^{-1}>0,\quad c(s,y)=q^+(s)^{-1}\bigl(b(s)u(s)+a(s)^{-1}y\bigr),\quad K(s,y)=R(q^+(s),c(s,y)).\]

Corresponding Lean step

Measurable.subtype_mk, Measurable.prodMk, Kernel.comap; local t,q,c,r and hKupdated.

3. Construct the state-dependent Gaussian observation

Retain the input state and draw an independent standard Gaussian. Map this pair to sqrt(a(s)) times the Gaussian to form N. The product of T and N followed by addition defines H. Product and pushforward formulas establish the exact smoothing fiber and Markov property.

\[N(s)=\operatorname{Law}(\sqrt{a(s)}G),\qquad H(s)=\operatorname{Law}(X+\sqrt{a(s)}G),\quad X\sim T(s),\ G\sim\mathsf N(0,I)\text{ independently}.\]

Corresponding Lean step

Kernel.deterministic, Kernel.const, Kernel.prod, Kernel.map, Kernel.IsMarkovKernel.map; Measure.dirac_prod and Measure.map_map.

4. Identify the actual posterior and retain the state

Quadratic tilt closure identifies K with the backward tilt of T for every state and observation. Pair K with the deterministic state coordinate to form B. The already constructed section K(s,.) is identified with the existing pointwise recovery theorem; no measurable choice over pointwise witnesses is used.

\[K(s,y)=T(s).\mathrm{tilted}\!\left(-\frac{\|x-y\|^2}{2a(s)}\right),\quad B(s,y)=(x\mapsto(s,x))_\#K(s,y),\quad K(s,\cdot)\circ_mH(s)=T(s).\]

Corresponding Lean step

RGOClosure.quadratic_tilt_tilt, RGOBackward.rgo_backward_recovery; local hKf,hBf,hrec and kernel extensionality.

5. Recover the complete joint state-target law

For each measurable event in S times E, take its measurable section at a fixed state. The bind and compProd identities give the output event mass as an iterated nonnegative integral. Section recovery replaces the inner integral by T(s) of the section, yielding nu compProd T. No state coordinate or dependence is discarded.

\[\int_S\!\int_E B(s,y)(A)\,H(s)(dy)\,\nu(ds)=\int_S T(s)(A_s)\,\nu(ds).\]

Corresponding Lean step

Measure.bind_apply, Measure.lintegral_compProd, Measure.compProd_apply, Measure.map_apply, lintegral_congr.

Lean verification

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

Lean proof · state_dependent_recovery

Construct a normalized parameter kernel, comap along measurable current and updated states, construct actual variable Gaussian noise, identify posterior fibers and integrate section recovery.

Download module (.lean)

theorem state_dependent_recovery (μ : Measure E) [IsProbabilityMeasure μ]
    (b a : S → ℝ) (u : S → E) (hb : Measurable b) (ha : Measurable a)
    (hu : Measurable u) (hb0 : ∀ s, 0 ≤ b s) (ha0 : ∀ s, 0 < a s) :
    ∃ (T H : Kernel S E) (B : Kernel (S × E) (S × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ s, T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2)) ∧
      (∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        ((T s).tilted (fun x => -‖x-y‖^2/(2*a s)))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        (μ.tilted (fun x => -((b s+(a s)⁻¹)/2)*
          ‖x-(b s+(a s)⁻¹)⁻¹ • (b s • u s+(a s)⁻¹ • y)‖^2))) ∧
      ∀ (ν : Measure S), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T := by
  have universalTilt : ∃ R : Kernel (ℝ≥0 × E) E, IsMarkovKernel R ∧
      ∀ s, R s = μ.tilted (fun x => -((s.1 : ℝ)/2)*‖x-s.2‖^2) := by
    let w : (ℝ≥0 × E) → E → ℝ := fun s x => Real.exp (-((s.1 : ℝ) / 2) * ‖x-s.2‖^2)
    have hw : Measurable (Function.uncurry w) := by
      dsimp [w, Function.uncurry]
      fun_prop
    have hI (s : (ℝ≥0 × E)) : Integrable (w s) μ := by
      refine (integrable_const (1 : ℝ)).mono' (by fun_prop) ?_
      filter_upwards with x
      rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
      exact Real.exp_le_one_iff.mpr (mul_nonpos_of_nonpos_of_nonneg
        (neg_nonpos.mpr (div_nonneg s.1.coe_nonneg (by positivity))) (sq_nonneg _))
    let Z : (ℝ≥0 × E) → ℝ := fun s => ∫ x, w s x ∂μ
    have hZpos (s : (ℝ≥0 × E)) : 0 < Z s := integral_exp_pos (hI s)
    have hZ : Measurable Z := hw.stronglyMeasurable.integral_prod_right.measurable
    let d : (ℝ≥0 × E) → E → ℝ≥0∞ := fun s x => ENNReal.ofReal (w s x / Z s)
    have hd : Measurable (Function.uncurry d) :=
      (hw.div (hZ.comp measurable_fst)).ennreal_ofReal
    let T : Kernel (ℝ≥0 × E) E := (Kernel.const (ℝ≥0 × E) μ).withDensity d
    have hf (s : (ℝ≥0 × E)) : T s = μ.tilted (fun x => -((s.1 : ℝ) / 2) * ‖x-s.2‖^2) := by
      rw [show T = (Kernel.const (ℝ≥0 × E) μ).withDensity d from rfl,
        Kernel.withDensity_apply _ hd]
      rfl
    refine ⟨T, ⟨fun s => ?_⟩, hf⟩
    rw [hf]
    exact isProbabilityMeasure_tilted (hI s)
  obtain ⟨R,hR,hRf⟩ := universalTilt
  let := hR
  let t : S → ℝ≥0 × E := fun s => (⟨b s, hb0 s⟩, u s)
  have ht : Measurable t := (hb.subtype_mk).prodMk hu
  let T := R.comap t ht
  have hT : IsMarkovKernel T := inferInstance
  have hTf (s : S) : T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2) := hRf (t s)
  let := hT
  let q : S × E → ℝ := fun p => b p.1 + (a p.1)⁻¹
  let c : S × E → E := fun p => (b p.1+(a p.1)⁻¹)⁻¹ •
    (b p.1 • u p.1+(a p.1)⁻¹ • p.2)
  have hq : Measurable q := by dsimp [q]; fun_prop
  have hc : Measurable c := by dsimp [c]; fun_prop
  have hq0 (p : S × E) : 0 ≤ q p :=
    le_of_lt (add_pos_of_nonneg_of_pos (hb0 p.1) (inv_pos.mpr (ha0 p.1)))
  let r : S × E → ℝ≥0 × E := fun p => (⟨q p, hq0 p⟩, c p)
  have hr : Measurable r := (hq.subtype_mk).prodMk hc
  let K := R.comap r hr
  have hK : IsMarkovKernel K := inferInstance
  have hKupdated (p : S × E) : K p = μ.tilted (fun x => -(q p/2)*‖x-c p‖^2) := hRf (r p)
  let := hK
  let N : Kernel S E :=
    ((Kernel.deterministic (id : S → S) measurable_id) ×ₖ Kernel.const S (stdGaussian E)).map
      (fun p : S × E => Real.sqrt (a p.1) • p.2)
  have hN : IsMarkovKernel N := by
    dsimp only [N]
    exact Kernel.IsMarkovKernel.map _ (by fun_prop)
  let := hN
  have hNf (s : S) : N s = GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt (a s)) := by
    dsimp only [N]
    rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.deterministic_apply,
      Kernel.const_apply, Measure.dirac_prod, Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  let H := (T ×ₖ N).map (fun p : E × E => p.1+p.2)
  have hH : IsMarkovKernel H := by
    dsimp only [H]
    exact Kernel.IsMarkovKernel.map _ (by fun_prop)
  let := hH
  have hHf (s : S) : H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s)) := by
    dsimp only [H]
    rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, hNf]
    rfl
  have hKf (s : S) (y : E) : K (s,y) =
      (T s).tilted (fun x => -‖x-y‖^2/(2*a s)) := by
    rw [hKupdated,hTf]
    have heq : (fun x : E => -‖x-y‖^2/(2*a s)) =
        (fun x => -((a s)⁻¹/2)*‖x-y‖^2) := by
      funext x
      field_simp
    rw [heq]
    exact (RGOClosure.quadratic_tilt_tilt μ (hb0 s) (inv_pos.mpr (ha0 s)) (u s) y).symm
  let B := (Kernel.deterministic (Prod.fst : S × E → S) measurable_fst) ×ₖ K
  have hB : IsMarkovKernel B := inferInstance
  let := hB
  have hBf (s : S) (y : E) : B (s,y) = Measure.map (Prod.mk s) (K (s,y)) := by
    dsimp only [B]
    rw [Kernel.prod_apply, Kernel.deterministic_apply, Measure.dirac_prod]
  have hrec (s : S) : (K.comap (Prod.mk s) measurable_prodMk_left) ∘ₘ H s = T s := by
    obtain ⟨_,R,hR,hRf,_,hrecover,_⟩ :=
      RGOBackward.rgo_backward_recovery μ (b s) (a s) (hb0 s) (ha0 s) (u s)
    have heq : K.comap (Prod.mk s) measurable_prodMk_left = R := by
      ext y : 1
      change K (s,y) = R y
      rw [hKf,hTf,hRf]
    rw [heq,hHf,hTf]
    exact hrecover
  refine ⟨T,H,B,hT,hH,hB,hTf,hHf,?_,?_,?_⟩
  · intro s y
    rw [hBf,hKf]
  · intro s y
    rw [hBf,hKupdated]
  · intro ν hν
    let := hν
    ext t ht
    rw [Measure.bind_apply ht B.aemeasurable, Measure.lintegral_compProd (B.measurable_coe ht),
      Measure.compProd_apply ht]
    apply lintegral_congr
    intro s
    have ht' := ht.preimage (measurable_prodMk_left (x := s))
    have heq := congrArg (fun m : Measure E => m ((Prod.mk s) ⁻¹' t)) (hrec s)
    rw [Measure.bind_apply ht' (K.comap (Prod.mk s) measurable_prodMk_left).aemeasurable] at heq
    rw [← heq]
    apply lintegral_congr
    intro y
    rw [hBf,Measure.map_apply measurable_prodMk_left ht]
    rfl

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Algorithm3.3 uses a Euclidean Gibbs base target.	Arbitrary probability base mu on finite-dimensional real inner-product Borel E, including dimension zero.	generalization	Exact quadratic posterior recovery does not need a potential, curvature, density or moments; concrete Gibbs identification remains separate.
The current recursive target has center u and precision 1/A; new variance is (eta+tau)/beta_A.	Measurable b,a,u on arbitrary measurable S, with b>=0 and a>0 everywhere.	source-implicit	State can encode current history. Parameters are not assumed constant; actual source parameter maps and report/output semantics must still be instantiated.
The RGO closure updates inverse variance and center.	Both everywhere posterior formulas use b(s)+1/a(s) and weighted center (b(s)u(s)+y/a(s))/(b(s)+1/a(s)).	same	The normalized tilt composition is proved, including b(s)=0, without assuming posterior normalization.
The ideal Gaussian observation and posterior stage underpin recursive correctness.	Construct globally measurable T,H,B before every state distribution; B retains s and B composed with nu compProd H equals nu compProd T.	source-implicit	Joint normalized parameter kernel, state-dependent Gaussian law and full joint recovery are proved rather than assumed or selected pointwise.
The interface selects eta for each fixed call input and supplies a sample; the full algorithm recurses, terminates with FORS and has discrepancy/cost guarantees.	Exact ideal nu compProd H input for measurable current-state parameters, fixed conditional on the call input.	API-limitation	Actual output sampler kernels, recursion and stopping, terminal implementation, accuracy and expected costs remain open. This is a required kernel semantics edge, not full Algorithm3.3.

Fixed probability base, arbitrary measurable state space and measurable current-state parameters. Exact ideal joint observation law only. The source interface selects a smoothing level for each fixed call input; this theorem does not construct its actual output sampler, recursive stopping, FORS, numerical accuracy or expected query costs.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: General probability base and finite-dimensional Hilbert setting; no moments inferred. — No Gibbs density, topology or standard Borel structure on S; integration uses event sections rather than state disintegration.
assumptions: Measurable state maps abstract actual source parameters; their concrete instantiation remains. — hI domination, hZpos positive normalizer, hZ/hd measurability and proved RGO section recovery.
conclusion: Everywhere normalized posterior includes b=0; a=0 excluded. — Arbitrary measurable events and sections, bind and compProd integrals retain the state coordinate.
quantifiers: Complete retained-state recovery for every state law is an explicit ideal-stage elaboration. — Fixed-state witness only identifies an already constructed global section.
scopes: Eta selected per fixed call input; random runtime report extension is not asserted to be a required paper gap. Full sampler remains open. — Binding is prerequisite; documentation excludes complete algorithm and numerical/cost guarantees.

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

Fixed probability base, arbitrary measurable state space and measurable current-state parameters. Exact ideal joint observation law only. The source interface selects a smoothing level for each fixed call input; this theorem does not construct its actual output sampler, recursive stopping, FORS, numerical accuracy or expected query costs.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral_exp_pos
MeasureTheory.isProbabilityMeasure_tilted
ProbabilityTheory.Kernel.withDensity
ProbabilityTheory.Kernel.comap
ProbabilityTheory.Kernel.prod
ProbabilityTheory.Kernel.map
MeasureTheory.Measure.lintegral_compProd
MeasureTheory.Measure.bind_apply

Mathematical sources

SPHMC v1 Algorithm 3.3 and Theorem 6.5 — Expanded ideal stage semantics with measurable state-dependent parameters; not the full recursive algorithm.

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

Joint posterior recovery with measurable state-dependent RGO parameters

Complete source statement (Samplinglib restatement)

Actual retained-state joint recovery

Read the formalized proofs

Joint posterior recovery with measurable state-dependent RGO parameters

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Normalize a jointly measurable quadratic weight

2. Use measurable current and updated parameters

3. Construct the state-dependent Gaussian observation

4. Identify the actual posterior and retain the state

5. Recover the complete joint state-target law

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?