Actual Gaussian gradient-arc joint law and calculus

ASTIS mathematical restatement and proof exposition of the cited gradient-arc construction; used as a dependency of Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, Smoothed Picard Hamiltonian Monte Carlo. No author endorsement is implied.

Complete source statement (Samplinglib restatement)

The square of sqrt(eta) is eta. The map (h,r,x,z) to (gamma_r,v_r) is jointly measurable. For every real r its pushforward of the displayed input product law is N(h,eta I) product N(0,(pi/2)^2 eta I); in particular the position and velocity are independent. For every deterministic input pair, gamma has derivative v at every real r. Its positions at 0 and 1 are h+z and x; its velocities are (pi/2)(x-h) and -(pi/2)z.

Actual joint Gaussian law and derivative

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual Gaussian gradient-arc joint law and calculus

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianArcLaw.gaussian_arc_law · theorem · Teaching coverage

Read this first

Mathematical statement

\[(\gamma_r,v_r)_\#\bigl(N(h,\eta I)\otimes N(0,\eta I)\bigr)=N(h,\eta I)\otimes N(0,\tfrac{\pi^2}{4}\eta I),\qquad \frac{d}{dr}\gamma_r=v_r.\]

Lean statement · gaussian_arc_law

Actual product pushforward, joint measurability, pointwise path derivative and four endpoints at the source variance scale.

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.

Download module (.lean)

theorem gaussian_arc_law (eta : ℝ) (heta : 0 < eta) (h : E) :
    (Real.sqrt eta) ^ 2 = eta ∧
    Measurable (fun q : (E × ℝ) × (E × E) =>
      (arc q.1.1 q.1.2 q.2, velocity q.1.1 q.1.2 q.2)) ∧
    (∀ r : ℝ,
      (((stdGaussian E).map (fun x => h + Real.sqrt eta • x)).prod
        ((stdGaussian E).map (fun z => Real.sqrt eta • z))).map
        (fun p => (arc h r p, velocity h r p)) =
      ((stdGaussian E).map (fun x => h + Real.sqrt eta • x)).prod
        ((stdGaussian E).map (fun z => ((Real.pi / 2) * Real.sqrt eta) • z))) ∧
    (∀ (p : E × E) (r : ℝ), HasDerivAt (fun t => arc h t p) (velocity h r p) r) ∧
    (∀ p : E × E, arc h 0 p = h + p.2 ∧ arc h 1 p = p.1 ∧
      velocity h 0 p = (Real.pi / 2) • (p.1 - h) ∧
      velocity h 1 p = -(Real.pi / 2) • p.2)

Exact module and namespace context

Proof roadmap

1Start with actual independent standard Gaussian coordinates
Swap the two coordinates of the identical product measure; the law is unchanged. The existing centered Gaussian rotation theorem applies because every continuous linear functional has mean zero under the standard Gaussian.
2Transport the rotation to the actual input scales and center
Express the input as the product pushforward of h+sigma G1 and sigma G2. Compose the arc map with that input map. Scalar distributivity shows it equals the invariant rotation followed by the output map (u,w) to (h+sigma u,(pi/2)sigma w). Product-map and map-composition identities prove the entire joint product law, not merely two marginals.
3Prove joint measurability of the path and velocity
Coordinates, addition, subtraction, real scalar multiplication and sine/cosine are continuous. Their displayed compositions are jointly measurable in the center, time and both input vectors. This establishes deterministic parameter measurability without asserting a parameterized Gaussian-kernel theorem.
4Differentiate the actual path
The derivative of pi*r/2 is pi/2. The sine and cosine chain rules, scalar-vector multiplication and addition give the displayed velocity; the cosine derivative contributes the negative sine sign. The proof holds at every real time.
5Evaluate all endpoints and restore the source variance
At zero and pi/2, exact sine and cosine values give the four endpoint identities. The initial position includes the auxiliary Gaussian sample. Finally eta>0 justifies sqrt(eta)^2=eta and specializes the general affine law to the source variance.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner product space with its Borel measurable structure; second countability is explicitly available. Zero dimension is allowed.
eta>0 and h in E. The input is the actual independent product law of X=h+sqrt(eta)G1 and Z=sqrt(eta)G2, where G1,G2 are standard Gaussian.
For r in the real line set theta=pi*r/2, gamma_r=h+sin(theta)(X-h)+cos(theta)Z and v_r=(pi/2)(cos(theta)(X-h)-sin(theta)Z). Source consumption only requires r in [0,1].

Mathematical proof

1. Start with actual independent standard Gaussian coordinates

Swap the two coordinates of the identical product measure; the law is unchanged. The existing centered Gaussian rotation theorem applies because every continuous linear functional has mean zero under the standard Gaussian.

\[R_\theta(z,x)=(\cos\theta\,z+\sin\theta\,x,-\sin\theta\,z+\cos\theta\,x).\]

Corresponding Lean step

Measure.prod_swap; IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero; integral_strongDual_stdGaussian

2. Transport the rotation to the actual input scales and center

Express the input as the product pushforward of h+sigma G1 and sigma G2. Compose the arc map with that input map. Scalar distributivity shows it equals the invariant rotation followed by the output map (u,w) to (h+sigma u,(pi/2)sigma w). Product-map and map-composition identities prove the entire joint product law, not merely two marginals.

\[\sigma=\sqrt\eta,\qquad (u,w)\longmapsto(h+\sigma u,\tfrac\pi2\sigma w).\]

Corresponding Lean step

affine_arc_law; Measure.map_prod_map; Measure.map_map

3. Prove joint measurability of the path and velocity

Coordinates, addition, subtraction, real scalar multiplication and sine/cosine are continuous. Their displayed compositions are jointly measurable in the center, time and both input vectors. This establishes deterministic parameter measurability without asserting a parameterized Gaussian-kernel theorem.

\[(h,r,x,z)\longmapsto(\gamma_r(x,z),v_r(x,z)).\]

Corresponding Lean step

arc_joint_measurable; fun_prop

4. Differentiate the actual path

The derivative of pi*r/2 is pi/2. The sine and cosine chain rules, scalar-vector multiplication and addition give the displayed velocity; the cosine derivative contributes the negative sine sign. The proof holds at every real time.

\[\gamma_r^{\prime}=\tfrac\pi2\left(\cos(\tfrac\pi2r)(x-h)-\sin(\tfrac\pi2r)z\right).\]

Corresponding Lean step

arc_derivative; HasDerivAt.sin; HasDerivAt.cos; HasDerivAt.smul_const

5. Evaluate all endpoints and restore the source variance

At zero and pi/2, exact sine and cosine values give the four endpoint identities. The initial position includes the auxiliary Gaussian sample. Finally eta>0 justifies sqrt(eta)^2=eta and specializes the general affine law to the source variance.

\[\gamma_0=h+z,\quad\gamma_1=x,\quad v_0=\tfrac\pi2(x-h),\quad v_1=-\tfrac\pi2z.\]

Corresponding Lean step

arc_endpoints; Real.sq_sqrt; gaussian_arc_law

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · gaussian_arc_law

Centered Gaussian rotation invariance, actual affine pushforwards, elementary continuous-map measurability and trigonometric differentiation.

Download module (.lean)

theorem gaussian_arc_law (eta : ℝ) (heta : 0 < eta) (h : E) :
    (Real.sqrt eta) ^ 2 = eta ∧
    Measurable (fun q : (E × ℝ) × (E × E) =>
      (arc q.1.1 q.1.2 q.2, velocity q.1.1 q.1.2 q.2)) ∧
    (∀ r : ℝ,
      (((stdGaussian E).map (fun x => h + Real.sqrt eta • x)).prod
        ((stdGaussian E).map (fun z => Real.sqrt eta • z))).map
        (fun p => (arc h r p, velocity h r p)) =
      ((stdGaussian E).map (fun x => h + Real.sqrt eta • x)).prod
        ((stdGaussian E).map (fun z => ((Real.pi / 2) * Real.sqrt eta) • z))) ∧
    (∀ (p : E × E) (r : ℝ), HasDerivAt (fun t => arc h t p) (velocity h r p) r) ∧
    (∀ p : E × E, arc h 0 p = h + p.2 ∧ arc h 1 p = p.1 ∧
      velocity h 0 p = (Real.pi / 2) • (p.1 - h) ∧
      velocity h 1 p = -(Real.pi / 2) • p.2) := by
  refine ⟨Real.sq_sqrt heta.le, arc_joint_measurable, ?_, ?_, arc_endpoints h⟩
  · intro r
    exact affine_arc_law h (Real.sqrt eta) (Real.pi / 2 * r)
  · intro p r
    exact arc_derivative h p.1 p.2 r


end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianArcLaw

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Euclidean position and Gaussian auxiliary with common variance eta, eta>0.	Finite-dimensional real inner product space with Borel structure and explicit second countability; eta>0, actual affine standard-Gaussian product.	generalization	Basis-independent presentation includes zero dimension; no new source geometric restriction.
The interpolation parameter belongs to [0,1].	Joint law and derivative hold for all real times; endpoints 0 and 1 are proved.	generalization	The trigonometric identities and rotation invariance apply for every real angle.
The estimator uses h=x0-eta grad f(x_plus).	Arbitrary fixed center h; joint deterministic map measurable also in h.	generalization	The joint Gaussian law does not need the subsequent gradient assumptions. Actual estimator substitution and moment analysis remain separate.
Joint Gaussian position and velocity are independent with respective covariance eta I and (pi/2)^2 eta I.	Actual full product pushforward equality at standard deviations sqrt eta and (pi/2)sqrt eta.	same	The whole product law, rather than just marginal Gaussian laws, supplies independence.
The gradient estimator is followed by exponential-moment and clipping analysis.	Only Gaussian arc law, derivative, endpoints and deterministic joint measurability are proved.	API-limitation	A prerequisite boundary is explicit; no Claim 1 moment bound, measure-family measurability or full terminal sampler completion is asserted.

This is the actual Gaussian path prerequisite, not an exponential-moment or clipping theorem. The gradient-estimator consumer must separately substitute h=x0-eta grad f(x_plus), establish gradient and reference-point conditions, and prove moment, clipping and target-error bounds. No measurability of the eta-indexed measure family or full terminal sampler is asserted. The external printed Claim 1 log-moment discrepancy is a separate possible-source-error, not silently repaired by this result.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: Basis-independent domain includes zero dimension. — Independent formal reviewer accepted this disclosed delta.
quantifiers: All-real-time law and derivative extend source interval. — Independent formal reviewer accepted this disclosed delta.
assumptions: Arbitrary center is valid; gradient substitution remains separate. — Independent formal reviewer accepted this disclosed delta.
conclusion: Actual product law preserves exact scales and independence. — Independent formal reviewer accepted this disclosed delta.
scopes: No moment, clipping, accuracy or complete sampler assertion. — Independent formal reviewer accepted this disclosed delta.

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 the actual Gaussian path prerequisite, not an exponential-moment or clipping theorem. The gradient-estimator consumer must separately substitute h=x0-eta grad f(x_plus), establish gradient and reference-point conditions, and prove moment, clipping and target-error bounds. No measurability of the eta-indexed measure family or full terminal sampler is asserted. The external printed Claim 1 log-moment discrepancy is a separate possible-source-error, not silently repaired by this result.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero
ProbabilityTheory.integral_strongDual_stdGaussian
MeasureTheory.Measure.prod_swap
MeasureTheory.Measure.map_prod_map
MeasureTheory.Measure.map_map
Real.sq_sqrt

Mathematical sources

Appendix D.1 gradient arc and Claim 1 — Actual independent position and velocity law used before exponential-moment analysis.
SPHMC Appendix A.1 and A.4(2) — Terminal gradient-estimator consumer of the external arc construction.

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

Actual Gaussian gradient-arc joint law and calculus

Complete source statement (Samplinglib restatement)

Actual joint Gaussian law and derivative

Read the formalized proofs

Actual Gaussian gradient-arc joint law and calculus

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Start with actual independent standard Gaussian coordinates

2. Transport the rotation to the actual input scales and center

3. Prove joint measurability of the path and velocity

4. Differentiate the actual path

5. Evaluate all endpoints and restore the source variance

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?