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

GaussianArcLaw: 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. Actual Gaussian gradient-arc joint law and calculus
ASTIS mathematical exposition

Actual Gaussian gradient-arc joint law and calculus

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

Statement

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.

\[(\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.\]

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 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.

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

Lean proof · gaussian_arc_law

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

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 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

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.

Source and reuse

ASTIS 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

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