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

GradientArcMean: 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 unclipped gradient-arc mean
ASTIS mathematical exposition

Actual unclipped gradient-arc mean

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean.gradient_arc_mean · theorem · Teaching coverage

Statement

The square of sqrt(eta) equals eta, U is a probability measure, and f(h+Z) is integrable under P. Define the finite constant C=integral f(h+z) dP(z)-<grad f(x_plus),h> before choosing x. For every x, W_x is jointly measurable and integrable under U product P, its integral is <grad f(x_plus),x>-f(x)+C, and for every z its time integral from 0 to 1 equals <grad f(x_plus),x-(h+z)>-f(x)+f(h+z).

\[\mathbb E_{(r,Z)\sim U\otimes P}W_x(r,Z)=\langle\nabla f(x_+),x\rangle-f(x)+C,\qquad C=\mathbb E_P f(h+Z)-\langle\nabla f(x_+),h\rangle.\]

All objects and hypotheses

  • E is a finite-dimensional real inner-product space with its Borel measurable structure; second countability is explicit and automatic for this domain. The real-valued potential f is differentiable everywhere and its actual gradient is globally beta-Lipschitz.
  • eta>0, beta>=0 and h,x_plus are arbitrary points. No positive dimension, convexity, center residual or clipping step restriction is assumed.
  • P is the pushforward of stdGaussian E by z -> sqrt(eta) z, hence the actual auxiliary N(0,eta I). U is Lebesgue measure restricted to (0,1], which is the same uniform probability law as on [0,1].
  • For each x,z and real r, theta=pi*r/2, gamma=h+sin(theta)(x-h)+cos(theta)z, v=(pi/2)(cos(theta)(x-h)-sin(theta)z), and W_x(r,z)=<v,grad f(x_plus)-grad f(gamma)>.

Mathematical proof

1. Use the actual auxiliary input and uniform time

The noise is the pushforward of the centered identity-covariance Gaussian by sqrt(eta) scaling. Positive eta gives the exact variance identity. Lebesgue measure on (0,1] has total mass one. The choice of one open endpoint changes no probability mass and agrees with the interval-integral convention used below.

\[(\sqrt\eta)^2=\eta,\qquad U=\mathrm{Leb}|_{(0,1]},\qquad U(\mathbb R)=1.\]
Corresponding Lean step

gradient_arc_mean; Real.sq_sqrt

2. Integrate the actual path derivative

Extract the public derivative and endpoints from GaussianArcLaw. Its auxiliary scale value 1 is used only to obtain these deterministic facts, never to replace the actual noise law. Apply the true gradient chain rule to r -> <grad f(x_plus),gamma_r>-f(gamma_r). The Lipschitz gradient and continuous path imply that its derivative W is continuous, so FTC applies. The path starts at h+z and ends at x.

\[\int_0^1 W_x(r,z)\,dr=\langle\nabla f(x_+),x-(h+z)\rangle-f(x)+f(h+z).\]
Corresponding Lean step

path_integral; GaussianArcLaw.gaussian_arc_law; DifferentiableAt.hasGradientAt; HasFDerivAt.comp_hasDerivAt; intervalIntegral.integral_eq_sub_of_hasDerivAt

3. Prove potential integrability from quadratic growth

Along the straight line h+t z, the gradient norm is at most norm(grad f(h))+beta norm(z) for t in [0,1]. The segment derivative bound yields the displayed quadratic growth estimate; no convexity is required. Gaussian second moments persist under actual scalar pushforward, so the constant, linear norm and squared norm terms are integrable. Measurable domination proves f(h+Z) integrable before defining its expectation.

\[|f(h+z)|\le |f(h)|+\|\nabla f(h)\|\,\|z\|+\beta\|z\|^2.\]
Corresponding Lean step

potential_growth; potential_integrable; norm_image_sub_le_of_norm_deriv_le_segment_01'; ProbabilityTheory.IsGaussian.memLp_two_id; MeasureTheory.integrable_map_measure

4. Bound the same estimator uniformly in time

Let A=norm(x-h) and D=norm(x_plus-h). Sine and cosine are bounded by one in absolute value, so the speed norm is at most (pi/2)(A+norm(z)) and the arc distance from x_plus is at most D+A+norm(z). Apply the actual gradient Lipschitz inequality and the inner-product norm inequality. This bound holds for every real time; it supplies one majorant for the whole uniform-time integral.

\[|W_x(r,z)|\le\frac\pi2\,\beta(A+\|z\|)(D+A+\|z\|).\]
Corresponding Lean step

estimator_bound; norm_inner_le_norm; LipschitzWith.norm_sub_le

5. Establish joint integrability before Fubini

Expand the majorant as a constant plus a linear norm term plus a squared norm term. The actual mapped Gaussian has finite second moment, making this polynomial integrable. Its lift to the product with the finite uniform-time measure is integrable. Gradient continuity makes the explicit W jointly measurable; domination then proves W integrable under the product. The proof does not infer joint integrability merely from fixed-time sections.

\[W_x\in L^1(U\otimes P).\]
Corresponding Lean step

estimator_integrable; MeasureTheory.memLp_map_measure_iff; MeasureTheory.MemLp.integrable_sq; MeasureTheory.Integrable.comp_snd; MeasureTheory.Integrable.mono'

6. Identify one finite constant for every x

Use Fubini only after the preceding joint-integrability result, then replace each time integral by the FTC identity. The actual auxiliary mean is zero, proved by the Gaussian map integral and scalar linearity. The linear, constant and potential terms are individually integrable, so their integrals can be separated. The remaining C depends on f,h,x_plus,eta and is defined before the universal quantifier over x.

\[\mathbb E_P\langle\nabla f(x_+),x-(h+Z)\rangle=\langle\nabla f(x_+),x-h\rangle,\qquad \mathbb E_P Z=0.\]
Corresponding Lean step

auxiliary_mean; MeasureTheory.integral_prod_symm; intervalIntegral.integral_of_le; ProbabilityTheory.integral_id_stdGaussian; integral_inner; gradient_arc_mean

Lean statement · gradient_arc_mean

Actual Gaussian/uniform input integrability, path integral and a common finite constant identifying the mean for every fixed output point.

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 gradient_arc_mean (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (h xp : E) :
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    (Real.sqrt eta)^2 = eta ∧ IsProbabilityMeasure U ∧
      Integrable (fun z => f (h+z)) P ∧
      ∀ x : E, Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) ∧
        Integrable (fun q : ℝ × E => estimator f h xp x q.2 q.1) (U.prod P) ∧
        (∀ z : E, (∫ r in (0 : ℝ)..1, estimator f h xp x z r) =
          inner ℝ (gradient f xp) (x-(h+z)) - f x + f (h+z)) ∧
        (∫ q : ℝ × E, estimator f h xp x q.2 q.1 ∂(U.prod P)) =
          inner ℝ (gradient f xp) x - f x + C

Exact module and namespace context

Lean proof · gradient_arc_mean

Actual arc calculus, quadratic potential growth, true Gaussian moments, joint polynomial domination, Fubini and zero auxiliary mean.

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 gradient_arc_mean (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (h xp : E) :
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    (Real.sqrt eta)^2 = eta ∧ IsProbabilityMeasure U ∧
      Integrable (fun z => f (h+z)) P ∧
      ∀ x : E, Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) ∧
        Integrable (fun q : ℝ × E => estimator f h xp x q.2 q.1) (U.prod P) ∧
        (∀ z : E, (∫ r in (0 : ℝ)..1, estimator f h xp x z r) =
          inner ℝ (gradient f xp) (x-(h+z)) - f x + f (h+z)) ∧
        (∫ q : ℝ × E, estimator f h xp x q.2 q.1 ∂(U.prod P)) =
          inner ℝ (gradient f xp) x - f x + C := by
  dsimp only
  refine ⟨Real.sq_sqrt heta.le, ⟨by simp⟩,
    potential_integrable f hf ⟨beta,hbeta⟩ hlip h (Real.sqrt eta), ?_⟩
  intro x
  have hg := hlip.continuous
  have hm : Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) := by
    unfold estimator arc velocity
    fun_prop
  exact ⟨hm, estimator_integrable f ⟨beta,hbeta⟩ hlip h xp x (Real.sqrt eta) _,
    fun z => path_integral f hf ⟨beta,hbeta⟩ hlip h xp x z,
    auxiliary_mean f hf ⟨beta,hbeta⟩ hlip h xp x (Real.sqrt eta)⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean

Exact module and namespace context

Scope and omitted-condition boundaries

  • This proves the actual unclipped estimator mean for each fixed x, including genuine Gaussian/uniform joint integrability. Coordinate-free spaces, zero dimension, beta=0 and arbitrary h are disclosed extensions. It does not assert joint parameter measurability in x,h,x_plus or an additional random-x integral. The source center h=x0-eta grad f(x_plus), completion of the Gaussian square, positive finite target normalization, clipped output law, Renyi comparison, initialization and actual query costs remain separate. L1 integrability of f(h+Z) does not imply exponential Gibbs integrability. Neither full companion paper is complete.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • DifferentiableAt.hasGradientAt
  • HasFDerivAt.comp_hasDerivAt
  • intervalIntegral.integral_eq_sub_of_hasDerivAt
  • norm_image_sub_le_of_norm_deriv_le_segment_01'
  • ProbabilityTheory.IsGaussian.memLp_two_id
  • MeasureTheory.memLp_map_measure_iff
  • MeasureTheory.integrable_map_measure
  • MeasureTheory.Integrable.comp_snd
  • MeasureTheory.integral_prod_symm
  • ProbabilityTheory.integral_id_stdGaussian
  • integral_inner

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.