ASTIS mathematical exposition

The Gaussian posterior is an actual measurable conditional kernel

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel · theorem · Teaching coverage

Statement

Let μ be any probability measure on a finite-dimensional real inner-product Borel space E, and let η>0. For independent X∼μ and G∼N(0,I), set Y=X+√η G and let J be the law of (X,Y). There exists a measurable Markov kernel R from E to E such that for every y its law is the normalized quadratic tilt μ.tilted(x↦−‖x−y‖²/(2η)), and R disintegrates the law of (Y,X) with respect to the actual observation marginal.

\[R(y,dx)=\frac{e^{-\|x-y\|^2/(2\eta)}\mu(dx)}{\int_E e^{-\|z-y\|^2/(2\eta)}\mu(dz)},\qquad\mathcal L(Y,X)=\mathcal L(Y)\otimes R.\]

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel sigma algebra; μ is a probability measure, possibly singular and without finite moments.
The variance η is strictly positive. No curvature bound, density for μ, or restriction η≤1/β is needed for this law identity.
A kernel means a measure-valued function with measurable dependence on its input. Every returned fiber is a probability law; these properties are proved, not supplied.
The explicit formula selects a version at every y. Conditional laws chosen in other ways need agree with it only almost everywhere under the observation marginal.

Mathematical proof

1. A bounded positive likelihood has a genuine normalizer

For each observation y put w(y,x)=exp(−‖x−y‖²/(2η)). Positivity of η gives 0<w≤1. Joint continuity makes w measurable; the finite input measure makes every fiber integrable. Since μ has mass one and w is strictly positive everywhere, its integral is strictly positive. Thus neither division nor the tilted-measure API can fall back to a zero law.

\[w(y,x)=e^{-\|x-y\|^2/(2\eta)},\qquad Z(y)=\int_Ew(y,x)\,\mu(dx),\qquad0<Z(y)\le1.\]

Corresponding Lean step

hw proves joint measurability. hI uses integrable_const and Integrable.mono' with the explicit bound by one; hZpos invokes integral_exp_pos. The upper bound is the domination used in hI, not a separate production declaration.

2. Make the normalized fibers into one measurable Markov kernel

Measurability of parameter integrals makes y↦Z(y) measurable. Consequently w(y,x)/Z(y) is jointly measurable. Weight the constant kernel μ by this density. Its fiber at every y is exactly the existing normalized tilted measure, whose probability theorem applies because hI has already been proved.

\[R(y,dx)=\frac{w(y,x)}{Z(y)}\mu(dx),\qquad R(y,E)=1.\]

Corresponding Lean step

hZ uses StronglyMeasurable.integral_prod_right. hd supplies the required joint measurability to Kernel.withDensity_apply; without it that totalized constructor would return zero. hRfiber identifies the exact Measure.tilted expression, and hR uses isProbabilityMeasure_tilted.

3. Express the actual joint law in observation-first order

Take independent X with law μ and a standard Gaussian G, and set Y=X+√η G. Reuse the already compiled Gaussian augmentation density, then swap its coordinates. The symmetry ‖y−x‖=‖x−y‖ gives the displayed density with respect to dy μ(dx). No density of μ relative to volume is needed.

\[J^\leftrightarrow(dy,dx)=C_\eta w(y,x)\,dy\,\mu(dx),\qquad C_\eta=(\sqrt{2\pi\eta})^{-\dim E}.\]

Corresponding Lean step

hJ calls the ASTIS-owned GaussianAugmentation.augmentation_eq_withDensity, transports the density through MeasurableEquiv.prodComm using the existing ASTIS RadonNikodym lemma, then uses Measure.prod_swap and norm_sub_rev.

4. Cancel only the proven positive normalizer

Introduce the auxiliary observation measure ν(dy)=Cη Z(y)dy. This measure is s-finite, so its composition-product with R is defined by the usual kernel integral. The density-product identities combine the factors; Z(y)>0 justifies cancellation at every point. This proves the full joint-measure identity, not merely proportionality of densities.

\[(\nu\otimes R)(dy,dx)=C_\eta Z(y)\frac{w(y,x)}{Z(y)}\,dy\,\mu(dx)=J^\leftrightarrow(dy,dx).\]

Corresponding Lean step

hcomp uses Measure.compProd_withDensity, Measure.compProd_const, prod_withDensity_left and withDensity_mul. ENNReal.ofReal_mul converts the nonnegative density product, and field_simp receives (hZpos y).ne'. No cancellation of a possibly zero integral is permitted.

5. Identify the observation marginal and certify disintegration

Take first marginals of the joint identity. Because each R(y,·) has total mass one, the first marginal of ν⊗R is ν. Therefore ν is the actual law of Y, and the joint identity is precisely the conditional-kernel certificate. Taking second marginals also recovers the original input law after applying R to the law of Y.

\[\nu=J^\leftrightarrow_1=\mathcal L(Y),\qquad\mathcal L(Y)\otimes R=\mathcal L(Y,X),\qquad\int R(y,\cdot)\,\mathcal L(Y)(dy)=\mu.\]

Corresponding Lean step

hf applies congrArg Measure.fst and Measure.fst_compProd. Measure.IsCondKernel packages exactly the resulting equality. The separate focused test takes second marginals with Measure.snd_compProd and checks the backward-law recovery consumer.

Lean statement · exists_tilted_isCondKernel

The let-bound J is the pushforward of μ.prod(stdGaussian E) by (x,g)↦(x,x+sqrt η•g), so independence and the actual observation law are encoded explicitly. IsMarkovKernel and the all-y fiber formula are returned together with (J.map Prod.swap).IsCondKernel R. Measure.tilted already expresses normalized exponential reweighting; no duplicate posterior definition is introduced.

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 exists_tilted_isCondKernel (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let J := Measure.map
      (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    ∃ R : Kernel E E, IsMarkovKernel R ∧
      (∀ y, R y = μ.tilted (fun x => -‖x - y‖ ^ 2 / (2 * η))) ∧
      (J.map Prod.swap).IsCondKernel R

Exact module and namespace context

Lean proof · exists_tilted_isCondKernel

All weights, normalizers, densities and the constructed kernel are local proof terms. Their measurability and normalization witnesses are proved before density or composition APIs are used. The focused tests exercise a singular Dirac input and the general backward-law recovery identity, and print the theorem's axioms.

theorem exists_tilted_isCondKernel (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let J := Measure.map
      (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    ∃ R : Kernel E E, IsMarkovKernel R ∧
      (∀ y, R y = μ.tilted (fun x => -‖x - y‖ ^ 2 / (2 * η))) ∧
      (J.map Prod.swap).IsCondKernel R := by
  classical
  let J := Measure.map
    (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
    (μ.prod (stdGaussian E))
  let w : E → E → ℝ := fun y x => Real.exp (-‖x - y‖ ^ 2 / (2 * η))
  let Z : E → ℝ := fun y => ∫ x, w y x ∂μ
  have hw : Measurable (Function.uncurry w) := by fun_prop
  have hI (y : E) : Integrable (w y) μ := 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
      (div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) (by positivity))
  have hZpos (y : E) : 0 < Z y := integral_exp_pos (hI y)
  have hZ : Measurable Z := hw.stronglyMeasurable.integral_prod_right.measurable
  let d : E → E → ℝ≥0∞ := fun y x => ENNReal.ofReal (w y x / Z y)
  have hd : Measurable (Function.uncurry d) :=
    (hw.div (hZ.comp measurable_fst)).ennreal_ofReal
  let R : Kernel E E := (Kernel.const E μ).withDensity d
  have hRfiber (y : E) : R y = μ.tilted (fun x => -‖x - y‖ ^ 2 / (2 * η)) := by
    rw [show R = (Kernel.const E μ).withDensity d from rfl,
      Kernel.withDensity_apply _ hd]
    rfl
  have hR : IsMarkovKernel R := ⟨fun y => by
    rw [hRfiber]
    exact isProbabilityMeasure_tilted (hI y)⟩
  let C : ℝ := ((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E
  have hC : 0 ≤ C := by positivity
  let a : E → ℝ≥0∞ := fun y => ENNReal.ofReal (C * Z y)
  have ha : Measurable a := (measurable_const.mul hZ).ennreal_ofReal
  let ν : Measure E := volume.withDensity a
  have hJ : J.map Prod.swap = (volume.prod μ).withDensity
      (fun p : E × E => ENNReal.ofReal (C * w p.1 p.2)) := by
    dsimp only [J]
    rw [ExampleCases.ProximalBPS.GaussianAugmentation.augmentation_eq_withDensity μ η hη]
    change ((μ.prod volume).withDensity _).map
      (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E) = _
    rw [Measure.RadonNikodym.measurableEquiv_map_withDensity
      (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E) _ (by fun_prop)]
    change ((μ.prod volume).map Prod.swap).withDensity _ = _
    rw [Measure.prod_swap]
    congr 1
    funext p
    change ENNReal.ofReal (C * Real.exp (-‖p.1 - p.2‖ ^ 2 / (2 * η))) =
      ENNReal.ofReal (C * Real.exp (-‖p.2 - p.1‖ ^ 2 / (2 * η)))
    rw [norm_sub_rev p.1 p.2]
  have hcomp : ν ⊗ₘ R = J.map Prod.swap := by
    rw [hJ]
    change ν ⊗ₘ (Kernel.const E μ).withDensity d = _
    rw [Measure.compProd_withDensity hd, Measure.compProd_const]
    change ((volume.withDensity a).prod μ).withDensity _ = _
    rw [prod_withDensity_left ha]
    rw [← withDensity_mul _
      (show Measurable (fun p : E × E => a p.1) from ha.comp measurable_fst)
      (show Measurable (fun p : E × E => d p.1 p.2) from hd)]
    congr 1
    funext p
    change ENNReal.ofReal (C * Z p.1) * ENNReal.ofReal (w p.1 p.2 / Z p.1) = _
    rw [← ENNReal.ofReal_mul (mul_nonneg hC (hZpos p.1).le)]
    congr 1
    field_simp [(hZpos p.1).ne']
  have hf := congrArg Measure.fst hcomp
  rw [Measure.fst_compProd] at hf
  refine ⟨R, hR, hRfiber, ⟨?_⟩⟩
  rw [← hf]
  exact hcomp

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel

Exact module and namespace context

Scope and omitted-condition boundaries

This closes the conditional-law construction behind PBPS (2.7)-(2.8), not a realizable RGO algorithm, PBPS trajectory, nonexplosion, invariant process law, mixing bound or expected query cost.
Gibbs specialization uses the separately proved positive Gibbs normalizer and probability certificate. The generic theorem itself assumes an input probability law and does not prove those Gibbs facts again.
The focused consumer test proves exact recovery of μ from the actual smoothed marginal via this kernel. This is one joint-law marginal identity, not stationarity of the PBPS process.
Curvature, covariance, moment bounds and implementation error remain separate. No pointwise uniqueness among arbitrary conditional versions is claimed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

integral_exp_pos
StronglyMeasurable.integral_prod_right
Kernel.withDensity_apply
isProbabilityMeasure_tilted
Measure.prod_swap
Measure.compProd_withDensity
Measure.compProd_const
prod_withDensity_left
withDensity_mul
Measure.fst_compProd

Mathematical sources

Chen, Chewi, Lu and Zhang, PBPS v1, §2.2, (2.7)-(2.8) — Conditional-law step, expanded by ASTIS with normalization, measurability and disintegration; no copied paper prose.
Chen, Chewi, Lu and Zhang, SPHMC v1, §3.4 — Intended consumer: the backward restricted Gaussian law. Algorithm implementation and quantitative guarantees are independent.
Rémy Degenne and Mathlib contributors, Apache-2.0 — Existing measurable density-kernel and composition APIs are reused, not counted as ASTIS-owned results.

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