The joint density of a Gaussian augmentation for any input law
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation.augmentation_eq_withDensity · theorem · Teaching coverage
Mathematical 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.
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 * η))))Proof roadmap
- 1Scale 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.
- 2Express 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.
- 3The 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.
- 4Transport 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.
Full assumptions and notation
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.
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.
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.
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.
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.GaussianAugmentationSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The input is the paper's normalized smooth strongly log-concave Gibbs law on R^d | Any probability measure mu on a finite-dimensional real inner-product Borel space E | generalization | The selected density is relative to mu tensor volume. Only the independent Gaussian coordinate is given a volume density, so mu may even be a Dirac measure. The missing Gibbs substitution is a separate obligation, not a hidden hypothesis. |
| d>=1 and Euclidean Lebesgue volume | Every finite real dimension, including zero, with the canonical inner-product-space volume | generalization | The proved noise-density parent and shear identity apply in zero dimension too. No arbitrary Haar normalization or extra measure-space parameter is introduced. |
| 0<eta<=1/beta | eta>0 | generalization | The upper bound is not used for the joint Gaussian-density identity; it belongs to other curvature and algorithmic statements. |
| Joint Gibbs density relative to dx dy, with the source's target-density definition | Density relative to mu.prod volume, with factor q_eta(y-x) | unresolved | The actual Gaussian augmentation adapter is proved, but the final target-density and Gibbs-normalizer substitution is still outside this theorem and remains an unbound source obligation. |
| Independent sampling and translation of the Gaussian auxiliary coordinate | Product probability measure, proved measurable factorization, explicit density transport, and shear preserving mu.prod volume | source-implicit | The proof supplies the required measurable maps and product-measure contracts. Translation invariance is required only of volume, not of mu. |
Actual joint-law density relative to mu tensor volume only; source Gibbs-density substitution remains unbound and open. No reflection or PBPS-process claim.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The formal component explicitly includes arbitrary probability inputs, abstract finite-dimensional inner-product spaces and zero dimension rather than only the source's Gibbs sampling setting. — The fresh extraction and lesson openly state this generalization. The proof leaves μ untouched in the first coordinate; a Dirac input is allowed, and dimension zero gives density one on the one-point space.
- assumptions: The isolated Gaussian identity uses η>0 without the source's sampler upper bound η≤1/β. — No step of scaling, product-density conversion or shear transport uses β. This wider range is appropriate for the selected intermediate theorem and does not modify any sampler guarantee.
- conclusion: The theorem's reference measure is μ⊗volume; the full displayed source Gibbs density uses volume⊗volume. — The missing Gibbs-density insertion is explicitly retained as gibbs-density-substitution. Consequently this component may be accepted without certifying full equation (2.6); arbitrary singular μ prevents silently treating the two reference measures as interchangeable.
- scopes: No conditional representative, reflection property, PBPS-process invariance, convergence or query-cost result is supplied. — Those conclusions occur nowhere in the current formal statement or selected binding, and the lesson expressly excludes them. The metadata correction gives exact dependency targets without enlarging mathematical completion credit.
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
- 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensityAutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensity
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
- Chen, Chewi, Lu and Zhang, Accelerated High-Accuracy Sampling from a Warm Start via the Proximal Bouncy Particle Sampler v1 — Joint-law density component of equations (2.6)-(2.7), with reference measure mu tensor volume kept explicit. Original ASTIS exposition, not reproduced paper prose.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.