Why reflecting the Gaussian auxiliary point preserves its joint law
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentation · theorem · Teaching coverage
Statement
Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, let mu be a probability measure on E, and let eta>0. Independently draw X with law mu and a standard Gaussian Z, and put Y=X+sqrt(eta) Z. The map R(x,y)=(x,2x-y) is an involution, and (X,2X-Y) has exactly the same joint law as (X,Y).
All objects and hypotheses
- E is a normed additive commutative group with a real inner product and finite real dimension; its measurable sets are the Borel sets.
- mu is a probability measure. The product mu tensor gamma encodes independence; gamma is Mathlib's standard Gaussian on E.
- eta is a positive real scale. Positivity retains the sampling interpretation; the reflection calculation itself uses no division by eta.
- This selected proof component is more general than the paper's Gibbs/curvature setting. It neither assumes nor proves that its pushforward law equals the density displayed in (2.6).
Mathematical proof
1. Check the reflection is an involution
The first coordinate stays fixed. Reflecting the second coordinate twice cancels the two subtractions, so no exceptional point or almost-everywhere qualification is needed.
Corresponding Lean step
The first conjunction branch proves equality of the two product coordinates. The second coordinate is sub_sub_cancel; it holds pointwise for every state.
2. Reverse the Gaussian displacement
Negation is an orthogonal linear isometry. Hence the standard Gaussian is unchanged by Z becoming -Z. Product pushforward preserves the first law and changes only the independent auxiliary variable.
Corresponding Lean step
ProbabilityTheory.stdGaussian_map is instantiated with LinearIsometryEquiv.neg. Measure.map_prod_map and Measure.map_id then transport this equality to the product measure. These are Mathlib results, not new ASTIS Gaussian lemmas.
3. Relate noise reversal to state reflection
Reflecting Y around X reverses its displacement from X. This is an equality of actual measurable functions, not merely equality in distribution.
Corresponding Lean step
The proof establishes the composition identity pointwise with scalar/additive algebra. Measurability of the reflection, augmentation and sign map is supplied before using Measure.map_map.
4. Transport the invariant product law
Pushforward composition and the preceding symmetry now give equality of the entire joint measures, hence equality on every measurable event. No density argument, integral interchange or conditional representative is hidden in this calculation.
Corresponding Lean step
The final rewrite uses Measure.map_map twice, the proved composition identity and the proved product symmetry. It does not assume the desired invariance as a hypothesis.
Lean statement · reflection_preserves_augmentation
Measure.map is pushforward and Measure.prod is product measure. The IsProbabilityMeasure typeclass supplies finiteness for the product transport theorem; BorelSpace ties measurable sets to the topology. Function.Involutive is a pointwise statement that applying a function twice is the identity. The conjunction packages both parts of the source's reflection claim without adding a duplicate wrapper.
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 reflection_preserves_augmentation (μ : Measure E) [IsProbabilityMeasure μ]
(η : ℝ) (_hη : 0 < η) :
Function.Involutive (fun p : E × E => (p.1, (2 : ℝ) • p.1 - p.2)) ∧
Measure.map (fun p : E × E => (p.1, (2 : ℝ) • p.1 - p.2))
(Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E))) =
Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E))Lean proof · reflection_preserves_augmentation
Local names abbreviate the three displayed affine functions inside the proof only. Every map needed by pushforward composition is proved measurable. ASTIS composes Mathlib's Gaussian-isometry theorem and product/map transport with the source-specific reflection algebra. The source hypotheses on potential smoothness are not silently used or claimed: they belong to the still-open density and algorithmic adapters.
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 reflection_preserves_augmentation (μ : Measure E) [IsProbabilityMeasure μ]
(η : ℝ) (_hη : 0 < η) :
Function.Involutive (fun p : E × E => (p.1, (2 : ℝ) • p.1 - p.2)) ∧
Measure.map (fun p : E × E => (p.1, (2 : ℝ) • p.1 - p.2))
(Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E))) =
Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E)) := by
let Φ : E × E → E × E := fun p => (p.1, p.1 + Real.sqrt η • p.2)
let R : E × E → E × E := fun p => (p.1, (2 : ℝ) • p.1 - p.2)
let S : E × E → E × E := Prod.map id (fun z => -z)
have hΦ : Measurable Φ := by fun_prop
have hR : Measurable R := by fun_prop
have hS : Measurable S := by fun_prop
have hneg : Measure.map (fun z : E => -z) (stdGaussian E) = stdGaussian E := by
simpa using (stdGaussian_map (LinearIsometryEquiv.neg ℝ (E := E)))
have hprod : Measure.map S (μ.prod (stdGaussian E)) = μ.prod (stdGaussian E) := by
dsimp [S]
rw [← Measure.map_prod_map μ (stdGaussian E) measurable_id (by fun_prop),
hneg, Measure.map_id]
have hcomp : R ∘ Φ = Φ ∘ S := by
funext p
apply Prod.ext
· rfl
· dsimp [R, Φ, S]
simp only [smul_neg, two_smul]
abel
constructor
· intro p
apply Prod.ext
· rfl
· exact sub_sub_cancel ((2 : ℝ) • p.1) p.2
· change Measure.map R (Measure.map Φ (μ.prod (stdGaussian E))) =
Measure.map Φ (μ.prod (stdGaussian E))
rw [Measure.map_map hR hΦ, hcomp, ← Measure.map_map hΦ hS, hprod]
end AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflectionScope and omitted-condition boundaries
- Only the generative-law symmetry component of Proposition 2.1(iii) is formalized here; source assimilation still needs (2.6)=(2.7).
- A measure-preserving deterministic reflection is not an invariance proof for the conditional half-turn process or the complete PBPS Markov chain.
- No conditional density, non-explosion, reversibility, L2 operator domain, mixing rate or query complexity is asserted.
- The claimed downstream uses in Section 3.1 and Appendix B are intended consumers, not already compiled Lean callers.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- ProbabilityTheory.stdGaussian_map: invariance of the standard Gaussian under linear isometric equivalence.
- LinearIsometryEquiv.neg: negation as a real linear isometry.
- MeasureTheory.Measure.map_prod_map, map_id and map_map: measurable product and composition pushforwards.
- Measurability of continuous affine maps; elementary additive-group cancellation.
Mathematical sources
- Chen, Chewi, Lu and Zhang, Accelerated High-Accuracy Sampling from a Warm Start via the Proximal Bouncy Particle Sampler v1 — Proposition 2.1(iii), with the generative law (2.7) and reflection (2.14). ASTIS exposition, not copied source prose.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.