Why reflecting the Gaussian auxiliary point preserves its joint law
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentation · theorem · Teaching coverage
Mathematical 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).
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))Proof roadmap
- 1Check 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.
- 2Reverse 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.
- 3Relate 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.
- 4Transport 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.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.GaussianReflectionSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The target is a strongly log-concave smooth Gibbs probability law on R^d | Any probability measure on a finite-dimensional real inner-product space with its Borel sigma algebra | generalization | The selected symmetry calculation only uses independence and symmetry of the auxiliary standard Gaussian. Neither a density nor potential regularity enters this proof component; the density adapter remains open. |
| 0<eta<=1/beta | 0<eta | generalization | The upper step-size restriction controls other curvature and algorithmic bounds. Gaussian sign symmetry works at every positive scale; it does not establish those bounds. |
| The joint law is written by both a normalized density and a generative representation | The joint law is explicitly a pushforward of mu.prod(stdGaussian E) | unresolved | The formalized measure is the generative representation. Identifying it with the density requires a separate normalization/change-of-variables proof. |
| The state-space maps are affine maps on Euclidean space | Measurability is proved from BorelSpace, finite-dimensional topology, addition and scalar multiplication | source-implicit | The pushforward composition rules require measurable maps. The proof supplies this prerequisite rather than treating the totalized map API as mathematical invariance. |
The generative-law proof component, not the density identification or any PBPS transition/process invariance theorem.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Compared with the full paper setting, the selected result allows arbitrary finite-dimensional real inner-product spaces. — Explicitly disclosed in extraction, module and lesson; a valid broader calculation.
- assumptions: The actual theorem allows any probability μ and all η>0, without Gibbs, smoothness, curvature or upper-step-size assumptions. — Explicit in lesson and candidate assumptions; not presented as proving those source assumptions.
- scopes: The source proposition concerns its density-defined joint law; the Lean law is a generative pushforward. — The missing density-to-generative identification is expressly a separate obligation. Acceptance covers only generative-reflection.
- scopes: The generative proof route does not formalize the source's direct density proof or its operator/process consequences. — No such closure is claimed. L² and algorithmic adapters remain outside this declaration.
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
- 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.