One actual RGO backward kernel: precision update, recovery and KL control

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; ASTIS expanded proof, no author endorsement implied.

Complete source statement (Samplinglib restatement)

Let mu be a probability measure on a finite-dimensional real inner-product Borel space, b>=0, a>0 and u a point. Define rho as mu tilted by -b*norm(x-u)^2/2. Then rho is a probability measure and there exists one Markov kernel K, chosen before every input law and radius, with K(y)=rho.tilted(-norm(x-y)^2/(2a)) at every y, equivalently mu tilted with precision b+a^-1 and center (b+a^-1)^-1 times (b*u+a^-1*y). The actual composition K with GaussianSmoothing rho sqrt(a) equals rho. For all probability nu and r>=0 with actual infimum quadratic displacement cost from nu to rho at most ofReal(r^2), the actual KL of K composed with GaussianSmoothing nu sqrt(a) relative to rho is at most ofReal(r^2/(2a)).

Actual backward recovery and KL input guarantee

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

One actual RGO backward kernel: precision update, recovery and KL control

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward.rgo_backward_recovery · theorem · Teaching coverage

Read this first

Mathematical statement

Let mu be a probability measure on a finite-dimensional real inner-product Borel space, b≥0, a>0 and u a point. Define rho as mu tilted by -b*norm(x-u)^2/2. Then rho is a probability measure and there exists one Markov kernel K, chosen before every input law and radius, with K(y)=rho.tilted(-norm(x-y)^2/(2a)) at every y, equivalently mu tilted with precision b+a^-1 and center (b+a^-1)^-1 times (b*u+a^-1*y). The actual composition K with GaussianSmoothing rho sqrt(a) equals rho. For all probability nu and r≥0 with actual infimum quadratic displacement cost from nu to rho at most ofReal(r^2), the actual KL of K composed with GaussianSmoothing nu sqrt(a) relative to rho is at most ofReal(r^2/(2a)).

\[K_aH_a\rho=\rho,\qquad \inf_{\gamma\in\Pi(\nu,\rho)}\int\|x-y\|^2d\gamma\le r^2\ \Longrightarrow\ \operatorname{KL}(K_aH_a\nu\|\rho)\le\frac{r^2}{2a}.\]

Lean statement · rgo_backward_recovery

One actual Markov kernel has every-point normalized precision update, exact recovery, and all quadratic-budget KL guarantees.

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 rgo_backward_recovery {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧ ∃ K : Kernel E E, IsMarkovKernel K ∧
      (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*a))) ∧
      (∀ y, K y = μ.tilted (fun x => -((b+a⁻¹)/2)*
        ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2)) ∧
      K ∘ₘ GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt a) = ρ ∧
      ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
        Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) ν ρ ≤
          ENNReal.ofReal (r^2) →
        InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt a)) ρ ≤
          ENNReal.ofReal (r^2/(2*a))

Exact module and namespace context

Proof roadmap

1Normalize the initial quadratic tilt
The exponential weight is positive and at most one. Its integrability under the probability base proves that the normalized tilted law rho is a probability, including zero precision.
2Construct the same measurable backward kernel
Apply the existing actual Gaussian conditional-kernel construction to rho. It supplies a Markov kernel with a normalized fiber at every y, and disintegrates the swapped joint law of (X,X+sqrt(a)Z).
3Identify actual forward and backward marginals
The first marginal of J is rho. Product-map composition identifies its second marginal with the existing GaussianSmoothing operator. These are actual pushforward equalities, not assumed stochastic semantics.
4Recover the target by disintegration
Take the second marginal of the disintegration identity for the swapped joint law. That second marginal is the original target, while its first marginal is the noisy law. This proves exact recovery for the constructed kernel.
5Identify every normalized source precision update
Write the backward precision as a^-1 and apply normalized quadratic tilt composition to the same kernel fiber. The summed precision is positive, so the updated center is valid even when b=0.
6Propagate the actual input KL budget
For any admissible input, derive probability of the smoothed measures, apply KL contraction through the same Markov kernel, substitute exact recovery, and invoke the already proved Gaussian KL reverse-transport bound.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel space, including dimension zero; mu is a probability measure.
b≥0, a>0 and arbitrary u. Precision b=0 retains the source A=infinity case.
The kernel is selected before all probability inputs nu and radii r≥0. The budget is transportCost(nu,rho), in that direction.
General probability base abstracts the source Gibbs presentation; no concrete potential identification is included.
Actual raw infimum cost is used, without inferring marginal P2 membership or claiming full W2 API correspondence.

Mathematical proof

1. Normalize the initial quadratic tilt

The exponential weight is positive and at most one. Its integrability under the probability base proves that the normalized tilted law rho is a probability, including zero precision.

\[0<e^{-b\|x-u\|^2/2}\le1,\qquad \rho=\frac{e^{-b\|x-u\|^2/2}\mu}{\int e^{-b\|x-u\|^2/2}d\mu}.\]

Corresponding Lean step

hi and isProbabilityMeasure_tilted derive hρ; no normalizer premise.

2. Construct the same measurable backward kernel

Apply the existing actual Gaussian conditional-kernel construction to rho. It supplies a Markov kernel with a normalized fiber at every y, and disintegrates the swapped joint law of (X,X+sqrt(a)Z).

\[J=\mathcal L(X,X+\sqrt a Z),\quad K(y,dx)\propto e^{-\|x-y\|^2/(2a)}\rho(dx).\]

Corresponding Lean step

GaussianConditionalKernel.exists_tilted_isCondKernel provides hK, hfiber and hcond.

3. Identify actual forward and backward marginals

The first marginal of J is rho. Product-map composition identifies its second marginal with the existing GaussianSmoothing operator. These are actual pushforward equalities, not assumed stochastic semantics.

\[J_1=\rho,\qquad J_2=H_a\rho.\]

Corresponding Lean step

hfst uses fst_map_prodMk and fst_prod; hsnd uses snd_map_prodMk, map_prod_map and map_map.

4. Recover the target by disintegration

Take the second marginal of the disintegration identity for the swapped joint law. That second marginal is the original target, while its first marginal is the noisy law. This proves exact recovery for the constructed kernel.

\[(H_a\rho)\otimes K=\operatorname{swap}_\#J\quad\Longrightarrow\quad K H_a\rho=\rho.\]

Corresponding Lean step

congrArg Measure.snd hcond.disintegrate; snd_compProd, fst_map_swap and snd_map_swap.

5. Identify every normalized source precision update

Write the backward precision as a^-1 and apply normalized quadratic tilt composition to the same kernel fiber. The summed precision is positive, so the updated center is valid even when b=0.

\[b^+=b+a^{-1},\quad u^+(y)=(b+a^{-1})^{-1}(bu+a^{-1}y),\quad K(y)=\mu.\mathrm{tilted}(-b^+\|x-u^+(y)\|^2/2).\]

Corresponding Lean step

hfiber, exact denominator algebra and RGOClosure.quadratic_tilt_tilt with inv_pos.mpr ha.

6. Propagate the actual input KL budget

For any admissible input, derive probability of the smoothed measures, apply KL contraction through the same Markov kernel, substitute exact recovery, and invoke the already proved Gaussian KL reverse-transport bound.

\[\operatorname{KL}(K H_a\nu\|\rho)\le\operatorname{KL}(H_a\nu\|H_a\rho)\le r^2/(2a).\]

Corresponding Lean step

InformationTheory.klDiv_comp_right_le and GaussianKL.gaussian_kl_reverse_transport; no approximate kernel or unbounded-cost transfer.

Lean verification

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

Lean proof · rgo_backward_recovery

Actual Gaussian disintegration and marginal identities, normalized tilt composition, then same-kernel KL data processing.

Download module (.lean)

theorem rgo_backward_recovery {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧ ∃ K : Kernel E E, IsMarkovKernel K ∧
      (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*a))) ∧
      (∀ y, K y = μ.tilted (fun x => -((b+a⁻¹)/2)*
        ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2)) ∧
      K ∘ₘ GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt a) = ρ ∧
      ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
        Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) ν ρ ≤
          ENNReal.ofReal (r^2) →
        InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt a)) ρ ≤
          ENNReal.ofReal (r^2/(2*a)) := by
  have backward_core (μ : Measure E) [IsProbabilityMeasure μ] (a : ℝ) (ha : 0 < a) :
      ∃ K : Kernel E E, IsMarkovKernel K ∧
        (∀ y, K y = μ.tilted (fun x => -‖x-y‖^2/(2*a))) ∧
        K ∘ₘ GaussianSmoothing.gaussianSmoothing μ (Real.sqrt a) = μ := by
    obtain ⟨K, hK, hfiber, hcond⟩ := GaussianConditionalKernel.exists_tilted_isCondKernel μ ha
    let := hK
    let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt a • p.2))
      (μ.prod (stdGaussian E))
    have hfst : J.fst = μ := by
      dsimp [J]
      rw [Measure.fst_map_prodMk (by fun_prop)]
      exact Measure.fst_prod
    have hsnd : J.snd = GaussianSmoothing.gaussianSmoothing μ (Real.sqrt a) := by
      dsimp [J]
      rw [Measure.snd_map_prodMk measurable_fst]
      unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
        GaussianSmoothing.scaledStdGaussian
      have hp := Measure.map_prod_map μ (stdGaussian E) measurable_id
        (show Measurable (fun z : E => Real.sqrt a • z) by fun_prop)
      rw [Measure.map_id] at hp
      rw [hp, Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    have : IsProbabilityMeasure J := Measure.isProbabilityMeasure_map (by fun_prop)
    have hd : (J.map Prod.swap).fst ⊗ₘ K = J.map Prod.swap := hcond.disintegrate
    have heq := congrArg Measure.snd hd
    rw [Measure.snd_compProd, Measure.fst_map_swap, Measure.snd_map_swap, hfst, hsnd] at heq
    exact ⟨K, hK, hfiber, heq⟩
  dsimp only
  let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
  have hi : Integrable (fun x => Real.exp (-(b/2)*‖x-u‖^2)) μ := by
    refine (integrable_const (1 : ℝ)).mono' (by fun_prop) ?_
    filter_upwards [] with x
    rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    apply Real.exp_le_one_iff.mpr
    exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (by positivity)) (sq_nonneg _)
  have hρ : IsProbabilityMeasure ρ := isProbabilityMeasure_tilted hi
  let := hρ
  obtain ⟨K, hK, hfiber, hrecover⟩ := backward_core ρ a ha
  let := hK
  refine ⟨hρ, K, hK, hfiber, ?_, hrecover, ?_⟩
  · intro y
    rw [hfiber]
    have halg : (fun x : E => -‖x-y‖^2/(2*a)) = (fun x => -(a⁻¹/2)*‖x-y‖^2) := by
      funext x
      field_simp
    rw [halg]
    exact RGOClosure.quadratic_tilt_tilt μ hb (inv_pos.mpr ha) u y
  · intro ν hν r hr hcost
    let := hν
    have hkl := GaussianKL.gaussian_kl_reverse_transport ν ρ r a hr ha hcost
    have hsmooth (η : Measure E) [IsProbabilityMeasure η] :
        IsProbabilityMeasure (GaussianSmoothing.gaussianSmoothing η (Real.sqrt a)) := by
      unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
      exact Measure.isProbabilityMeasure_map (by fun_prop)
    let := hsmooth ν
    let := hsmooth ρ
    have hdata := InformationTheory.klDiv_comp_right_le
      (GaussianSmoothing.gaussianSmoothing ν (Real.sqrt a))
      (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt a)) K
    rw [hrecover] at hdata
    exact hdata.trans hkl
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source RGO is defined for Gibbs potentials with the stated regularity and curvature assumptions.	An arbitrary probability base, followed by a normalized nonnegative quadratic-precision tilt.	generalization	The normalized kernel and parameter-update identity need only a probability base. Concrete Gibbs-potential identification and curvature guarantees are not asserted.
Equation(6.1) uses A inverse plus a inverse and its precision-weighted center, including A=infinity.	b>=0,a>0; updated precision b+a^-1 and center (b+a^-1)^-1(bu+a^-1*y), every y for the same Markov kernel.	same	Zero b retains infinite A and positive a ensures positive updated precision.
Theorem6.5 exact R_j=P_j K_j and Gaussian regularization are used within a recursive sampling proof.	Actual backward disintegration, noisy marginal identification, exact recovery and same-kernel KL guarantee for all admissible inputs.	source-implicit	No target recovery or conditional law premise is added; existing every-point measurable construction is consumed.
Gaussian KL input control is presented with Euclidean marginal P2 membership and W2.	Finite-dimensional inner-product Borel spaces including zero dimension and an actual infimum quadratic transport-cost budget.	generalization	No marginal moments are inferred; full W2 correspondence remains separate.
The full algorithm uses approximate recursive kernels, actual stage parameters, error accumulation and query costs.	Exact backward kernel consumer only, selected before all input laws and budgets.	API-limitation	No approximate sampler construction, measurable proxy selection, convolution-time identification or expected-cost result follows from this packet.

General probability-base abstraction of the source regularized Gibbs target and actual raw quadratic transport budget. The same measurable exact kernel has every-point precision-update fibers and target recovery. No concrete Gibbs-potential identification, marginal moment inference, approximate recursive sampler, measurable proxy selection, convolution time identification or expected query cost is asserted.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: General probability base abstracts concrete Gibbs potential. — No potential, density, curvature or positive-dimension premise; abstraction disclosed.
assumptions: Raw quadratic budget neither requires nor establishes marginal P2. — Positive bounded weights prove normalization; proved kernel supplies measurability; no marginal moment inference.
quantifiers: K measurable in y and fixed before nu,r; no jointly measurable parameter selection. — Same K in both fibers, recovery and KL; no joint measurable selection across target parameters.
scopes: Exact backward kernel only, not approximate recursive sampler or costs. — No concrete Gibbs identification, approximate recursion, parameter-joint selection or full algorithm guarantee.

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

General probability-base abstraction of the source regularized Gibbs target and actual raw quadratic transport budget. The same measurable exact kernel has every-point precision-update fibers and target recovery. No concrete Gibbs-potential identification, marginal moment inference, approximate recursive sampler, measurable proxy selection, convolution time identification or expected query cost is asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.snd_compProd
MeasureTheory.Measure.IsCondKernel.disintegrate
InformationTheory.klDiv_comp_right_le
MeasureTheory.isProbabilityMeasure_tilted

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1 Lemma6.4 and Theorem6.5 — Exact backward RGO semantics and its input KL guarantee; approximate recursive sampler remains separate.

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

One actual RGO backward kernel: precision update, recovery and KL control

Complete source statement (Samplinglib restatement)

Actual backward recovery and KL input guarantee

Read the formalized proofs

One actual RGO backward kernel: precision update, recovery and KL control

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Normalize the initial quadratic tilt

2. Construct the same measurable backward kernel

3. Identify actual forward and backward marginals

4. Recover the target by disintegration

5. Identify every normalized source precision update

6. Propagate the actual input KL budget

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?