ASTIS mathematical exposition

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

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO.two_noise_rgo · theorem · Teaching coverage

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}.\]

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 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.

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

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.

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

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.

Source and reuse

ASTIS 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.

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