An actual two-noise RGO stage with the added-time KL denominator

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, eta>=0, tau>0 and u a point. Put rho=mu.tilted(-b*norm(x-u)^2/2). Then rho is probability and H_tau(H_eta rho)=H_(eta+tau)rho as actual measures, where H_s is GaussianSmoothing at standard deviation sqrt(s). There exists one Markov kernel K, selected before all proposal laws nu and radii r, with every-point fiber rho.tilted(-norm(x-y)^2/(2*(eta+tau))), and K composed with H_tau(H_eta rho)=rho. For every probability nu and r>=0 with actual extended-nonnegative WassersteinSpace.wassersteinDistance(nu,H_eta rho)<=ofReal(r), the actual ENNReal KL(K composed with H_tau nu,rho)<=ofReal(r^2/(2*tau)).

Actual two-noise stage with W2 input and added-time KL control

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

An actual two-noise RGO stage with the added-time KL denominator

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO.two_noise_rgo · 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, eta≥0, tau>0 and u a point. Put rho=mu.tilted(-b*norm(x-u)^2/2). Then rho is probability and H_tau(H_eta rho)=H_(eta+tau)rho as actual measures, where H_s is GaussianSmoothing at standard deviation sqrt(s). There exists one Markov kernel K, selected before all proposal laws nu and radii r, with every-point fiber rho.tilted(-norm(x-y)^2/(2*(eta+tau))), and K composed with H_tau(H_eta rho)=rho. For every probability nu and r≥0 with actual extended-nonnegative WassersteinSpace.wassersteinDistance(nu,H_eta rho)≤ofReal(r), the actual ENNReal KL(K composed with H_tau nu,rho)≤ofReal(r^2/(2*tau)).

\[W_2(\nu,H_\eta\rho)\le r,\quad K_{\eta+\tau}H_\tau H_\eta\rho=\rho\quad\Longrightarrow\quad \operatorname{KL}(K_{\eta+\tau}H_\tau\nu\|\rho)\le\frac{r^2}{2\tau}.\]

Lean statement · two_noise_rgo

Actual Gaussian semigroup, one total-time backward kernel, exact two-noise recovery and added-time input KL guarantee.

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 two_noise_rgo {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b η τ : ℝ)
    (hb : 0 ≤ b) (hη : 0 ≤ η) (hτ : 0 < τ) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧
      GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η))
        (Real.sqrt τ) = GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η+τ)) ∧
      ∃ K : Kernel E E, IsMarkovKernel K ∧
        (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*(η+τ)))) ∧
        K ∘ₘ GaussianSmoothing.gaussianSmoothing
          (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) (Real.sqrt τ) = ρ ∧
        ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
          WassersteinSpace.wassersteinDistance ν
            (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) ≤ ENNReal.ofReal r →
          InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt τ)) ρ ≤
            ENNReal.ofReal (r^2/(2*τ))

Exact module and namespace context

Proof roadmap

1Compute the actual scaled Gaussian characteristic function
The existing standard Gaussian characteristic function and the map-under-scaling formula give the exact exponent. Nonnegative time justifies replacing sqrt(s)^2 by s, also at zero.
2Prove the measure semigroup by characteristic-function uniqueness
The existing smoothing is definitionally the convolution of the input with its scaled Gaussian law. Its measures are probabilities. The convolution characteristic function is a product, so the two Gaussian exponents add. Uniqueness yields equality of the actual smoothed measures; no noise-composition premise is assumed.
3Choose the exact backward kernel at total time
Apply the existing RGO backward theorem at positive eta+tau to the actual regularized target. It proves target probability, supplies one Markov kernel with every-point normalized fiber and recovers rho from H_(eta+tau)rho.
4Identify the actual two-noise target recovery
Substitute the proved semigroup equality into recovery. The two random noise additions followed by the selected backward kernel now have exactly the target output law.
5Apply input error control only at the added time
Introduce nu,r after choosing K. Square the actual ENNReal W2 bound and use its existing exact square identity to derive the quadratic budget. GaussianKL compares nu to the already smoothed target H_eta rho using only added noise tau. Same-kernel data processing and exact recovery transfer that bound to the actual output. Total variance cannot replace tau in the denominator.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel space including zero dimension; mu probability; b≥0 and arbitrary u.
eta≥0 and tau>0, so total eta+tau>0. Zero existing smoothing time is allowed.
The kernel may depend on mu,b,eta,tau,u but is chosen before nu,r. No joint measurable choice across these parameters is asserted.
The proposal input is the actual ENNReal W2(nu,H_eta rho)≤ofReal(r), r≥0. Its exact square identity gives the internal quadratic coupling budget; no toReal fallback, optimizer or marginal moments are supplied.
General probability base and absence of marginal P2 assumptions explicitly generalize the source Gibbs/P2 setting. This packet uses the existing actual W2 interface; concrete normalized source times and full recursion remain separate.

Mathematical proof

1. Compute the actual scaled Gaussian characteristic function

The existing standard Gaussian characteristic function and the map-under-scaling formula give the exact exponent. Nonnegative time justifies replacing sqrt(s)^2 by s, also at zero.

\[\widehat G_{\sqrt s}(t)=\exp(-s\|t\|^2/2),\qquad s\ge0.\]

Corresponding Lean step

Local hc uses charFun_map_smul, charFun_stdGaussian and Real.sq_sqrt.

2. Prove the measure semigroup by characteristic-function uniqueness

The existing smoothing is definitionally the convolution of the input with its scaled Gaussian law. Its measures are probabilities. The convolution characteristic function is a product, so the two Gaussian exponents add. Uniqueness yields equality of the actual smoothed measures; no noise-composition premise is assumed.

\[\widehat{H_\tau H_\eta P}(t)=\widehat P(t)e^{-\eta\|t\|^2/2}e^{-\tau\|t\|^2/2}=\widehat{H_{\eta+\tau}P}(t).\]

Corresponding Lean step

Local heat_semigroup uses actual convolution, charFun_conv and Measure.ext_of_charFun.

3. Choose the exact backward kernel at total time

Apply the existing RGO backward theorem at positive eta+tau to the actual regularized target. It proves target probability, supplies one Markov kernel with every-point normalized fiber and recovers rho from H_(eta+tau)rho.

\[K(y)=\rho.\mathrm{tilted}(-\|x-y\|^2/(2(\eta+\tau))),\quad K H_{\eta+\tau}\rho=\rho.\]

Corresponding Lean step

RGOBackward.rgo_backward_recovery at eta+tau; retain hρ,hK,hfiber,hrecover.

4. Identify the actual two-noise target recovery

Substitute the proved semigroup equality into recovery. The two random noise additions followed by the selected backward kernel now have exactly the target output law.

\[K H_\tau(H_\eta\rho)=K H_{\eta+\tau}\rho=\rho.\]

Corresponding Lean step

hsem and hrec use actual measure equality, not a symbolic time convention.

5. Apply input error control only at the added time

Introduce nu,r after choosing K. Square the actual ENNReal W2 bound and use its existing exact square identity to derive the quadratic budget. GaussianKL compares nu to the already smoothed target H_eta rho using only added noise tau. Same-kernel data processing and exact recovery transfer that bound to the actual output. Total variance cannot replace tau in the denominator.

\[\operatorname{KL}(K H_\tau\nu\|\rho)\le\operatorname{KL}(H_\tau\nu\|H_\tau H_\eta\rho)\le r^2/(2\tau).\]

Corresponding Lean step

WassersteinSpace.wassersteinDistance_sq and ENNReal.ofReal_pow derive hcost; InformationTheory.klDiv_comp_right_le, hrec and GaussianKL at added tau.

Lean verification

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

Lean proof · two_noise_rgo

Characteristic functions identify actual smoothing composition, then the total-time RGO recovery and added-time Gaussian KL yield the output bound.

Download module (.lean)

theorem two_noise_rgo {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b η τ : ℝ)
    (hb : 0 ≤ b) (hη : 0 ≤ η) (hτ : 0 < τ) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧
      GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η))
        (Real.sqrt τ) = GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η+τ)) ∧
      ∃ K : Kernel E E, IsMarkovKernel K ∧
        (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*(η+τ)))) ∧
        K ∘ₘ GaussianSmoothing.gaussianSmoothing
          (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) (Real.sqrt τ) = ρ ∧
        ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
          WassersteinSpace.wassersteinDistance ν
            (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) ≤ ENNReal.ofReal r →
          InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt τ)) ρ ≤
            ENNReal.ofReal (r^2/(2*τ)) := by
  have heat_semigroup (μ : Measure E) [IsProbabilityMeasure μ] (η τ : ℝ) (hη : 0 ≤ η) (hτ : 0 ≤ τ) :
      GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing μ (Real.sqrt η))
        (Real.sqrt τ) = GaussianSmoothing.gaussianSmoothing μ (Real.sqrt (η+τ)) := by
    have hc (a : ℝ) (ha : 0 ≤ a) (t : E) :
        charFun (GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt a)) t =
          Complex.exp (-(a : ℂ) * (‖t‖ : ℂ)^2 / 2) := by
      unfold GaussianSmoothing.scaledStdGaussian
      rw [charFun_map_smul, charFun_stdGaussian]
      simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg a),
        Complex.ofReal_mul, mul_pow]
      rw [← Complex.ofReal_pow, Real.sq_sqrt ha]
      congr 1
      ring
    have hs (ν : Measure E) [IsProbabilityMeasure ν] (s : ℝ) :
        IsProbabilityMeasure (GaussianSmoothing.gaussianSmoothing ν s) := by
      unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
      exact Measure.isProbabilityMeasure_map (by fun_prop)
    let := hs μ (Real.sqrt η)
    let := hs (GaussianSmoothing.gaussianSmoothing μ (Real.sqrt η)) (Real.sqrt τ)
    let := hs μ (Real.sqrt (η+τ))
    apply Measure.ext_of_charFun
    funext t
    change charFun ((μ ∗ GaussianSmoothing.scaledStdGaussian (Real.sqrt η)) ∗
        GaussianSmoothing.scaledStdGaussian (Real.sqrt τ)) t =
      charFun (μ ∗ GaussianSmoothing.scaledStdGaussian (Real.sqrt (η+τ))) t
    rw [charFun_conv, charFun_conv, charFun_conv, hc η hη, hc τ hτ, hc (η+τ) (add_nonneg hη hτ)]
    rw [mul_assoc, ← Complex.exp_add]
    congr 2
    push_cast
    ring
  dsimp only
  let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
  obtain ⟨hρ,K,hK,hfiber,_,hrecover,_⟩ :=
    RGOBackward.rgo_backward_recovery μ b (η+τ) hb (add_pos_of_nonneg_of_pos hη hτ) u
  let := hρ
  let := hK
  have hs (ν : Measure E) [IsProbabilityMeasure ν] (s : ℝ) :
      IsProbabilityMeasure (GaussianSmoothing.gaussianSmoothing ν s) := by
    unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
    exact Measure.isProbabilityMeasure_map (by fun_prop)
  have hsem := heat_semigroup ρ η τ hη hτ.le
  have hrec : K ∘ₘ GaussianSmoothing.gaussianSmoothing
      (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) (Real.sqrt τ) = ρ := by
    rw [hsem]
    exact hrecover
  refine ⟨hρ,hsem,K,hK,hfiber,hrec,?_⟩
  intro ν hν r hr hW
  have hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) ν
      (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) ≤ ENNReal.ofReal (r^2) := by
    have hh := pow_le_pow_left₀ (by positivity) hW 2
    rw [WassersteinSpace.wassersteinDistance_sq, ← ENNReal.ofReal_pow hr] at hh
    exact hh
  let := hν
  let := hs ρ (Real.sqrt η)
  let := hs ν (Real.sqrt τ)
  let := hs (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) (Real.sqrt τ)
  have hk := InformationTheory.klDiv_comp_right_le
    (GaussianSmoothing.gaussianSmoothing ν (Real.sqrt τ))
    (GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η))
      (Real.sqrt τ)) K
  rw [hrec] at hk
  exact hk.trans (GaussianKL.gaussian_kl_reverse_transport ν
    (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) r τ hr hτ hcost)
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Theorem6.5 uses a regularized Gibbs target and a proposal close to its already-smoothed law in W2.	General probability base quadratically tilted; actual Samplinglib ENNReal W2(nu,H_eta rho)<=ofReal(r).	generalization	The existing exact square identity derives the quadratic budget; finite transport distance does not imply individual marginal P2 membership. Concrete Gibbs potential assumptions are abstracted explicitly.
Stage times are normalized by beta_A and compose before the exact backward RGO.	eta>=0,tau>0, actual H_tau(H_eta rho)=H_(eta+tau)rho; K at total eta+tau.	source-implicit	Characteristic functions prove actual Gaussian convolution; concrete normalized stage substitutions remain separate.
Gaussian regularization compares the proposal with an already-smoothed target using newly added noise.	Actual KL(K composed with H_tau nu,rho)<=ofReal(r^2/(2*tau)), input against H_eta rho.	same	Denominator uses only added tau, not total eta+tau. KL direction and one fixedK are exact.
The kernel is fixed by the target and stage, independently of the approximate input law.	One K after mu,b,eta,tau,u and before every nu,r, with every-y normalized fiber and actual two-noise recovery.	same	No joint measurable parameter/history selection is asserted.
Full recursive algorithm uses approximate kernels, error accumulation and expected query costs.	Fixed-target exact two-noise stage only.	API-limitation	Concrete source times, adaptive/history kernels, measurable proxies, approximate sampler, accumulated errors and costs remain separate.

The input is Samplinglib actual extended-nonnegative W2, defined as the square root of the quadratic coupling infimum; its proved square identity supplies the internal cost budget. Finite W2 does not establish marginal P2 membership. General probability-base target and fixed-stage formulation explicitly generalize source Gibbs/P2. Joint parameter/history kernels, concrete source-time substitutions, approximate recursion, measurable proxies, accumulated errors and costs remain separate. The local semigroup helper is not a separately public Gaussian-law API.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: General probability-base/finite-dimensional formulation abstracts concrete Gibbs. — No concrete potential, curvature or positive-dimension premise.
assumptions: No individual P2 assumption; eta0 allowed, finite W2 does not imply marginal moments. — Zeroexistingnoise allowed; hcost derived from squaredactualW2, no optimizer or P2inference.
objects: Actual W2 input is implemented and is not a deferred correspondence gap. — Actual two-noise law and existing W2 square identity; no symbolic/toReal replacement.
scopes: Fixed stage does not assert concrete beta-normalized time substitution or history-dependent approximate sampling. — Concrete source times, adaptive/historykernels, approximate recursion anderrors/costs excluded.
scopes: General semigroup remains localhelper, not separately public Gaussian-law API. — Concrete source times, adaptive/historykernels, approximate recursion anderrors/costs excluded.

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

The input is Samplinglib actual extended-nonnegative W2, defined as the square root of the quadratic coupling infimum; its proved square identity supplies the internal cost budget. Finite W2 does not establish marginal P2 membership. General probability-base target and fixed-stage formulation explicitly generalize source Gibbs/P2. Joint parameter/history kernels, concrete source-time substitutions, approximate recursion, measurable proxies, accumulated errors and costs remain separate. The local semigroup helper is not a separately public Gaussian-law API.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.charFun_stdGaussian
MeasureTheory.charFun_map_smul
MeasureTheory.charFun_conv
MeasureTheory.Measure.ext_of_charFun
InformationTheory.klDiv_comp_right_le

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1 Theorem6.5 and Lemma6.3(i) — Fixed-stage smoothed proposal, additional Gaussian noise and exact backward sampling; not full approximate recursion.

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

An actual two-noise RGO stage with the added-time KL denominator

Complete source statement (Samplinglib restatement)

Actual two-noise stage with W2 input and added-time KL control

Read the formalized proofs

An actual two-noise RGO stage with the added-time KL denominator

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Compute the actual scaled Gaussian characteristic function

2. Prove the measure semigroup by characteristic-function uniqueness

3. Choose the exact backward kernel at total time

4. Identify the actual two-noise target recovery

5. Apply input error control only at the added time

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?