Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

GaussianAugmentation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The joint density of a Gaussian augmentation for any input law
ASTIS mathematical exposition

The joint density of a Gaussian augmentation for any input law

AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation.augmentation_eq_withDensity · theorem · Teaching coverage

Statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra and canonical volume, mu a probability measure on E, and eta>0. Independently draw X with law mu and Z with the standard Gaussian law, and put Y=X+sqrt(eta) Z. Then the entire joint law of (X,Y) has density q_eta(y-x) relative to mu tensor volume. The input mu need not have a density relative to volume.

\[\Phi_\eta(x,z)=(x,x+\sqrt\eta\,z),\quad (\Phi_\eta)_\#(\mu\otimes\gamma_E)=(\mu\otimes\mathrm{vol}_E)\,q_\eta(y-x),\quad q_\eta(w)=((\sqrt{2\pi\eta})^{-1})^d\exp(-\|w\|^2/(2\eta)),\quad d=\dim_{\mathbb R}E.\]

All objects and hypotheses

  • E is a normed additive commutative group with a real inner product, finite real dimension, and its Borel measurable structure. Volume is the canonical inner-product-space volume, not an arbitrary Haar normalization.
  • mu is any probability measure on E. Independence is represented by the product measure mu.prod(stdGaussian E). Singular inputs, including point masses, are allowed.
  • eta is a positive real number. There is no upper scale bound and no potential, curvature, or input-density assumption. Finite dimension zero is included.
  • The reference measure is mu tensor volume. A density relative to volume tensor volume requires an additional density for mu, such as the source's Gibbs representation. That substitution is outside this theorem.

Mathematical proof

1. Scale the independent Gaussian noise

The existing isotropic Gaussian density theorem identifies the law of sqrt(eta) Z with volume weighted by q_eta. Mapping the two independent coordinates separately leaves the first law unchanged and applies this identity to the second law.

\[(x,z)\mapsto(x,\sqrt\eta\,z),\qquad (\mathrm{id}\times(\sqrt\eta\,\cdot))_\#(\mu\otimes\gamma_E)=\mu\otimes(\mathrm{vol}_E q_\eta).\]
Corresponding Lean step

The new local ASTIS IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity parent supplies the actual noise-law identity. Measure.map_prod_map and Measure.map_id then establish hprod. The density parent is compiled local work, not asserted to be Registry-admitted merely because this module imports it.

2. Express the independent product by a joint density

The product-density theorem moves the weight in the second coordinate to a density on the product reference measure. The Gaussian density is measurable, and the first probability measure needs no Lebesgue density.

\[\mu\otimes(\mathrm{vol}_E q_\eta)=(\mu\otimes\mathrm{vol}_E)\,[q_\eta(w)].\]
Corresponding Lean step

MeasureTheory.prod_withDensity_right is applied with the proved measurability of q. The formula is with respect to mu.prod volume, so it remains valid for a Dirac input.

3. The additive shear preserves the reference measure

The shear S(x,w)=(x,x+w) is a measurable equivalence, with inverse S inverse(x,y)=(x,y-x). It leaves the first coordinate fixed and translates volume in the second coordinate. Therefore it preserves mu tensor volume even when mu is not translation-invariant.

\[S_\#(\mu\otimes\mathrm{vol}_E)=\mu\otimes\mathrm{vol}_E,\qquad S^{-1}(x,y)=(x,y-x).\]
Corresponding Lean step

MeasurableEquiv.shearAddRight supplies the equivalence, and measurePreserving_prod_add mu volume supplies hvol. Probability of mu and canonical-volume sigma-finiteness discharge the product-measure prerequisites; no Jacobian proof is introduced.

4. Transport the density through the shear

Augmentation is exactly the composition of independent noise scaling and the shear. The existing ASTIS measurable-equivalence density theorem composes the density with the inverse shear, changing q_eta(w) into q_eta(y-x). This gives equality of the entire joint measures, not only equality of their total mass.

\[(\Phi_\eta)_\#(\mu\otimes\gamma_E)=S_\#((\mu\otimes\mathrm{vol}_E)q_\eta(w))=(\mu\otimes\mathrm{vol}_E)q_\eta(y-x).\]
Corresponding Lean step

Measure.map_map uses the proved factorization hPhi and measurable maps. RadonNikodym.measurableEquiv_map_withDensity transports the explicit product density. The inverse shear's second coordinate is -x+y; additive commutativity rewrites it to y-x.

Lean statement · augmentation_eq_withDensity

Measure.map denotes pushforward; Measure.prod is the independent product measure. withDensity takes an ENNReal-valued function obtained by ENNReal.ofReal from the nonnegative displayed real density. Equality is equality of measures, hence holds on every measurable event. Module.finrank is a natural dimension, and the normalizer uses a natural power of an inverse square root.

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 augmentation_eq_withDensity (μ : Measure E) [IsProbabilityMeasure μ]
    (η : ℝ) (hη : 0 < η) :
    Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
        (μ.prod (stdGaussian E)) =
      (μ.prod (volume : Measure E)).withDensity (fun p =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
            Real.exp (-‖p.2 - p.1‖ ^ 2 / (2 * η))))

Exact module and namespace context

Lean proof · augmentation_eq_withDensity

One theorem composes the newly compiled isotropic Gaussian density with existing product-density and measurable-equivalence transport. All abbreviations are local to the proof. No desired joint-law equality, density of mu, conditional representative, or volume-preservation claim is assumed as a hypothesis. The source-specific Gibbs density remains a separate consumer-level substitution.

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 augmentation_eq_withDensity (μ : Measure E) [IsProbabilityMeasure μ]
    (η : ℝ) (hη : 0 < η) :
    Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
        (μ.prod (stdGaussian E)) =
      (μ.prod (volume : Measure E)).withDensity (fun p =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
            Real.exp (-‖p.2 - p.1‖ ^ 2 / (2 * η)))) := by
  let σ : E → E := fun z => Real.sqrt η • z
  let q : E → ℝ≥0∞ := fun z => ENNReal.ofReal
    (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
      Real.exp (-‖z‖ ^ 2 / (2 * η)))
  let S : E × E ≃ᵐ E × E := MeasurableEquiv.shearAddRight E
  have hq : Measurable q := by fun_prop
  have hnoise : (stdGaussian E).map σ = (volume : Measure E).withDensity q :=
    TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity
      η hη
  have hprod : Measure.map (Prod.map id σ) (μ.prod (stdGaussian E)) =
      μ.prod ((volume : Measure E).withDensity q) := by
    rw [← Measure.map_prod_map μ (stdGaussian E) measurable_id (by fun_prop),
      hnoise, Measure.map_id]
  have hΦ : (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2)) =
      S ∘ Prod.map id σ := rfl
  have hvol : (μ.prod (volume : Measure E)).map S = μ.prod volume :=
    (measurePreserving_prod_add μ volume).map_eq
  rw [hΦ, ← Measure.map_map S.measurable (by fun_prop), hprod,
    prod_withDensity_right hq,
    TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensity
      S _ (f := fun p : E × E => q p.2) (by fun_prop), hvol]
  congr 1
  funext p
  change q (-p.1 + p.2) = q (p.2 - p.1)
  rw [neg_add_eq_sub]

end AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation

Exact module and namespace context

Scope and omitted-condition boundaries

  • This is an actual joint density relative to mu tensor canonical volume. It is not yet the source's exp(-V(x)-||x-y||^2/(2 eta)) density relative to volume tensor volume; substituting mu's Gibbs density and normalizer is the remaining edge.
  • Generic finite-dimensional E, dimension zero, arbitrary probability mu and all eta>0 are explicit generalizations of the paper's Euclidean Gibbs setting with 0<eta<=1/beta.
  • No reflection theorem, conditional-law representative, PBPS transition/process invariance, convergence, or query complexity is asserted. The density-defined reflection result is an intended downstream consumer.
  • The isotropic-density parent is a frozen compiled local result. Independent source review and shared Registry/publication admission are separately required.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • MeasureTheory.Measure.map_prod_map, map_id and map_map: independent-product and composed pushforwards.
  • MeasureTheory.prod_withDensity_right: second-coordinate density on a product reference measure.
  • MeasurableEquiv.shearAddRight and MeasureTheory.measurePreserving_prod_add: the additive shear and invariance of mu tensor volume.
  • Measurability of the explicit Gaussian density and continuous affine maps; neg_add_eq_sub.

Mathematical sources

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