ASTIS mathematical exposition

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

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

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

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

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

Lean proof · rgo_backward_recovery

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

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

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.

Source and reuse

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

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